Theorem setquotpr {X : UU} (R : eqrel X) : X -> setquot R. Proof. intros X0. set (rax := eqrelrefl R). set (sax := eqrelsymm R). set (tax := eqreltrans R). apply (tpair _ (λ x : X, R X0 x)). split. - exact (hinhpr (tpair _ X0 (rax X0))). - split; intros x1 x2 X1 X2. + exact (tax X0 x1 x2 X2 X1). + exact (tax x1 X0 x2 (sax X0 x1 X1) X2). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.