proposition: Lemma vcomp_move_L_Mp {C : bicat} {X Y : C} {f g h : C⟦X,Y⟧} (η₁ : f ==> h) (η₂ : f ==> g) (ε : g ==> h) (Hε : is_invertible_2cell ε) : Hε^-1 o η₁ = η₂ -> η₁ = ε o η₂.
proof: Proof. intros. rewrite <- (id2_right η₁). rewrite <- (vcomp_linv Hε). rewrite vassocr. apply maponpaths_2. assumption. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat