Theorem weqsetquottodirprod {X Y : UU} (RX : eqrel X) (RY : eqrel Y) : weq (setquot (eqreldirprod RX RY)) ((setquot RX) × (setquot RY)). Proof. intros. set (f := setquottodirprod RX RY). set (g := dirprodtosetquot RX RY). split with f. assert (egf : ∏ a : _, paths (g (f a)) a). { apply (setquotunivprop _ (λ a : _, (make_hProp _ (isasetsetquot _ (g (f a)) a)))). intro xy. induction xy as [ x y ]. simpl. apply (invmaponpathsincl _ (isinclpr1setquot _)). simpl. apply funextsec. intro xy'. induction xy' as [ x' y' ]. apply idpath. } assert (efg : ∏ a : _, paths (f (g a)) a). { intro a. induction a as [ ax ay ]. apply pathsdirprod. generalize ax. clear ax. apply (setquotunivprop RX (λ ax : _, (make_hProp _ (isasetsetquot _ _ _)))). intro x. simpl. generalize ay. clear ay. apply (setquotunivprop RY (λ ay : _, (make_hProp _ (isasetsetquot _ _ _)))). intro y. simpl. apply (invmaponpathsincl _ (isinclpr1setquot _)). apply funextsec. intro x0. simpl. apply idpath. generalize ax. clear ax. apply (setquotunivprop RX (λ ax : _, (make_hProp _ (isasetsetquot _ _ _)))). intro x. simpl. generalize ay. clear ay. apply (setquotunivprop RY (λ ay : _, (make_hProp _ (isasetsetquot _ _ _)))). intro y. simpl. apply (invmaponpathsincl _ (isinclpr1setquot _)). apply funextsec. intro x0. simpl. apply idpath. } apply (isweq_iso _ _ egf efg). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.