fact: Definition make_mnd_actegory (V : category) (Mon_V : monoidal V) (C : category) (M : Monad C) (Act : actegory Mon_V C) (Ml : lineator_lax Mon_V Act Act M) (ηlinear : is_linear_nat_trans (identity_lineator_lax Mon_V Act) Ml (η M)) (μlinear : is_linear_nat_trans (comp_lineator_lax Mon_V Ml Ml) Ml (μ M)) : mnd (actbicat Mon_V).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Preservation UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Examples.StructuredCategories UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.Examples.EndoMap UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax UniMath.Bicategories.DisplayedBicats.Examples.Prod UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats UniMath.Bicategories.Monads.Examples.MonadsInBicatOfCats UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.Bicategories.MonoidalCategories.BicatOfActegories