Effective Quotient

In type theory, a quotient type $X/R$ is said to be effective if the Identity Type on $X/R$ coincides exactly with the Equivalence Relation $R$. Notably, a quotient $X/R$ is effective if the following Inference Rule is Admissible:

This was historically quite hard to do without breaking Canonicity, as simply adding the $\mathsf{eff}$ terms causes computation to get stuck. Moreover, if the equality type is a Strict Proposition yet $R$ is an H-Proposition, this is literally impossible without some form of Equality Reflection see Section 8.2 of A Cubical Language for Bishop Sets.

This gets extra tricky if one decides to erase propositions, as there is literally no way to recover proofs of $R(x,y)$. This can be solved in a couple of ways:

• Via Quotient Inductive Types or Higher Inductive Types, where we store the proofs of $R(x,y)$ used to equate terms in the quotient as extra inductive constructors. When eliminating, these inductives require us to eliminate into the Identity Type of the motive, which also has the nice benefit of removing side conditions to the elimination form for quotients
• Via Observational Type Theory, where the identity type of the quotient $X/R$ literally is $R$. This is conceptually elegant, but