Definition weqsetquotweq {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X ≃ Y) (is1 : iscomprelrelfun RX RY f) (is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') : (setquot RX) ≃ (setquot RY). Proof. intros. set (ff := setquotfun RX RY f is1). split with ff. assert (is2' : ∏ y y' : Y, RY y y' -> RX (invmap f y) (invmap f y')). intros y y'. rewrite (pathsinv0 (homotweqinvweq f y)). rewrite (pathsinv0 (homotweqinvweq f y')). rewrite (homotinvweqweq f (invmap f y)). rewrite (homotinvweqweq f (invmap f y')). apply (is2 _ _). set (gg := setquotfun RY RX (invmap f) is2'). assert (egf : ∏ a, paths (gg (ff a)) a). { apply (setquotunivprop RX (λ a0, make_hProp _ (isasetsetquot RX (gg (ff a0)) a0))). simpl. intro x. unfold ff. unfold gg. apply (maponpaths (setquotpr RX) (homotinvweqweq f x)). } assert (efg : ∏ a, paths (ff (gg a)) a). { apply (setquotunivprop RY (λ a0, make_hProp _ (isasetsetquot RY (ff (gg a0)) a0))). simpl. intro x. unfold ff. unfold gg. apply (maponpaths (setquotpr RY) (homotweqinvweq f x)). } apply (isweq_iso _ _ egf efg). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.