Lemma whisker_r_hcomp {W X Y Z : C} {f : C⟦X,Y⟧} {g : C⟦Y,Z⟧} (k₁ k₂ : C⟦Z,W⟧) (α : k₁ ==> k₂) : rassociator _ _ _ o (α ▻ g ∘ f) = (α ▻ g) ▻ f o rassociator _ _ _. Proof. use vcomp_move_R_Mp. { is_iso. } cbn. rewrite <- vassocr. use vcomp_move_L_pM. { is_iso. } cbn. symmetry. apply @lwhisker_lwhisker. 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.