Coherence for monoidal categoriesLast updated Feb 3, 2024Extracting a proof of coherence for monoidal categories from a formal proof of mnormalization for monoids (Beylin, Dybjer)