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
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!