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