Definition ctlong {X : UU} (R : hrel X) (is : isdecrel R) (x x' : X) (e : decreltobrel (make_decrel is) x x' = true) : R x x'. Proof. unfold decreltobrel in e. simpl in e. induction (is x x') as [ e' | ne ]. - apply e'. - induction (nopathsfalsetotrue e). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.