Quotient Types #4
Description
We want quotient types. We could do it in the standard way similar to how Lean does it. The only question is whether we should make the beta law propositional or definitional. IIRC a definitional beta law for quotients in this manner causes a loss of subject reduction (don't quote me), but that honestly shouldn't matter since we already lose subjection reduction due to extensional identity.