Lemma whisker_r_natural {X Y : C} {f : C⟦X,X⟧} (η : id₁ X ==> f) (k₁ k₂ : C⟦Y,X⟧) (α : k₁ ==> k₂) : η ▻ k₂ o rinvunitor k₂ o α = (f ◅ α) o (η ▻ k₁) o rinvunitor k₁. Proof. rewrite lwhisker_hcomp, rwhisker_hcomp. rewrite !vassocr. rewrite rinvunitor_natural. rewrite <- !vassocr. apply maponpaths. rewrite lwhisker_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.