依赖类型理论中良基树的拓扑对应
摘要：用依赖类型论在拓扑学中提供了有关well-founded trees（简称W-types）的拓扑学对应物，通过使用在形式拓扑学中引入的具有证明相关性的概念，即归纳生成的示意格，也被称为归纳生成的基本覆盖。更详细地说，我们首先展示了在同伦类型论中，W-types和证明重要的归纳生成的基本覆盖是可以命题互相编码的。其次，我们证明了它们在intensional Martin-Loef's type theory的Agda实现中是可以定义地互相编码的。最后，我们通过引入well-founded predicates作为依赖W-types的逻辑对应物，在Minimalist Foundation框架中重新构建了等价关系。所有的结果都已经在Agda证明助手中进行了验证。
作者：Maria Emilia Maietti and Pietro Sabelli
论文ID：2308.08404
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-17