一句话：提出一种内化类型间态射、含 Π/Σ/同一类型的类型论，并证明其在 comprehension 范畴语义下的可靠性。
近期内涵类型论的模型常建立在代数弱分解系统（AWFS）之上，由此得到的 comprehension 范畴具有类型之间的非平凡态射，而标准 Martin-Löf 类型论解释并不使用这些态射。本文把这一语义特征反映回语法，发展出一种内化类型间态射的类型论，包含 Π、Σ 与同一类型；并说明它可视为 Coraglia 和 Emmenegger 所勾勒的带强制子类型的 Martin-Löf 类型论扩展。作者定义了相应的语义结构，证明该类型论相对于该语义的可靠性，并给出大量语义结构实例，从而获得丰富的解释。
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{NajmaeiWAN26,
title = {From Semantics to Syntax: A Type Theory for Comprehension Categories},
author = {Niyousha Najmaei and Niels van der Weide and Benedikt Ahrens and Paige Randall North},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776725}
}