fact: Definition odot_x_otimes_y_functor : (A ⊠ Mon_V) ⊠ Mon_V ⟶ A := functor_composite (precategory_binproduct_unassoc _ _ _) (functor_composite (pair_functor (functor_identity _) tensor) odot).
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal