proposition: Lemma is_mon_nat_trans_underlying_inserter_1cell_pr1 (q : inserter_cone Fm Gm) : is_mon_nat_trans (comp_fmonoidal (fmonoidal_underlying_inserter_1cell q) (dialgebra_monoidal_pr1 (pr2 Fm) (pr12 Gm))) (pr12 (inserter_cone_pr1 q)) (pr1 (inserter_1cell_pr1 (underlying_inserter_1cell q))).
proof: Proof. split. - intros x y. cbn. unfold projection_preserves_tensordata, fmonoidal_preservestensordata. rewrite id_left. rewrite id_right. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, tensor_id_id. } apply pathsinv0, id_left. - red. cbn. unfold projection_preserves_unit, fmonoidal_preservesunit. rewrite id_left. apply id_right. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Categories.Dialgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.Limits.Inserters UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Examples.MonoidalDialgebras UniMath.CategoryTheory.Monoidal.Displayed.MonoidalFunctorLifting UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.Bicategories.MonoidalCategories.BicatOfWhiskeredMonCats UniMath.Bicategories.Limits.Examples.BicatOfCatsLimits