The really sad part is that the condition on the monad T that gives the structure of the context is that it needs to preserve pullbacks (and so too the natural transformations η and μ in the monad need all their naturality squares to be pullbacks) and the "free commutative monoid" monad doesn't have this property. So naïvely setting up, say, bunched logic in terms of a monad that takes the free structure with two commutative monoids, one of them with contraction and weakening, looks like a total no-go. On the other hand,

*something*about symmetry is obviously workable, since operads and multicatories equipped with a symmetry "on the outside" are totally well-understood. It's troubling that one can't independently sneak symmetries into things by just adding (non-strongly regular) equational laws.