Know your types!
• Sum types (+)
• Dependent sum types (Σ)
• Product types (×)
• Dependent product types (Π)
2
13
Conversation
are quotient types a thing
2
3
Yes! They pop up in homotopy type theory and are pretty useful. Although they are probably not ‘quotients’ in the way you are thinking (ie. being like ‘division’ in arithmetic). I think those are usually called ‘fractional types’.
Fractional types are a bit less understood afaik – there was a preprint floating about for a while that wasn’t published due to some stumbling blocks in the metatheory. I think they *might* have been fixed in a recent paper, but I’m not an expert on this stuff!
3
They're like taking a big thing and mapping it onto a smaller thing, but with types, right?
1
1
I *think* that's it! Like, you can say that some elements of the bigger thing are the same, using an equivalence relation? But yeah, this is just what I've gleaned as a non-expert.
2