Symmetric Monoidal Categories

[Alizter]

@jdchristensen here is a definition of symmetric monoidal category together with a partially finished twist construction. By this I mean using a swap and twist map we get associativity, triangle and hexagon with appropriate assumptions. Only the pentagon is left. Pentagon is done.

Note that this cannot be applied to JoinAssoc as is as there is a difference between fmap11 and functor_join. This might be a good reason to redefined bifunctor like I suggested in #1883. It's not too difficult to wrangle it to fit however.

• finish cartesian symmetric monoidal structure
• optimize proofs in Monoidal.v
• split bifunctor work into another PR
• refactor twist class? (didn't turn out to be easy)
• Use in joins?
• modify long form notation of $==.

[Alizter]

I've wrangled with the pentagon proof, cancelling things where possible and making sure no naturality squares remain. The goal I've ended up with looks like:

    ((τ (a ⊗ b) d c ∘ σ (d ⊗ c) (a ⊗ b)) ∘ τ a (d ⊗ c) b) ∘ a ⊗R σ b (d ⊗ c)
$== ((d ⊗R σ c (a ⊗ b) ∘ d ⊗R τ a c b) ∘ τ a d (c ⊗ b)) ∘ (a ⊗R (d ⊗R σ b c) ∘ a ⊗R τ b d c)

I'm not sure if it can be simplified further. The double functor application (a ⊗R (d ⊗R σ b c) looks like it might commute by naturality of twist and go somewhere, but I haven't been able to make progress on that. This might be the pentagon for twist that we are looking for, but it doesn't look great. I still feel like there is more that could be done here.

[jdchristensen]

I'll be taking a look at this PR sometime soon. Also, this paper https://arxiv.org/abs/2404.08163 just appeared, and I wonder if anything from it can be used in this context.

[Alizter]

I'll be taking a look at this PR sometime soon. Also, this paper arxiv.org/abs/2404.08163 just appeared, and I wonder if anything from it can be used in this context.

Yes I saw that. I'm aware of some of the work from before. They have a nice way of visualising their proof calculus in coq-lsp as string diagrams which is what that work is based on.

ping @bhaktishh, how much work would it take to adapt the visualizer for Coq-HoTT? The tldr is that we have a library that doesn't use the coq standard library. I'm wondering if we can write a small plugin that can directly interface with the vscode extension and render diagrams in our categories. My main concern is that the visualizer described in the new paper pulls in a lot of prerequisites on opam so I'm wondering if anything more lightweight is possible.

[bhaktishh]

Thanks for the ping! Looping in @lczielinski @wjbs @adrianleh @caldwellb here for discussions about the library itself.

With respect to the visualizer, what prerequisites on opam are you worried about? The visualizer itself should work with coq-lsp as its only dependency. The library alone has no dependencies, it is just the examples that are implemented using other, larger libraries -- are these what you are referring to?

With respect to adapting for Coq-HoTT, it depends -- are you able to instantiate the typeclasses in the vicar library? If yes, then you're automatically able to make use of the visualization. If not, we can come up with some translation from your syntax to vicar's, as in theory they should be compatible.

[Alizter]

@bhaktishh Thanks for the explanation. I had a quick look at https://github.com/inQWIRE/ViCaR/tree/main/ViCaR/Classes and it seems the definition for the classes that you've chosen are the setoid based ones. In that case, I don't see any issue adapting our "wild cat" definitions to instantiate those. I'll create an issue so that we can track progress with setting this up. I might not have the time to do it now, but its definitely cool to see that it might work.

I've created:

• Use ViCaR to visualize terms in monoidal categories #1922

so that we can continue the discussion there, as this PR is not immediately relevant.

[jdchristensen]

I left a couple of comments, and will keep reviewing this.

[jdchristensen]

@Alizter Can I push a couple of cleanups to this? If you've made changes locally, you can push first.

[Alizter]

@jdchristensen Go ahead!

[jdchristensen]

@Alizter, I'm not sure what's causing the build errors.

[Alizter]

Completely bizarre. Your changes work fine locally, I have no idea what is going on. I'll try merging the master branch and see if being out of date was the problem.

[Alizter]

Yeah, it was due to the difference in the base. I get the same error when building locally now.

[Alizter]

In Monoidal.v a Basics.Tactics was removed in the requires. Adding it back fixes everything.

[Alizter]

I've renamed Symmetor to Braiding and fixed the axioms. Having a morphism rather than equivlaences actually simplified some proofs in a few places.

I also started the hexagon consisting of twists. No idea if it's possible, but I've created some lemmas for moving twists and friends around so that I can attack it with the other hexagon. I'll continue tomorrow.

[Alizter]

I was thinking that the Greek letter notations would be a temporary addition, however it is perhaps useful to include them in a module in this file. The proofs are quite unreadable without some abbreviation.

[Alizter]

@jdchristensen I've done some reorganisation. Moved things around. Added many more comments explaining the journey. And also cleaned up some of the proofs. I haven't revised the pentagon yet as I'm still trying to workout what kinds of form we want the 9-gon in.

[Alizter]

When this PR is a bit more ready, I will split off the material on bifunctors in a separate PR so that we can better review it.

[Alizter]

@jdchristensen I've been adding a lot of lemmas and notations to make the reasoning in the pentagon easier. I've come up with a shorter more readable proof that the pentagon (of associators) "reduces" to a 9-gon of twists. It's stated after the first pentagon proof. I think we should go ahead and make this the main proof and ask for the 9-gon as a piece of data.

[jdchristensen]

I don't like that form of the 9-gon, which expresses a homotopy between maps a ⊗ (b ⊗ (d ⊗ c)) $-> ((a ⊗ b) ⊗ c) ⊗ d. In the type of maps, it's hard to remember that you have to reverse the way the objects are associated and swap c and d, and the two maps themselves aren't obvious.

As we discussed elsewhere, there's a fairly natural 9-gon that you can write down, expressing a homotopy between maps a ⊗ (b ⊗ (c ⊗ d)) $-> c ⊗ (d ⊗ (a ⊗ b)). Here, the parentheses are the same, and you only have to remember that it involves the permutation (1,3)(2,4). One of the maps expresses that permutation as a product of transpositions of adjacent elements, (2,3)(3,4)(1,2)(2,3), keeping the parenthesization the same. The other map is obtained by associating the domain and codomain as (a ⊗ b) ⊗ (c ⊗ d) and (c ⊗ d) ⊗ (a ⊗ b) and using the braiding at the top-level; when you unfold the associator in terms of the braiding and the twist, two of the braidings cancel, and you are left with five maps. This is something I'd be able to generate, just remembering that the goal is the permutation (1,3)(2,4).

I'm pretty sure this more memorable 9-gon is the one that came up in one version of your first proof (possibly with permuted letters).

(I'm also not sure what your comment "2 extra sides nested in the left making it an 11-gon" in the proof means.)

[Alizter]

(I'm also not sure what your comment "2 extra sides nested in the left making it an 11-gon" in the proof means.)

Goal looks like (with new notation):

σ d ((a ⊗ b) ⊗ c)
∘ τ (a ⊗ b) d c
∘ σ (d ⊗ c) (a ⊗ b)
∘ τ a (d ⊗ c) b
∘ a ⊗R σ b (d ⊗ c)
 ~[a ⊗ (b ⊗ (d ⊗ c)) $-> ((a ⊗ b) ⊗ c) ⊗ d]~
 σ d ((a ⊗ b) ⊗ c)
∘ d ⊗R σ c (a ⊗ b)
∘ d ⊗R τ a c b
∘ d ⊗R (a ⊗R σ b c)
∘ τ a d (b ⊗ c)
∘ a ⊗R τ b d c

I'm just saying this is the 9-gon, but after you cancel σ d ((a ⊗ b) ⊗ c).

I'll try and understand how we can get the other 9-gon.

[Alizter]

I've managed to get:

d ⊗R σ (a ⊗ b) c
∘ τ (a ⊗ b) d c
∘ σ (d ⊗ c) (a ⊗ b)
∘ τ a (d ⊗ c) b
∘ a ⊗R σ b (d ⊗ c)
 ~[a ⊗ (b ⊗ (d ⊗ c)) $-> d ⊗ (c ⊗ (a ⊗ b))]~
 d ⊗R τ a c b
∘ d ⊗R (a ⊗R σ b c)
∘ τ a d (b ⊗ c)
∘ a ⊗R τ b d c

I believe this is acceptable?

[jdchristensen]

Yes, that looks good! When stated as an axiom, I'd swap the names of c and d, so they appear in order, but you can of course apply the axiom here with the variables reversed.

[Alizter]

I'm not sure if we want to keep these. I think we probably want modify the scope as it is really only a local one. Call it twist_monoidal_scope. It's unclear if the general notation for monoidal categories is useful.

[jdchristensen]

I think there's a good chance these three will be useful to others.

[Alizter]

I've just pushed a commit partially showing that cartesian products and terminal objects give a symmetric monoidal category. I've finished the triangle and pentagon, didn't have time to look at hexagon yet. Notably it shows that we should streamline some of the assumptions as I needed to repeat arguments in a few places.

Also I don't know if it's particularly useful, but cocartesian categories could also be shown to exist. That way, pointed categories with products and coproducts are cartesian and cocartesian. Then by Eckmann-Hilton products and coproducts commute yadayada.

[jdchristensen]

I've just pushed a commit partially showing that cartesian products and terminal objects give a symmetric monoidal category.

Why didn't you use the twist/braiding approach?! It should definitely be easier, and the associator for products is already defined in terms of the twist and braiding, so everything is set up to use the material already in this PR...

[Alizter]

@jdchristensen this is using the twist approach. Have I missed something?

[jdchristensen]

@jdchristensen this is using the twist approach. Have I missed something?

Sorry, I just read it too quickly! I saw how long the proof of the pentagon was and missed the first line. I'm surprised at how tedious that is, since you "just" need to check that the components of those maps agree. I wonder if there are some lemmas that can be factored out.

[Alizter]

@jdchristensen I will spend some more time refactoring the proof today. I think we can make the twist construction easier to use as currently there are quite a lot of hypotheses that need to be repeated.

[Alizter]

@jdchristensen I bundled up the swap assumptions so that they can be more easily shared. It does however mean the dependencies may be a bit coarser. Should I revert that and try something looser or do you think its ok?

Also, we could do something similar for twist.

[jdchristensen]

I think it seems smoother with the braiding bundled up like this. I haven't thought through how it would look with the twist bundled.

[Alizter]

@jdchristensen I will rebase and squash. Is that alright with you?

[Alizter]

Or actually nevermind, I'll just merge the master branch for now and leave the squashing and rebasing for later.

[Alizter]

I attempted to make a "twistor" class however stating the naturality condition is not easy since we are missing a bifunctor instance that populates Is0Functor (fun '(x, y) => F y x) for a bifunctor F. I'm not particularly keen on adding this, so I think the twist stuff is better left as is.

[Alizter]

I've marked this as ready-for-review as I have finished everything I wanted to prove. After the review is finished, I think we should squash the commit history before merging.

[Alizter]

I tweaked the long $== notation. It now prints like this:

braid d ((a ⊗ b) ⊗ c)
∘ twist (a ⊗ b) d c
∘ braid (d ⊗ c) (a ⊗ b)
 $==
 braid d ((a ⊗ b) ⊗ c)
∘ d ⊗R braid c (a ⊗ b)
∘ d ⊗R twist a c b
∘ d ⊗R (a ⊗R braid b c)
∘ twist a d (b ⊗ c)
∘ a ⊗R twist b d c
∘ a ⊗R braid (d ⊗ c) b
∘ twist (d ⊗ c) a b
:> ((d ⊗ c) ⊗ (a ⊗ b) $-> ((a ⊗ b) ⊗ c) ⊗ d)

[jdchristensen]

Isn't this just an example of a general result about moving an equivalence to the other side?

[Alizter]

Unfortunately not. The issue is that twist ... is not definitionally the same as cate_fun (twiste ...). This means in order to apply a lemma about moving equivalences you have to package and unpackage the equivalence. Therefore needing a lemma like this again to package up that reasoning. You might then ask, what if we had "catie" versions of the movement lemmas, and I tried this. The issue there is that we have no equation extracting the inverse from catie_adjointify so I couldn't relate twist^-1$ as an inverted CatIsEquiv to twist. This is why I opted to just have the specialised lemmas.

[jdchristensen]

I think we should be able to figure out a way to make this kind of lemma work (maybe with some tweaks to HasEquivs), but that can happen as a separate PR. Feel free to merge. Thanks for the great work!

[jdchristensen]

This LGTM. My only hesitation is that there are a lot of specialized lemmas. It would be great if many of them could be replaced with a smaller number of general purpose lemmas. I indicated one as an example, but my comment applies more generally. Still, it's fine with me if you want to merge it as is. And I think it makes sense to squash it. (BTW, I'll be offline for a few days on a short vacation.)

[Alizter]

@jdchristensen I've squashed everything. I think we should merge and I will go back to working on additive categories.