Monoidal coherence

[patrick-nicodemus]

This file extends some work previously done by @Alizter. Ali originally defined the free monoidal category FMC X on a type X, and the "normalized" free monoidal category NFMC X on X, which is just [List X] equipped with the path groupoid structure. I extend this by proving that these categories are equivalent, via functors interp_nfmc : FMC X -> NFMC X and embed_fmc : NFMC X -> FMC X.

Ali proved a monoidal coherence theorem for hsets stating that

Theorem monoidal_coherence {X} `{IsHSet X} {x y : FMC X} (f f' : x $-> y) : f $== f'.

An immediate consequence of the fact that the categories are equivalent is that the interpretation functor is faithful. This gives us the following coherence theorem:

(** A monoidal coherence theorem for general types. *)
Theorem monoidal_coherence {X} {x y : FMC X} (f f' : x $-> y)
 (p : fmap interp_nfmc f = fmap interp_nfmc f')
  : f $== f'.
Proof.
  exact (interp_nfmc_Faithful _ _ _ _ _ p).
Defined.

This can be seen as a strengthening of Ali's original theorem which drops the global truncatedness assumption. One still can only apply the theorem in situations where the paths are known to be equal, but with this strengthening one has at least a fair shot of applying the theorem to categories such as Group or Ring.

(Ali's original file considers the category of endofunctors on NFMC X as well, because NFMC X embeds into this category of endofunctors via the Cayley embedding, and the monoidal product in this category is definitionally unital and associative, so it is even stricter. I opted to trim that material because it can always be added back later.)

[patrick-nicodemus]

@Alizter This equivalence of categories is the equivalence of categories I referenced in this discussion : #2258 (comment). You asked for an example. In this file I have declared one of the Instances as Canonical. I do not have time to construct a minimal example right now, but I assume you will be interested in reading and playing around with this file at some point, and if you remove the Canonical declaration something will break, and you might be able to reduce that to a simple minimal example. While developing this proof I imported Ltac2 and used the Constr.type function to try and compute the type of a term t such that refine t was failing; I found the error messages arising from that tactic more informative than the error message generated by refine. I also used Set Debug "unification" and read through the unification steps to see where unification was failing.

[patrick-nicodemus]

I have been thinking that since NFMC X is a plain type and not a wild category, it is already a fully coherent oo-groupoid, whereas FMC X is a wild category and only has cells in degrees 0, 1, 2.
One could argue on these grounds that NFMC X is the more appropriate notion of free monoidal category for this library. But I'm not really sure where one would see a difference.