Definition paths_inl_inl_equiv {A B : UU} (a a' : A) : @inl A B a = inl a' ≃ a = a'. Proof. apply @equality_by_case_equiv. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.