proposition: Lemma bc_whisker_l_id₂ {C : bicat} {X Y Z : C} (f : C⟦X,Y⟧) (g : C⟦Y,Z⟧) : g ◅ (id₂ f) = id₂ (g ∘ f).
proof: Proof. apply id2_rwhisker. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat