Added a link to an MSE answer with an example of a non-symmetric monoidal monad: https://math.stackexchange.com/a/4877915/501886

]]>Regarding my last question, the paper On the Lambek Calculus with an Exchange Modality claims (results 9-12) to have a monad on a symmetric monoidal category that is monoidal, but not symmetric monoidal, and concludes that it is not commutative.

In light of the finer understanding of Kock’s result, this would mean that the strengths inherited from the monoidal monad are not related by the braiding, although they do make the monad commutative. I am not sure if the claim in the paper is correct though.

EDIT: in fact it doesn’t seem like it shows the monoidal monad isn’t symmetric, only that it need not be. So, not exactly a counter-example.

]]>I’ve edited proposition 2.7 to

- remove the assumption of a
*closed*monoidal category, and - separate the equivalence into two steps, first “monoidal ≃ commutative” in an arbitrary monoidal category and then “symmetric monoidal ≃ symmetric strength” on top of that. This had been a source of confusion for me and at least one other person, as the article seemed to be claiming that commutative monads were equivalent to both monoidal monads and symmetric monoidal monads.

And added a link to an Agda formalisation of the updated claims (own work).

I guess to make the picture 100% clear one would need to add an example of a non-symmetric monoidal monad, or equivalently a non-symmetric commutative strength. I am not sure if those exist.

]]>Have spelled out (here) the definition of a monoidal monad in components.

]]>added pointer to:

- Jean Goubault-Larrecq, Slawomir Lasota, David Nowak,
*Logical Relations for Monadic Types*, Mathematical Structures in Computer Science,**18**6 (2008) 1169-1217 [arXiv:cs/0511006, doi:10.1017/S0960129508007172]

here and elsewhere

]]>Made a lot of trivial cosmetic edits to wording and formatting of the subsection “Relation to commutative strong monads”

]]>have added (here) the following proposition, with pointer to Kock (1972), Thm. 2.3:

For a monad $T$ on (the underlying category of) a symmetric closed monoidal category, there is a bijection between the structure on $T$ of a:

]]>

have tried to bring more logic into the section outline:

Now there is a section “Properties” with three subsections, the first of which is “Relation to commutative strong monads”.

The claims in this subsection probably have canonical references, but essentially none are given currently.

]]>Add link to PDF for the paper “Commutative monads” by Lindner.

]]>Yes, that is the tensor product I meant: the one induced by Day convolution from the monoidal structure of the cube category.

Hmm, I thought that you were only using the symmetric structure of the underlying symmetric monoidal category to define that square, not the one on algebras? My feeling was that *if* that square commutes, it will force the monoidal structure on algebras to be symmetric, but I haven’t gone through the details.

One thing that I think is true is that the only way to get an example would be to have left and right strengths where the right strength is *not* compatible with the symmetric structure of the underlying symmetric monoidal category, but where one still has the necessary compatibility between the strengths to have a commutative monad (as defined in the non-symmetric setting). I think there should be such examples (I see no reason for the compatibility between strengths to force that the right strength comes from the symmetric structure), but if my idea about looking at non-symmetric-ness of the tensor product on algebras is no good, then I’m not sure where to look for them!

Hmm, I think the square can only be *defined* if the tensor product is symmetric (or at least braided) since the vertical maps are meant to be braiding maps. Anyway, which non-symmetric tensor product are you referring to? A kind of substitution tensor product?

EDIT: I assume that you mean the convolution tensor product on presheaves on this cube category. That’s indeed not symmetric.

]]>Interesting question! Do cubical sets perhaps provide an example? I’d guess that they can be viewed as algebras for some monoidal monad on the category $\mathsf{Set}^{\mathbb{N}}$ (with symmetric monoidal structure given by levelwise product), or something like that (thinking of each element of $X(n)$, for some $n \in \mathbb{N}$, as a free-standing $n$-cube), with the monoidalness of the monad inducing the usual tensor product of cubical sets; but this tensor product is not symmetric, and I think this would necessitate that the square you mention does not always commute.

]]>Does anybody know of an example of a monoidal monad on a symmetric monoidal category, where the monad itself is not symmetric, i.e. the square

$\begin{matrix} TA \otimes TB &\to& T(A\otimes B)\\ \downarrow && \downarrow\\ TB \otimes TA &\to& T(B\otimes A)\\ \end{matrix}$doesn’t necessarily commute?

I thought that André Joyal mentioned such a monad at a CT talk about the Dold Kan correspondence and Tom Leinster blogged about it, but although I found the blogpost here, it doesn’t mention any such monad.

Does anybody happen to remember the monad in question, or another non-symmetric monoidal monad on a symmetric monoidal category?

]]>It looks like the proof is actually for the second composite.

tgeng

]]>Attempt to better summarize the situation at the beginning of the article.

]]>Added monoidal structure on Kleisli category

]]>Added functoriality of correspondence.

]]>Started page about tensor product of algebras over a commutative monad.

]]>Excellent, thanks!

]]>Started an article on monoidal monad. An earlier redirect had sent it over to Hopf monad which is something that Zoran was working on, but I think it deserves an article to itself, with discussion of the relation to commutative monads, etc. (which I have started).

]]>