一句话：用同伦等价和带属性范畴语义，证明外延类型理论相对带计算公理类型理论的保守性。
论文研究外延类型理论与带命题计算规则（或称计算公理）的依赖类型理论之间的关系，证明前者相对于后者具有保守性。作者借鉴同伦类型论的思想，引入上下文之间“典范同伦等价”的概念，并使用带属性范畴（category with attributes）来表述依赖类型理论的语义。借助这一语义框架，论文给出保守性结果：对于本质上涉及 h-set 的判断，在外延类型理论与命题式计算公理类型理论中进行推理是等价的。
We prove a conservativity result for extensional type theories over propositional ones, i.e. dependent type theories with propositional computation rules, or computation axioms, using insights from homotopy type theory. The argument exploits a notion of canonical homotopy equivalence between contexts, and uses the notion of a category with attributes to phrase the semantics of theories of dependent types. Informally, our main result asserts that, for judgements essentially concerning h-sets, reasoning with extensional or propositional type theories is equivalent.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Spadetto25,
title = {Relating homotopy equivalences to conservativity in dependent type theories with computation axioms},
author = {Matteo Spadetto},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:32)2025}
}