论文标题
完全依赖的CCΩ的直觉设置理论模型
An Intuitionistic Set-theoretical Model of Fully Dependent CCω
论文作者
论文摘要
Werner的Set理论模型是CIC的最简单模型之一。它结合了谓语宇宙的功能视图，与不可思议的形式的折叠视图相结合。但是，这种道具模型是如此粗糙，以至于被排除的中间原理。在以前的工作之后，我们将道具解释为一个拓扑空间（一种特殊的代数），以使模型更直观，而无需牺牲简单性。我们通过使用Alexandroff空间对依赖产品类型进行完整解释来改进这项工作。我们还通过增加对列表的支持来扩展我们的归纳类型的方法。
Werner's set-theoretical model is one of the simplest models of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle holds. Following our previous work, we interpret Prop into a topological space (a special case of Heyting algebra) to make the model more intuitionistic without sacrificing simplicity. We improve on that work by providing a full interpretation of dependent product types, using Alexandroff spaces. We also extend our approach to inductive types by adding support for lists.
