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