Lemma equality_by_case_equiv {A B} (t u : A ⨿ B) : (t = u) ≃ equality_cases t u. Proof. use weq_iso. - apply equality_by_case. - apply inv_equality_by_case. - apply inv_equality_by_case_equality_by_case. - apply equality_by_case_inv_equality_by_case. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.