proposition: 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: Proof. use vcomp_move_R_Mp. { is_iso. } cbn. rewrite <- vassocr. use vcomp_move_L_pM. { is_iso. } cbn. symmetry. apply @lwhisker_lwhisker. 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