proposition: Lemma vcomp_lcancel {C : prebicat} {a b : C} {f g : C⟦a, b⟧} (x : f ==> g) (inv_x : is_invertible_2cell x) {h : C⟦a, b⟧} {y z : g ==> h} : x • y = x • z -> y = z.
proof: Proof. intro R. transitivity (inv_x^-1 • (x • y)). - rewrite vassocr, vcomp_linv. apply (!id2_left _). - rewrite R, vassocr, vcomp_linv. apply id2_left. 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