Definition isirreflresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : isirrefl L) : isirrefl (resrel L P). Proof. intros. intros x r. apply (isl _ r). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.