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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.