无唯一正规形式的相干性

由范畴所承载的协变结构的相干性定理，传统上依赖于该结构底层项重写系统的终止性与合流性。尽管这一性质在多种情形下成立，但它并非相干性问题本身所固有的特征。迭代幺半范畴的理论即说明了这一点——它为迭代 loop 空间建模，具有相干性定理，却不具有合流性。我们构建了一个框架，用于以配备二维同余关系的项重写系统来表达相干性问题。在该框架内，我们为两个相关的相干性定理提供了通解：判定所得结构中图表交换性是否存在判定过程，以及给出确保“所有图表交换”的充分条件。所得到的相干性定理既不依赖于底层重写系统的终止性，也不依赖于其合流性。我们将该理论应用于迭代幺半范畴，并获得了其相干性定理的一个新的、概念性的证明。