consider adding a symmetric version of enriched category thoery

[HuStmpHrrr]

I find it could be more useful to implement a portion of enriched category theory which is enriched in a symmetric monoidal category. one sweet spot is that opposites exist and that many categories are in fact symmetric monoidal, e.g. CCC, which is often seen in programming languages.

[sstucki]

Good idea. That was my plan, actually. I just haven't had time yet to do it.

This corresponds to Section 1.4 of Kelly's book. (The section after that deals with closed/cartesian-closed enriched categories.)

[JacquesCarette]

If we go there (which I'm in favour of), we'll probably also want to enrich over skew monoidal categories as well (introduced in https://arxiv.org/abs/1201.4981 but then used in various places like https://arxiv.org/abs/1708.06088 and many more , some of which are of direct interest to me).

In other words, there is a naming issue to solve. Will this end up multiplying? Or are there just 3 cases? In the latter situation, then Enriched, SymmetricEnriched and SkewEnriched would not be entirely unreasonable. But once it gets to 4+ cases, that gets silly.

[sstucki]

In other words, there is a naming issue to solve. Will this end up multiplying? Or are there just 3 cases? In the latter situation, then Enriched, SymmetricEnriched and SkewEnriched would not be entirely unreasonable. But once it gets to 4+ cases, that gets silly.

I don't think that's a problem in practice. Currently, every module in the Enriched hierarchy is parametrized by a category V (over which things are enriched) and a proof that V is monoidal. I don't see why one could not instead parametrize a module with a proof that V is symmetric monoidal or skew monoidal for those modules that require the extra structure. These modules can still make use of the basic definitions that only require V to be monoidal. No need to duplicate anything. Or am I missing something?

(BTW. The same goes if we replace the two parameters with a single parameter V : MonoidalCategory or V : SymmetricMonoidalCategory. The downcast is still straightforward.)

[HuStmpHrrr]

there is no need to explore all cases, unless they all are worth the effort. I think the definition of symmetric monoidal category should be adjusted: there is no need to prove two hexagon identities because symmetry can derive one from another.

[sstucki]

I think the definition of symmetric monoidal category should be adjusted: there is no need to prove two hexagon identities because symmetry can derive one from another.

While that's true, I don't think it's a good idea to change the definition of symmetric monoidal categories. The current definition has the virtue of being symmetric (in a sense similar to the definition of Category including the redundant sym-assoc field). If anything, it would make more sense to add a helper record/function that allows one to define instances more easily (specifying only one of the hexagon identities) which derives the missing pieces.

More generally, I think it doesn't make sense to "optimize" definitions in this way since different, equivalent definitions may be better or worse depending on a use case. Another example that we have discussed before is that of CCCs, where the "canonical" definition is easier to implement, but also a lot less concise.

BTW. This definition is a bit off-topic. If we want to continue it, maybe it should go into a separate issue.

[HuStmpHrrr]

@sstucki you are right. I realized that too. I have pushed the modification already. actually it should be the definition of Braided that gets changed. the two hexagon identities should be dual of each other. you can see the change I made in the master branch.

[sstucki]

you can see the change I made in the master branch.

LGTM!

[sstucki]

Just re-discovered this old issue. I think many (most?) of the prerequisites to do this are now ready. It turns out some of the dependencies were rather non-trivial (e.g. the properties of the interchange in SMCs). So hopefully I'll soon be able to add the missing chapter. If someone else wants to work on it, let me know so we don't duplicate work.

[JacquesCarette]

Cool! It does seem like working over SMCs is currently trendy. And simpler. It's odd that it relies on such non-trivial properties though - that seems to be elided from textbooks.

[sstucki]

[...] It's odd that it relies on such non-trivial properties though - that seems to be elided from textbooks.

Indeed. The example I gave elsewhere is from Kelly's book (p. 12, comment below diagram 1.17):

[...] where m: (W ⊗ X) ⊗ (Y ⊗ Z) ≅ (W ⊗ Y) ⊗ (X ⊗ Z) is the middle-four interchange defined by any suitable composite of instances of a and of c. The identity element is the composite [...] and axioms (1.3) and (1.4) are easy to verify.

If I recall correctly, the "easy to verify" properties involve some of the larger proofs in the Monoidal.Interchange module (that the interchange m "commutes" with associators and unitors). The reason Kelly's says they're easy is (I think) because the string-diagrammatic versions are! But to use the machinery of string diagrams, we'd have to prove the coherence theorem for symmetric monoidal categories, which is well-known but (as far as I can tell) hard to mechanize.

[sstucki]

To be fair, Kelly's book is incredibly dense.

[JacquesCarette]

I've gotten better at taking string diagrams and translating them to combinator expressions (as an art, not as a procedure!). Are they in Geoff Cruttwell's thesis?

Also, I think the reason that the SMC coherence theorem is so hard to mechanize is that the "normal forms" aren't expressible without quotients. This is the root reason that things like Bags are not something one can easily do in MLTT. Both Nils and I have done it (independently) with Setoids, where it is very important that the witnesses of equality are data, not propositions (in this case, explicit permutations).

[sstucki]

I've gotten better at taking string diagrams and translating them to combinator expressions (as an art, not as a procedure!). Are they in Geoff Cruttwell's thesis?

Yes, at least the big one that takes up most of the interchange module (swapInner-assoc) is on p. 57 (in the proof of Prop 5.3.4) and on the following page (in the proof of the following propositions), and here's the full "proof" graphically (applying the braiding laws explicitly). All these are really just instances of the same coherence theorem for the interchange (coherence w.r.t. the associator). What's deceptive about all these diagrams is that they hide all the mindless re-association that needs to be done in an explicit proof (in two dimensions). That's where a tactic would be helpful...

Also, I think the reason that the SMC coherence theorem is so hard to mechanize is that the "normal forms" aren't expressible without quotients. This is the root reason that things like Bags are not something one can easily do in MLTT. Both Nils and I have done it (independently) with Setoids, where it is very important that the witnesses of equality are data, not propositions (in this case, explicit permutations).

That's very interesting. Do you have a link to that development? I'm still hoping that we could actually proof the coherence theorems and possibly even use them to implement tactics, like the one @TOTBWF started in #279. That draft PR contains a coherence theorem for monoidal categories (without braidings), as per the nLab definition (point 1).