集合型中的W类型
摘要：构建W类型的扩展性setoid模型，使用基础内涵理论中的依赖式W类型。更精确地说，我们证明setoid的内部范畴具有多项式自函子的初始代数。特别地，我们将从初始代数到给定代数的代数态射的setoid描述为依赖W型上的一个setoid。最后，我们讨论了自由setoid的情况。我们在一个完全内涵的理论中工作，并且事实上，我们只在讨论自由setoid时才假设恒等类型。通过使用依赖W类型，我们还可以避免进入类型宇宙。这些结果已在Coq中验证，并且作者的GitHub页面上提供了形式化的版本。
作者：Jacopo Emmenegger
论文ID：1809.02375
分类：Logic
分类简称：math.LO
提交时间：2023-06-22