proposition: Lemma whisker_l_iso_id₁ {X Y : C} {f : C⟦X,X⟧} (η : id₁ X ==> f) (k₁ k₂ : C⟦Y,X⟧) (α : k₁ ==> k₂) (inv_η : is_invertible_2cell η) : α = runitor k₂ o (inv_η^-1 ▻ k₂) o (f ◅ α) o (η ▻ k₁) o rinvunitor k₁.
proof: Proof. rewrite !vassocr. use vcomp_move_L_Mp. { is_iso. } use vcomp_move_L_Mp. { is_iso. } rewrite <- !vassocr. exact (whisker_r_natural η k₁ k₂ α). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Unitors