proposition: Lemma vcomp_rcancel {C : prebicat} {a b : C} {f g : C⟦a, b⟧} (x : f ==> g) (inv_x : is_invertible_2cell x) {e : C⟦a, b⟧} {y z : e ==> f} : y • x = z • x -> y = z.
proof: Proof. intro R. transitivity ((y • x) • inv_x^-1). - rewrite <- vassocr, vcomp_rinv. apply (!id2_right _). - rewrite R, <- vassocr, vcomp_rinv. apply id2_right. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct