[WIP] Commutative Monad

[Reijix]

Adding commutative monads (see #402 also).

First I've added the notion of RightStrength to Categories.Monad.Strong, then CommutativeMonad is defined as in nlab, i.e. a (left) strong monad on a symmetric monoidal category, where the left strength and the induced right strength commute.

I'm currently stuck on the proof that the induced strength is actually strong (Categories.Monad.Strong.Properties), any help would be much appreciated.

[JacquesCarette]

Happy to help - I think the easiest way for me to do so would be if you give me access to your fork.

[Reijix]

Happy to help - I think the easiest way for me to do so would be if you give me access to your fork.

Ah I thought people could just add onto this PR, I've added you now.

[JacquesCarette]

Maybe if my git-fu was stronger? It clearly says above

Add more commits by pushing to the comm-monad branch on Reijix/agda-categories.

I know that one other way to deal with this is for me to merge your branch into a branch on here, instead of on master.

[JacquesCarette]

I've given it a try, and got stuck as well. I have a partial proof plan (i.e. I managed to get to where I could apply strength-assoc), but reshaping everything to get to the end goal escapes me. I have a hunch that I need to apply the hexagon laws a couple of times. I will try again later. Would you be fine if I asked for some help / references on the category theory Zulip?

I could also push my (very partial) attempt, but I'm not sure it is worthwhile.

[Reijix]

Asking for help sounds good! My feeling has also been that using the hexagon laws at appropriate places should solve it, but I can't figure out where.

[JacquesCarette]

There are 2 'clear' spots in my attempt where the hexagon laws can be applied. Unfortunately what comes out the other end does not feel "closer" to solving the problem, although it does uncover more opportunities for shuffling things around.

I've asked on Zulip.

[JacquesCarette]

Recording the help that I got:

1. Nathanael Arkor said "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}^{\mathsf{rev}}$ (essentially by definition). A symmetric monoidal category satisfies $\mathcal{C} ≅\mathcal{C}^{\mathsf{rev}}$ , and this isomorphism is monoidal. Your statement should follow from the combination of these observations.
2. Mike Shulman added "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. If the same difficulty does pop up anywhere, I would expect it to be in the proof that strong monads transfer across monoidal isomorphisms."

[JacquesCarette]

So I'm going to start a new branch on here to test out these ideas, basically because 1/2 of it is independent of Strength and would be useful to have regardless.

[sstucki]

With the hint that a right strength is a left strength in $\mathcal{C}^{\mathsf{rev}}$, I've managed to find a diagrammatic proof of strength-assoc'. That seems to be the blocker, right?

I don't have time to implement the proof in Agda right now, but I'm happy to share my drawings if someone else wants to give it a go. I'm afraid this will require a non-trivial amount of fiddling with isos to get the hexagon law into the right shape(s) for in the diagrams though. (This seems to be a recurring pain when working with monoidal categories. That half-finished monoid solver we have somewhere in a PR would have come handy here. 😉)

[JacquesCarette]

Yes, that is the missing part. Please do share your drawing!

There are a few more shapes of hexagon in the library, but I'd be happy to add more.

[sstucki]

OK, here are the drawings:

The lower diagram is the core proof: it starts from associativity of the left strength (the central "pentagon") and then "reverses" the order of the monoidal products in the five corners using braiding. Then the strengths forming the top and bottom of the center are pushed out via naturality diagrams and the fact that the left and right strengths commute with braiding (this follows directly from the definition of the right strength and the fact that the braiding is self-inverse - you may want to factor it into a lemma or two).

To finish the proof, one has to show that the left and right edge of the lower diagram are (the inverse of) the associator. That's what the upper diagram proves via repeated use of the hexagon law. This is the bit that I expected to be most cumbersome to translate to Agda. It should certainly be made a lemma because it's used on both sides of the lower diagram.

I hope I didn't miss anything.

[sstucki]

It seems there hasn't been any progress on this, so I'll giving it a go now.

[JacquesCarette]

Thanks. Do let us know of partial progress, as I have time this weekend to push on this.

[sstucki]

OK, I managed to prove strength-assoc for the induced right strength now.

I refactored the module a bit to make the new proofs more readable but left most of the existing proofs as they were (modulo white space cleanup, etc.) I also left FIXME comments suggesting some further ways to clean things up.

There is still an open goal: RightStrength⇒Strength. We could probably prove this quite straight-forwardly (but tediously) now, since everything is symmetric. But it might be cleaner to use this symmetry explicitly: show that a right strength in $\mathcal{C}$ is a left strength in $\mathcal{C}^\mathsf{rev}$ and vice-versa, then use that to derive the that the right strength induces a left strength from the existing proof that a left strength induces a right strength.

I think that would be more fun and also more insightful. The only issue is that we'd need to mechanize $\mathcal{C}^\mathsf{rev}$ first, but that might be an interesting exercise. How far did you get with that @JacquesCarette?

[sstucki]

Interesting observation: the proof that a left strength $\sigma$ for $T$ in $\mathcal{C}$ induces a right strength $\tau$ for $T$ in $\mathcal{C}$ seems to work even if $\mathcal{C}$ is merely braided (as opposed to symmetric), as long as one defines $\tau$ as $\tau = T B^{-1} \circ \sigma \circ B$.

[sstucki]

@JacquesCarette, I have mechanized the definition of $\mathcal{C}^\mathsf{rev}$ now, including proofs that reversing the product preserves braidedness and symmetry. I guess I should open a separate PR for this, or is it OK to push it to this PR for now?

[JacquesCarette]

Wow, thanks! Adding those definitions to this PR is fine, they are sufficiently related.

[sstucki]

OK, all goals solved and make test passes on my machine. 🥳

The PR definitely still needs some cleanup (see FIXMEs) but it's getting late here, so I'll stop for today.

I put the definition of reverse categories in a separate commit, so it could easily be cherry-picked or rebased into a separate branch, if you decide the PR is getting too big.

[sstucki]

@Reijix, would you like me to wrap this up, or do you prefer to put on the finishing touches yourself?

@JacquesCarette, I think the PR is ready for review. Would you mind having a look to see if there's anything that needs fixing (beyond the small FIXMEs)?

[JacquesCarette]

It's on my pile. The week started out fine, and then kind of exploded on me.

[sstucki]

Sure, no rush. Bon courage!

[Reijix]

@sstucki, you can finish it, I'm happy with the state this PR is in now. Thanks for finishing the proofs!

[sstucki]

OK, I've cleaned up the remaining FIXMEs and I think the code is good to go.

But the PR now has quite a few commits, and I forgot what the policy is re. squashing/cleaning up the commit history. Do we usually merge PRs as they are or rebase the history into a few self-contained commits?

@JacquesCarette, any preferences?