References. Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids (Beylin, Dybjer)
