Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Left/Right Monad strength over symmetric monoidal category

Jacques Carette (Jan 03 2024 at 18:05):

We (Leon Vatthauer and I) are trying to formalize that having a left-strong monad is equivalent to having a right-strong monad when over a symmetric monoidal category. It's all easy enough, except for associativity, which has us both befuddled.

So we're looking for some reference(s) that has a sufficiently detailed proof (here, we're expecting a giant commutative diagram, likely with multiple uses of the hexagon laws) that we can formalize. Of course, if someone's already formalized this, we'd love to look at that too.

Simon Burton (Jan 03 2024 at 18:28):

did you try using string diagrams?

Jacques Carette (Jan 03 2024 at 18:30):

I am one of those rare people for whom string diagram make things more obscure. And, because of that, if someone gave me one such thing, I would be at a massive loss as to how to translate it to an equational proof!

Simon Burton (Jan 03 2024 at 18:31):

ok well i guess you are letting me off the hook then :-)

Jacques Carette (Jan 03 2024 at 18:32):

Well, maybe a tag-team effort is needed, to go string diagram -> commutative diagram -> equational proof...

Mike Shulman (Jan 03 2024 at 18:34):

Jacques Carette said:

I am one of those rare people for whom string diagram make things more obscure.

Kudos for admitting that! I'm halfway between; some things I find easier with string diagrams, but other things I have to translate back into commutative diagrams to make sense of. Some people seem to think that string diagrams are always better, but I think different notations can each have their strengths and weaknesses. And that it's entirely reasonable for individual people to prefer one notation over another.

Nathanael Arkor (Jan 03 2024 at 18:45):

Perhaps a more abstract proof might be simpler to formalise. A right-strength with respect to a monoidal category $\mathcal C$ is equivalently a left-strength with respect to $\mathcal C^{\text{rev}}$ (essentially by definition). A symmetric monoidal category satisfies $\mathcal C \cong \mathcal C^{\text{rev}}$, and this isomorphism is monoidal. Your statement should follow from the combination of these observations.

Jacques Carette (Jan 03 2024 at 18:52):

Certainly worth a try. Wonder if Agda's going to cooperate into believing that this is indeed the case. That might end up shuffling the deck chairs around (i.e. the proof of 'this isomorphism is monoidal' will resurface the same difficulty.)

Mike Shulman (Jan 03 2024 at 18:53):

I would expect it to simplify things, since at that point the monad and the strength wouldn't be part of the argument any more, only the monoidal structure.

Mike Shulman (Jan 03 2024 at 18:54):

If the same difficulty does pop up anywhere, I would expect it to be in the proof that strong monads transfer across monoidal isomorphisms. (If you use Cubical Agda, of course, that part would be trivial!)

Jacques Carette (Jan 03 2024 at 19:08):

(Sunk cost fallacy: I have too much invested in agda-categories to switch to 1lab wholesale, even though I am using it in joint work). It's definitely worth trying, as it would indeed 'factor' the issues into different pieces.