the strictness theorem and the coherence theorem for mono...

Stream: new members

[Shanghe Chen]

Hi! Is the coherence theorem for monoidal categories possible proved using the strictness theorem, i.e. that every monoidal category is monoidally equivalent to a strict monoidal category, as said in /tensor categories, theorem 2.9.2/? Currently mathlib prove it via /Ilya Beylin and Peter Dybjer/ in docs#CategoryTheory.FreeMonoidalCategory.subsingleton_hom

[Shanghe Chen]

Currently I am learning some basic properties of monoidal categories and wondering if it’s possible to use Lean as an assistant for usual textbook. Traditionally it seems easier to understand the proof using "the strictness theorem" approach rather than "the free category" approach for the coherence theorem. I haven’t written any code about this and wondering what difficulties would arise in it.