Coherence without unique normal forms

TL;DR

This paper develops a new framework for coherence theorems that does not depend on termination or confluence of rewriting systems, demonstrated through iterated monoidal categories.

Contribution

It introduces a two-dimensional congruence framework for coherence problems, enabling proofs without requiring rewriting systems to be terminating or confluent.

Findings

Provides decision procedures for diagram commutativity

Establishes conditions for all diagrams to commute

Offers a new proof of coherence in iterated monoidal categories

Abstract

Coherence theorems for covariant structures carried by a category have traditionally relied on the underlying term rewriting system of the structure being terminating and confluent. While this holds in a variety of cases, it is not a feature that is inherent to the coherence problem itself. This is demonstrated by the theory of iterated monoidal categories, which model iterated loop spaces and have a coherence theorem but fail to be confluent. We develop a framework for expressing coherence problems in terms of term rewriting systems equipped with a two dimensional congruence. Within this framework we provide general solutions to two related coherence theorems: Determining whether there is a decision procedure for the commutativity of diagrams in the resulting structure and determining sufficient conditions ensuring that ``all diagrams commute''. The resulting coherence theorems rely on neither the termination nor the confluence of the underlying rewriting system. We apply the theory to iterated monoidal categories and obtain a new, conceptual proof of their coherence theorem.