Lemma whisker_r_iso_id₁ {X Y : C} {f : C⟦X,X⟧} (η : id₁ X ==> f) (k₁ k₂ : C⟦X,Y⟧) (α : k₁ ==> k₂) (inv_η : is_invertible_2cell η) : α = lunitor k₂ o (k₂ ◅ inv_η^-1) o (α ▻ f) o (k₁ ◅ η) o linvunitor k₁. Proof. rewrite !vassocr. use vcomp_move_L_Mp. { is_iso. } use vcomp_move_L_Mp. { is_iso. } rewrite <- !vassocr. exact (whisker_l_natural η k₁ k₂ α). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors.