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