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. intro R. transitivity (inv_x^-1 • (x • y)). - rewrite vassocr, vcomp_linv. apply (!id2_left _). - rewrite R, vassocr, vcomp_linv. apply id2_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.