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’.
2
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.