Computational coherence
Jon Cohen – 9 May 2007
Iterated monoidal categories form a categorical model of iterated loop spaces. The original paper on these structures included an intricate proof of coherence of the "every diagram commutes" flavour. From a computational perspective, what makes the coherence theorem nontrivial is that the underlying term rewriting system is non-confluent and, as such, does not enjoy unique normal forms. We'll begin with a brief introduction to iterated monoidal categories and use this as motivation for reducing coherence problems to questions in term rewriting theory. Within this setting, we'll derive sufficient conditions for the positive resolution of various coherence problems even in cases where the rewriting system is non-confluent and/or non-terminating. With this machinery in hand, we'll return to iterated monoidal categories and give a more conceptual approach to their coherence problem.
Back