fact: Definition bc_whisker_r {C : bicat} {X Y Z : C} {g₁ : C⟦Y,Z⟧} {g₂ : C⟦Y,Z⟧} (β : g₁ ==> g₂) (f : C⟦X,Y⟧) : (g₁ ∘ f) ==> (g₂ ∘ f) := β ⋆⋆ id₂ f.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat