Definition weqsubquot {X : UU} (R : eqrel X) (P : hsubtype (setquot R)) : weq P (setquot (resrel R (funcomp (setquotpr R) P))). Proof. intros. set (f := fromsubquot R P). set (g := tosubquot R P). split with f. assert (int0 : isaset P). { apply (isasetsubset (@pr1 _ P)). - apply (setproperty (setquotinset R)). - refine (isinclpr1carrier _). } assert (egf : ∏ (a : P), paths (g (f a)) a). { intros a. induction a as [ p isp ]. generalize isp. generalize p. clear isp. clear p. assert (int : ∏ (p : setquot R), isaprop (∏ isp : P p, paths (g (f (tpair _ p isp))) (tpair _ p isp))). { intro p. apply impred. intro. apply (int0 _ _). } apply (setquotunivprop _ (λ a, make_hProp _ (int a))). simpl. intros x isp. apply (invmaponpathsincl _ (isinclpr1carrier P) _ _). apply idpath. } assert (efg : ∏ (a : setquot (resrel R (P ∘ setquotpr R))), paths (f (g a)) a). { assert (int : ∏ a, isaprop (paths (f (g a)) a)). { intro a. apply (setproperty (setquotinset (resrel R (funcomp (setquotpr R) P)))). } set (Q := reseqrel R (funcomp (setquotpr R) P)). apply (setquotunivprop Q (fun a : setquot (resrel R (funcomp (setquotpr R) P)) => make_hProp _ (int a))). intro a. simpl. unfold f. unfold g. unfold fromsubquot. unfold tosubquot. apply (invmaponpathsincl _ (isinclpr1 _ (λ a, isapropiseqclass _ a))). apply idpath. } apply (isweq_iso _ _ egf efg). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.