Definition isrefldirprod {X Y : UU} (RX : hrel X) (RY : hrel Y) (isx : isrefl RX) (isy : isrefl RY) : isrefl (hreldirprod RX RY) := λ xy : _, make_dirprod (isx _) (isy _).
Require Import UniMath.Foundations.UnivalenceAxiom.