Definition dirprodtosetquot {X Y : UU} (RX : hrel X) (RY : hrel Y) (cd : (setquot RX) × (setquot RY)) : setquot (hreldirprod RX RY) := make_setquot _ _ (iseqclassdirprod (pr2 (pr1 cd)) (pr2 (pr2 cd))).
Require Import UniMath.Foundations.UnivalenceAxiom.