Definition iscoantisymmresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : iscoantisymm L) : iscoantisymm (resrel L P). Proof. intros. intros x1 x2 r12. induction (isl _ _ r12) as [ l | e ]. - apply (ii1 l). - apply ii2. apply (invmaponpathsincl _ (isinclpr1carrier _) _ _ e). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.