Definition bc_whisker_l {C : bicat} {X Y Z : C} {f₁ : C⟦X,Y⟧} {f₂ : C⟦X,Y⟧} (g : C⟦Y,Z⟧) (α : f₁ ==> f₂) : (g ∘ f₁) ==> (g ∘ f₂) := id₂ g ⋆⋆ α.
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.