proposition: Lemma left_unitor_naturality {C : prebicategory} {a b : C} (f g : a -1-> b) (alpha : f -2-> g) : whisker_left (identity1 _) alpha ;v; left_unitor g = left_unitor f ;v; alpha.
proof: Proof. intermediate_path ((functor_on_morphisms (functor_composite (bindelta_pair_functor (functor_composite (functor_to_unit _) (constant_functor unit_category _ (identity1 a))) (functor_identity _)) (compose_functor a a b)) alpha) ;v;(left_unitor g)). reflexivity. intermediate_path (left_unitor f ;v; functor_on_morphisms (functor_identity _) alpha). apply (nat_trans_ax (left_unitor_trans a b)). reflexivity. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.WkCatEnrichment.prebicategory UniMath.Bicategories.WkCatEnrichment.Notations