Definition hreldirprod {X Y : UU} (RX : hrel X) (RY : hrel Y) : hrel (X × Y) := λ xy xy' : dirprod X Y, hconj (RX (pr1 xy) (pr1 xy')) (RY (pr2 xy) (pr2 xy')).
Require Import UniMath.Foundations.UnivalenceAxiom.