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. intro R. transitivity ((y • x) • inv_x^-1). - rewrite <- vassocr, vcomp_rinv. apply (!id2_right _). - rewrite R, <- vassocr, vcomp_rinv. apply id2_right. 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.