Definition neqchoiceresrel {X : UU} (L : hrel X) (P : hsubtype X) (isl : neqchoice L) : neqchoice (resrel L P). Proof. intros. intros x1 x2 ne. set (int := negf (invmaponpathsincl _ (isinclpr1carrier P) _ _) ne). apply (isl _ _ int). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.