Lemma μ_1_is_instance_of_left_unitor : μ_1 = lu^{Mon_V}_{gh}. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Import BifunctorNotations. Import MonoidalNotations.