Definition eqreldirprod {X Y : UU} (RX : eqrel X) (RY : eqrel Y) : eqrel (X × Y) := eqrelconstr (hreldirprod RX RY) (istransdirprod _ _ (eqreltrans RX) (eqreltrans RY)) (isrefldirprod _ _ (eqrelrefl RX) (eqrelrefl RY)) (issymmdirprod _ _ (eqrelsymm RX) (eqrelsymm RY)).
Require Import UniMath.Foundations.UnivalenceAxiom.