Definition setquottosetquot2 (X : UU) (R : hrel X) (is : iseqrel R) : setquot R -> setquot2 R. Proof. intros X0. apply (setquotuniv R (make_hSet _ (isasetsetquot2 R)) (setquot2pr R) (iscompsetquot2pr R) X0). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.