Lemma whisker_l_natural {X Y : C} {f : C⟦X,X⟧} (η : id₁ X ==> f) (k₁ k₂ : C⟦X,Y⟧) (α : k₁ ==> k₂) : k₂ ◅ η o linvunitor k₂ o α = α ▻ f o (k₁ ◅ η) o linvunitor k₁. Proof. rewrite lwhisker_hcomp, rwhisker_hcomp. rewrite !vassocr. rewrite linvunitor_natural. rewrite <- !vassocr. apply maponpaths. rewrite rwhisker_hcomp. rewrite <- !interchange. rewrite !id2_right, !id2_left. apply idpath. 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.