Monoidal Natural Transformation

definition

A monoidal natural transformation between (lax) monoidal functors $(F,\phi ),(G,\psi ):\mathcal{C}\to \mathcal{D}$ is a Natural Transformation $\alpha :F\to G$ compatible with the coherence maps:

$${\alpha }_{c_1\otimes c_2}\circ {\phi }_{c_1,c_2}={\psi }_{c_1,c_2}\circ ({\alpha }_{c_1}\otimes {\alpha }_{c_2}),{\alpha }_I\circ {\phi }_I={\psi }_I.$$

Monoidal categories, monoidal functors and monoidal natural transformations form the 2-Category $\mathbf{MonCat}$.

Sources: DaoFP §14.9 (“The category of monoidal categories with monoidal functors as arrows is called MonCat. In fact it’s a 2-category, since one can define structure-preserving natural transformations between monoidal functors”); 7 Sketches §6.4 (morphisms of decoration functors induce hypergraph functors between decorated cospan categories), §4.4.

• Between applicative functors a monoidal natural transformation is an applicative morphism: t :: forall a. f a -> g a with t (pure x) = pure x and t (u <*> v) = t u <*> t v.
• Between monoidal monotone maps there is at most one, so the preorder version is trivial.
• A Natural Transformation between functorial semantics of a Prop (symmetric monoidal functors $\mathcal{P}\to \mathbf{Set}$) is a homomorphism of models, e.g. a monoid homomorphism between models of the theory of monoids.

Haskell

-- an applicative morphism = monoidal natural transformation between lax monoidal endofunctors
maybeToList :: Maybe a -> [a]                       -- t (pure x) = pure x ; t (u <*> v) = t u <*> t v
maybeToList Nothing  = []
maybeToList (Just a) = [a]