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