Definition negrtopaths {X : UU} (R : decrel X) (x x' : X) (nr : neg (R x x')) : decreltobrel R x x' = false. Proof. unfold decreltobrel. intros. induction (pr2 R x x') as [ r | nr' ]. - induction (nr r). - apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.