Una categoria monoidale simmetrica e' una categoria munita di un prodotto (binario) associativo e commutativo e di un oggetto che rappresenta l'unita' per questo prodotto. Queste proprieta' sono soddisfatte modulo isomorfismi naturali che verificano delle condizioni di coerenza. Il teorema di coerenza afferma la commutativita' di tutti i diagrammi lineari costituiti da questi isomorfismi.

Dopo un'introduzione agli string diagrams e alla riscrittura, dimostreremo il teorema di coerenza provando la convergenza del sistema di riscrittura di Y. Lafont e usando questo per costruire una base dell'omotopia tramite la quale verificare la commutativita' di ogni diagramma in una categoria monoidale simmetrica.