Why is reflexivity enough in this HoTT formulation of quotient types?
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.