Definition confirm_equal {X : UU} (i : isdeceq X) (x x' : X) (e : decreltobrel (deceq_to_decrel i) x x' = true) : x = x'. Proof. intros. exact (pathstor (deceq_to_decrel i) _ _ e). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.