Lemma isdecnegrel {X : UU} (R : hrel X) (isr : isdecrel R) : isdecrel (negrel R). Proof. intros. intros x1 x2. induction (isr x1 x2) as [ r | nr ]. - apply ii2. apply (todneg _ r). - apply (ii1 nr). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.