一句话:给出笛卡尔闭双范畴相干性的两种证明,将高维结构构造归约到一维范畴论。
本文研究笛卡尔闭双范畴的相干性问题:在对象集合上自由生成的笛卡尔闭双范畴中,任意平行 1-胞之间的结构 2-胞至多只有一个。该结果把在任意笛卡尔闭双范畴中构造结构的困难归约为一维范畴论的层面。作者给出两种证明。第一种沿用经典的 Yoneda 引理方法;第二种则改造 Fiore 对简单类型 lambda 演算的 normalisation-by-evaluation 的范畴分析,将其提升到双范畴情形。作者指出,在构造好适当双范畴结构后,该论证并不比一维对应情形显著复杂,并为借助范畴语义工具进一步证明相干性开辟了道路。
We present two proofs of coherence for cartesian closed bicategories. Precisely, we show that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells. We thereby reduce the difficulty of constructing structure in arbitrary cartesian closed bicategories to the level of 1-dimensional category theory. Our first proof follows a traditional approach using the Yoneda lemma. For the second proof, we adapt Fiore's categorical analysis of normalisation-by-evaluation for the simply-typed lambda calculus. Modulo the construction of suitable bicategorical structures, the argument is not significantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics.