[Merged by Bors] - feat(category_theory/monoidal): the monoidal coherence theorem

[TwoFX]

This PR contains a proof of the monoidal coherence theorem, stated in the following way: if C is any type, then the free monoidal category over C is a preorder.

This should immediately imply the statement needed in the coherence branch.

---

[semorrison]

Is there a reason you use l instead of \lambda?

[TwoFX]

It appears that constructors of inductive types aren't allowed to start with the symbol λ. The error message is invalid introduction rule, atomic identifier expected.

[semorrison]

@gebner, is this a restriction that could easily be lifted?

[gebner]

It's not really a restriction per se, λ_hom_inv just means something different, namely a lambda with an argument called _hom_inv. You can use French quotes though:

inductive Λ | «λ»

[semorrison]

Imagine I don't want to read hom_equiv (it isn't hard to do), but want to be convinced it is correct. Could we state
(C → D) ≃ (monoidal_functor (F C) D), with the forward direction being project (beefed up to be monoidal), and the backwards direction being λ G X, G.obj (free_monoidal_category.of X)?

I'm saying it's really essential or useful to do so here: I'm just making sure I understand!

[TwoFX]

Imagine I don't want to read hom_equiv (it isn't hard to do), but want to be convinced it is correct. Could we state
(C → D) ≃ (monoidal_functor (F C) D), with the forward direction being project (beefed up to be monoidal), and the backwards direction being λ G X, G.obj (free_monoidal_category.of X)?

I don't think this is true. To be precise, we get the left_inv part of the equiv, but not the right_inv. The reason is simply that not every monoidal_functor (F C) D will send 𝟙_ (F C) exactly to 𝟙_ D (only to something isomorphic to it), but this is always true for project f.

However, I'm guessing that the right_inv part holds up to natural isomorphism (I haven't checked this).

If you really care about correctness of hom_equiv, maybe the following weaker observation will satisfy you: if there was a relation missing in hom_equiv, then we wouldn't be able to show that free_monoidal_category C is a monoidal category, and if there were too many relations in hom_equiv, then we wouldn't be able to fulfill the proof obligation in project_map.

[semorrison]

bors d+

[bors]

✌️ TwoFX can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[TwoFX]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests