将同伦等价与带计算公理的依赖类型理论中的保守性联系起来
Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
AI总结：
本文借助同伦类型理论与带属性范畴，通过上下文间典范同伦等价证明外延类型理论对带命题计算公理的依赖类型理论具有保守性。
摘要：
我们利用同伦类型理论的洞见，证明了外延类型理论相对于命题类型理论（即具有命题计算规则或计算公理的依赖类型理论）的保守性结果。该论证利用了上下文之间典范同伦等价的概念，并使用带属性范畴的概念来表述依赖类型理论的语义。非正式地说，我们的主要结果断言，对于本质上关于 h-集合的判断，使用外延类型理论或命题类型理论进行推理是等价的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
