建模拟方块类型论的公理在一个拓扑中
摘要：同伦方法用到意向类型理论将等式的证明视为路径。我们探讨了在一个拓扑中，一个对象$I$需要满足什么条件才能提供这样的基于路径的类型理论模型，其中路径只是以$I$为定义域的函数。Cohen、Coquand、Huber和M"ortberg使用一类特定的预层给出了这样的模型。我们研究了他们的模型构造在任何拓扑的内部类型理论中可以表达到什么程度，并确定了一个相当弱的公理集合来实现这个目的。这进一步阐明了在他们对Voevodsky的同构公理的建设性解释中的统一Kan补充概念的定义和性质。（这篇论文是对25th EACSL年度计算机科学逻辑会议（CSL 2016）同名论文的修订和扩展版本。）
作者：Ian Orton and Andrew M. Pitts
论文ID：1712.04864
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22