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