Definition istransdirprod {X Y : UU} (RX : hrel X) (RY : hrel Y) (isx : istrans RX) (isy : istrans RY) : istrans (hreldirprod RX RY) := λ xy1 xy2 xy3 : _, λ is12 : _ , λ is23 : _, make_dirprod (isx _ _ _ (pr1 is12) (pr1 is23)) (isy _ _ _ (pr2 is12) (pr2 is23)).
Require Import UniMath.Foundations.UnivalenceAxiom.