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