Definition tosubquot {X : UU} (R : eqrel X) (P : hsubtype (setquot R)) : setquot (resrel R (funcomp (setquotpr R) P)) -> P. Proof. assert (int : isaset P). { apply (isasetsubset (@pr1 _ P)). - apply (setproperty (setquotinset R)). - refine (isinclpr1carrier _). } apply (setquotuniv _ (make_hSet _ int) (λ xp, make_carrier P (setquotpr R (pr1 xp)) (pr2 xp))). intros xp1 xp2 rp12. apply (invmaponpathsincl _ (isinclpr1carrier P) _ _). simpl. apply (iscompsetquotpr). apply rp12. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.