Coherence With and Without Unique Normal Forms

One may define a structure on a category to be a two-dimensional system of generators and relations. In the case where all of the structuring functors are covariant in all of their arguments, Kelly [3] showed how to generate a doctrine, D, whose algebras are categories endowed with the free such structure. Viewing a coherence problem as being concerned with the commutativity of diagrams in the initial D-algebra on a discrete category, one may delineate two related coherence questions: (1) Do all diagrams commute?, and (2) Is there a decision procedure that determines whether a given diagram commutes? We recast Kelly’s construction in the framework of term rewriting theory, where the initial D-algebra on a discrete category becomes a term rewriting system modulo a two-dimensional congruence. Within this framework, it is possible to resolve the above coherence questions in terms of the underlying rewrite system. We shall briefly discuss a resolution to (1) for structures described by rewriting systems with unique normal forms. Such systems lend themselves to arguments involving induction on the length of the longest reduction to a normal form. The solution we provide ca