proposition: Lemma μ_1_is_instance_of_left_unitor : μ_1 = lu^{Mon_V}_{gh}.
proof: Proof. apply pathsinv0, (mfbracket_unique(Z:=I_{Mon_PtdV})). split. - cbn. unfold μ_0. rewrite monoidal_leftunitornat. apply cancel_postcomposition. apply pathsinv0, unitors_coincide_on_unit. - etrans. { apply cancel_postcomposition. apply pointedtensorialstrength_preserves_unitor. apply lineator_preservesunitor. } cbn. apply pathsinv0, monoidal_leftunitornat. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.CoproductsInActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects