Definition isantisymmnegresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : isantisymmneg L) : isantisymmneg (resrel L P). Proof. intros. intros x1 x2 nr12 nr21. apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ (isl _ _ nr12 nr21)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.