# Commit 2022-04-03 00:36 e41208d8

View on Github →feat(category_theory/monoidal): define monoidal structures on cartesian products of monoidal categories, (lax) monoidal functors and monoidal natural transformations (#13033) This PR contains (fairly straightforward) definitions / proofs of the following facts:

- Cartesian product of monoidal categories is a monoidal category.
- Cartesian product of (lax) monoidal functors is a (lax) monoidal functor.
- Cartesian product of monoidal natural transformations is a monoidal natural transformation.
These are prerequisites to defining a monoidal category structure on the category of monoids in a braided monoidal category (with the approach that I've chosen). In particular, the first bullet point above is a prerequisite to endowing the tensor product functor, viewed as a functor from
`C × C`

to`C`

, where`C`

is a braided monoidal category, with a strength that turns it into a monoidal functor (stacked PR). This fits as follows into the general strategy for defining a monoidal category structure on the category of monoids in a braided monoidal category`C`

, at least conceptually: first, define a monoidal category structure on the category of lax monoidal functors into`C`

, and then transport this structure to the category`Mon_ C`

of monoids along the equivalence between`Mon_ C`

and the category`lax_monoid_functor (discrete punit) C`

. All, not necessarily lax monoidal functors into`C`

form a monoidal category with "pointwise" tensor product. The tensor product of two lax monoidal functors equals the composition of their cartesian product, which is lax monoidal, with the tensor product on`C`

, which is monoidal if`C`

is braided. This gives a way to define a tensor product of two lax monoidal functors. The details still need to be fleshed out.