Add interchange for monoidal categories

[sstucki]

In braided monoidal categories one can define an "interchange law" (or rather an interchange map) aka the "four middle interchange". This map is used in many constructions involving braided and symmetric monoidal categories and product constructions, e.g. when defining the product of two enriched categories, or when showing that tensor products can be lifted pointwise to monoidal functors. As one would expect, the interchange is a coherent iso and the hard work is not to define the interchange map itself, but to prove its coherence properties. That's what this PR does.

The PR contains some of the most tedious proofs I've ever had the misfortune to mechanize. None of the proofs are conceptually hard (or even interesting) they can all be proved in just a few steps using string diagrams. But unfortunately, we don't have support for string diagrams in the library (yet) so the only way I knew how to do it was by hand.

The resulting proofs are not pretty. Especially the one for swapInner-assoc is long and ugly. If anyone wants to have a go and try to clean it up, that'd be appreciated.

The PR contains two commits. I would usually separate these into different PRs, but in this case, the second commit, which shows that the tensor product of a monoidal category with a coherent interchange is a monoidal functor, is used as a motivation for the choice of coherence laws for the interchange (and referred to in a comment in the module introducing them). So the two really go hand-in-hand. Still, if desired, I can split the PR.

[JacquesCarette]

swap-Inner-assoc is indeed a real monster. Splitting it up in a series of lemmas seems like the right thing to do. What they should be is less clear. I see you've already got some divisions in there (nice), but there's likely more patterns too.

No problem about twinning these commits: they really are deeply related. I'll do a more formal review later - it was mostly very clean. There were just a couple of naming things that I'd like to tweak, beyond finding ways to make those large tedious proofs less so. [I see you use the push/pull combinators a lot already, so at least the assoc-munging aspects are already under control, which is nice. Lets one see the next level of patterns.]

[sstucki]

swap-Inner-assoc is indeed a real monster. Splitting it up in a series of lemmas seems like the right thing to do.

Yes, that was my first intuition too. The challenge is to come up with parts that are useful on their own. I played around with a few lemmas but they seemed uninteresting on their own so I ended up doing the whole thing in one go in the end.

For the record, here's the string-diagrammatic proof, maybe it helps identify some useful factorization:

You mention tweaking names. Anything in particular you'd like me to adjust? Or do you want to do that yourself?

[HuStmpHrrr]

is it fair that all of them are implicit? also, we probably should use variable.

[sstucki]

It's a good question. We don't seem to have a uniform convention in the library. In the definition of natural transformations we make the maps explicit arguments, but then in concrete naturality conditions, e.g. in the definition of monoidal categories, we don't:

agda-categories/src/Categories/Category/Monoidal/Core.agda

Lines 94 to 99 in 650f1bf

	unitorˡ-commute-from : CommutativeSquare (C.id ⊗₁ f) λ⇒ λ⇒ f
	unitorˡ-commute-to : CommutativeSquare f λ⇐ λ⇐ (C.id ⊗₁ f)
	unitorʳ-commute-from : CommutativeSquare (f ⊗₁ C.id) ρ⇒ ρ⇒ f
	unitorʳ-commute-to : CommutativeSquare f ρ⇐ ρ⇐ (f ⊗₁ C.id)
	assoc-commute-from : CommutativeSquare ((f ⊗₁ g) ⊗₁ h) α⇒ α⇒ (f ⊗₁ (g ⊗₁ h))
	assoc-commute-to : CommutativeSquare (f ⊗₁ (g ⊗₁ h)) α⇐ α⇐ ((f ⊗₁ g) ⊗₁ h)

There, f, g, h are all implicit (via generalized variables). I think the implicit version might be easier to use, but I don't know. In any case, I can try making them generalized variables if you think that helps.

[JacquesCarette]

When the objects (and the maps) are completely arbitrary, variables work well. I don't always use variables if the maps need to have some endpoints in common, as that gets finicky if the inference mechanism doesn't figure it out.

[sstucki]

OK, I updated the code to use generalized variables. Let me know if it looks OK, then I'll mark this as resolved.

[sstucki]

I've pushed a commit where I address some of @JacquesCarette's comments. I'll fix up the history once I have addressed the other issues (rebasing these changes into the two original commits).

[JacquesCarette]

I know it's not fully changed, but I like where it's all heading.

[sstucki]

I think I addressed the remaining comments, let me know nid it looks OK.

[JacquesCarette]

Thanks, this looks good to go.