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