一句话：证明 C-系统与 B-系统范畴等价，解决 Voevodsky 猜想，并以 CE/E-系统统一二者。
论文研究类型依赖的代数表示。Cartmell 的 C-系统精确对应广义代数理论；Voevodsky 的 B-系统用于形式化并证明类型论的初始性猜想，但二者关系此前仅为猜想。作者构造 C-系统范畴与 B-系统范畴之间的等价，从而证明 Voevodsky 猜想。该等价是更一般的 CE-系统与 E-系统范畴等价在分层结构上的限制：C-系统与 B-系统分别被识别为分层的 CE-系统与 E-系统，即其语境从空语境出发、经语境扩张迭代生成。
C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky. We construct this equivalence as the restriction of an equivalence between more general structures, called CE-systems and E-systems, respectively. To this end, we identify C-systems and B-systems as "stratified" CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AhrensENR25,
title = {Algebraic Presentations of Type Dependency},
author = {Benedikt Ahrens and Jacopo Emmenegger and Paige Randall North and Egbert Rijke},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:14)2025}
}