proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Unitors