Definition setquottodirprod {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (cc : setquot (eqreldirprod RX RY)) : (setquot RX) × (setquot RY). Proof. intros. set (RXY := eqreldirprod RX RY). apply (make_dirprod (setquotuniv RXY (setquotinset RX) (funcomp (@pr1 _ (λ x : _, Y)) (setquotpr RX)) (λ xy xy' : dirprod X Y, λ rr : RXY xy xy', iscompsetquotpr RX _ _ (pr1 rr)) cc) (setquotuniv RXY (setquotinset RY) (funcomp (@pr2 _ (λ x : _, Y)) (setquotpr RY)) (λ xy xy' : dirprod X Y, λ rr : RXY xy xy', iscompsetquotpr RY _ _ (pr2 rr)) cc)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.