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