= Termination proof of monoidal coherence
Orient associativity towards right association and unit maps towards deletion of unit symbols. A lexicographic measure consisting of the number of leaves and the sum of the sizes of left subtrees decreases at every step. All overlapping reductions have commuting completions: the essential cases are the <pentagon identity for a monoidal category>, the <triangle identity for a monoidal category>, and the derived left and right unit identities. Induction on the decreasing measure makes every normalization arrow equal, proving that every structural arrow is determined by its endpoints.
Back to article page
