Definition pathstonegr {X : UU} (R : decrel X) (x x' : X) (e : decreltobrel R x x' = false) : neg (R x x'). Proof. unfold decreltobrel in e. induction (pr2 R x x') as [ e' | ne ]. - induction (nopathstruetofalse e). - apply ne. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.