fact: 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 _).
imports: UniMath.Foundations.Propositions