Why is reflexivity enough in this HoTT formulation of quotient types?

In this formulation of quotient types in cubical type theory I was able to implement an eliminator and use that to implement basically curried function application. However, in all this, the only requirement on the factoring relation is that it is reflexive.

I find this surprising. I would have expected transitivity and symmetry to also be needed somewhere along the way. Is there an intuitive explanation for why reflexivity is enough?

Your Quot construction is a set-truncated quotient by an arbitrary relation $R$ since you never use the reflexivity assumption in the construction. That is, you don't even need the reflexivity of $R$ to perform the quotient and derive its basic properties.

As the HoTT book explains in Section 6.10, it is perfectly possible to make set-truncated quotients by an arbitrary relation because reflexivity, transitivity and symmetry are taken care of by the paths themselves (because there are identity paths, paths can be reversed, and composed). That is, the quotient $A/R$ is equivalent to the quotient $A/\overline{R}$ where $\overline{R}$ is the equivalence relation generated by $R$.

There is one property that you will not get, namely that (using the notations from your file) $(x : A) \to (y : A) \to \mathsf{point}\;x = \mathsf{point}\;y \to R\;x\;y$. For that you need the fact that $R$ is a proposition and an equivalence relation.

StackExchange Computer Science Q#99910, answer score: 4