Is there a non-symmetric monoidal monad?
- ️Thu Mar 07 2024
Recall that a monoidal monad on a monoidal category $(\mathcal{C}, \otimes, I)$ is a monad $(M, \eta, \mu)$ on $\mathcal{C}$ such that $M$ is also equipped with the structure of a lax monoidal functor in a way that makes $\eta$ and $\mu$ monoidal natural transformations.
The structure of a monoidal monad on a given monad is equivalent to the structure of a commutative monad: a pair of a left and right monad strengths $(\sigma, \tau)$ such that the two induced lax monoidal structures agree: $$\mu \circ M\sigma \circ \tau = \mu \circ M\tau \circ \sigma : MA \otimes MB \to M (A \otimes B)$$
If furthermore $\mathcal{C}$ is a symmetric monoidal category with $\beta : A \otimes B \to B \otimes A$, then a monoidal monad is symmetric if the underlying monoidal functor is, and a strength is symmetric if $\tau = M\beta \circ \sigma \circ \beta$. Over the above equivalence, the property of being a symmetric monoidal monad is equivalent to the property of being a symmetric commutative monad (that is, a monad with a commutative symmetric strength). [1]
Question: is there a monoidal monad, on a symmetric monoidal category, that is not symmetric?
Equivalently: is there a commutative monad, on a symmetric monoidal category, whose left and right strengths are not related by the braiding?
On the Lambek Calculus with an Exchange Modality claims (lemma 9) to have a non-symmetric monoidal monad, but doesn't actually prove that it's non-symmetric — only that it need not be. The paper then concludes that the monad isn't commutative, which seems odd: being commutative is a property of a strength, not a monad, and since the monad is monoidal there is some commutative strength on it — just not the one you'd like. This all makes me wonder if I should trust the claim at all.
There is also a thread of people failing to answer this question at the nForum.
[1]: this is a decomposition of a well-known result by Kock; see 1Lab for an Agda formalisation of these claims.