further coherence conditions for monoidal categories

[Alizter]

Here are the extra axioms that MacLane gave for monoidal categories that were later shown to be redundant by Kelly.

At least one of these actually appears in the monoidal coherence proof so it is not something that follows from coherence for monoidal categories.

cc @patrick-nicodemus who stated two of these in the first (wild) monoidal categories formalization but didn't finish them.

[patrick-nicodemus]

This is really nice. Do you know if there has been any progress on the issue where importing the standard library zeroes out the typeclass database and replaces it with the empty typeclass database defined in the standard library? Because it would be nice to have setoid rewriting for these kinds of theorems.

[Alizter]

@patrick-nicodemus I have not been tracking any recent progress on generalized rewriting on the Coq side. I also haven't had a chance to experiment with it in the library as of yet.

I think the issue of generalized rewriting and noinit actually stems from the issue of using Program without the standard library. This is something that has been known to be unsatisfactory for some time, but I only recently created an issue for it: https://github.com/coq/coq/issues/19033

If we have the ability to register library constants in Program and by extension SetoidRewrite then we could register those directly ourselves without having to worry about importing the Coq standard library. Currently those plugins assume that the Coq standard library contains all the terms needed by the plugin.

I don't however believe any of the Coq devs are looking into this at the moment.

[patrick-nicodemus]

That's interesting. I was not aware that Setoid rewriting depends (nominally?) on Program. What about Ltac2 or Elpi, is it feasible to use either of those without the standard library?

[Alizter]

Ltac2 depends on Ltac but could in theory be separated. There has been work in this direction I believe. The overlap is due to syntax parsing of ltac/ltac2 grammar.

For Elpi, it should be more straightforward to support without the Coq stdlib. It may already be the case today, though I haven't checked. I've thought about using Hierarchy Builder in the library, but I don't have the energy to maintain something like that compared to say the mathcomp team.

[jdchristensen]

At least one of these actually appears in the monoidal coherence proof so it is not something that follows from coherence for monoidal categories.

Just to be sure, I'm guessing that the new lemmas do follow from the coherence. But since the proof of coherence uses at least one of them, we'll need to prove them separately before proving coherence.

[Alizter]

This makes me think that there's a symmetry we can use here. If F is a monoidal structure, then so is flip F, with exchanged unitors and inverted associator. So the second of these lemmas should follow formally from the first. And this might be useful in other places as well. Just an idea. It's ok with me if you merge this as is.

That's a good point. I think this is known as a "reversed monoidal category": https://ncatlab.org/nlab/show/reverse+monoidal+category#:~:text=1.-,Definition,%2C%20Y%20%2C%20X%20%E2%88%92%201%20.

I think that the coherence about the right unitor should follow from the left unitor coherence like you said. In the reversed monoidal category the associator is the inverse so it really is the formal dual of that.

I'll merge this for now and consider treating the reversed monoidal category separately. In 2-categorical language, reversed monoidal categories correspond to ops of the underlying bicategory wheras the opposite monoidal category is just the co of the underlying bicategory (where only the 2-cells are reversed).