Split Monoidal.Interchange into its components

[JacquesCarette]

with Interchange.Braided and Interchange.Symmetric in a sub-directory. Reformat all of it to be left/right even though it gets way beyond 80 columns; this lets one see more clearly what is being done. (Actually did manage to simplify a couple of proofs) Introduce a number of intermediate lemmas that clarify interediate steps. Naming could be improved.

This is by no means 'done', but still seems worth putting in at this point.

Q: is there a reference for the main proof?

[sstucki]

Thanks for reorganizing this @JacquesCarette!

I'll try to find a good reference. Though it might not be about these exact properties. The four-middle interchange is used where ever symmetric monoidal categories are used but seldom developed in detail (usually it's not even defined). I guess that's because the coherence laws that we prove here are all trivial consequences of the coherence theorem for symmetric monoidal categories. I don't think anyone would bother to prove them by hand, usually. But IIRC there's a paper by Fong and Spivak (could be one of the sketches) where they at least show a string-diagrammatic version of some of these laws. I'll have to check and get back to you in a few days (I'm on vacation and only have access to my phone).

[sstucki]

I dug a bit and finally found a good reference! Section 5.3 of the PhD thesis of Geoff Cruttwell states most (all?) the properties in the module, starting on p. 57 (starting with Prop. 5.3.4). It also has nice string-diagrammatic proofs.

I also want to offer two use-cases that motivated me to prove these properties. In both cases, there's a product construction that involves the interchange of a symmetric monoidal category (I hope to eventually mechanize these constructions in agda-categories).

First, there's Kelly's book on enriched categories, where the interchange is mentioned in passing when Kelly describes how to construct the composition functor for the (tensor) product of two enriched categories (see p. 12, diagram 1.17). He doesn't prove that the associativity and unit laws hold, he only says that they are "easy to verify". Easy, that is, if you have proven the coherence laws in this module... 😉

Another motivation is the proof that the 2-category of symmetric monoidal categories (SMCs), strong monoidal functors and monoidal natural transformations is itself monoidal (in fact, it has biproducts). The interchange is needed to construct the functorial action of the tensor product. Fong and Spivak give a sketch in their paper Supplying bells and whistles in symmetric monoidal categories (see Appendix A, Theorem 2.3 on p. 18).

[JacquesCarette]

Note that there might be definitions and theorems/proofs in https://arxiv.org/abs/1307.5969 of direct relevance.