带有一个 Mahlo 宇宙的 Martin-Löf 类型论中不可达集合的解释
Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
AI总结：
本文证明了在带有 Setzer 的 Mahlo 宇宙的 Martin-Löf 类型论中，通过添加可及性谓词替代上方宇宙，可自下而上解释扩展了不可达集合的 Aczel 构造性集合论，且该谓词可用 W-类型定义并在 Agda 中形式化。
摘要：
Rathjen 证明了，扩展了所有超限阶不可达集合的 Aczel 构造性集合论 $\mathbf{CZF}$ 可以在扩展了 Setzer 的 Mahlo 宇宙及其上方另一个宇宙的 Martin-Löf 类型论 $\mathbf{MLTT}$ 中进行解释。在本文中，我们展示了如果改为添加一个可及性谓词，则无需 Mahlo 宇宙上方的宇宙即可自下而上地执行此解释。如果在带有外延相等类型的 Martin-Löf 类型论中进行研究，则该可及性谓词可以用 $\mathrm{W}$-类型来定义。我们解释的主要部分已在证明助手 Agda 中形式化。
英文摘要：
Rathjen proved that Aczel's constructive set theory $\mathbf{CZF}$ extended with inaccessible sets of all transfinite orders can be interpreted in Martin-Löf type theory $\mathbf{MLTT}$ extended with Setzer's Mahlo universe and another universe above it. In this paper we show that this interpretation can be carried out bottom-up without the universe above the Mahlo universe, provided we add an accessibility predicate instead. If we work in Martin-Löf type theory with extensional identity types the accessibility predicate can be defined in terms of $\mathrm{W}$-types. The main part of our interpretation has been formalised in the proof assistant Agda.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
