基于Moore路径的类型理论模型
摘要：一种介绍Martin-Lo"of内指类型理论新模型家族的论文。我们在topos中使用有序代数。模型中的恒等类型由Moore路径的概念给出。通过考虑一个特定的大拓扑，我们展示了存在一个非平凡的非截断模型，即在所有维度上包含非平凡结构。换句话说，在这个模型中，一个嵌套序列的恒等类型中的类型可以包含超过一个元素，无论嵌套的程度有多大。尽管受到基于简单集和立方集的非截断类型理论模型的启发，但本文提出的模型概念在类型的语义中避免了任何形式的Kan填充条件。
作者：Ian Orton and Andrew M. Pitts
论文ID：1802.05629
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22