Coherence for monoidal categoriesLast updated Oct 7, 2024References.Extracting a proof of coherence for monoidal categories from a formal proof of mnormalization for monoids (Beylin, Dybjer)