decide_eqb_ok@{i} {A:Type@{i} } `{DecidablePaths A} : forall a b, iff@{Set i i} (eqb a b = true) (a = b). Proof. unfold eqb,decide_eqb. intros a b;destruct (decide_rel paths a b) as [E1|E1];split;intros E2;auto. - destruct (false_ne_true E2). - destruct (E1 E2). Qed.
Require Import HoTT.Classes.interfaces.canonical_names.