Lemma isdecreltoisnegrel {X : UU} {R : hrel X} (is : isdecrel R) : isnegrel R. Proof. intros. intros x1 x2. induction (is x1 x2) as [ r | nr ]. - intro. apply r. - intro nnr. induction (nnr nr). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.