同伦类型论中的终结余代数与非良基集合
逻辑
2025-09-03 v6 计算机科学中的逻辑
摘要
Lindström 使用集合oid 在 Martin-Löf 类型论中为非良基实质集合建立了模型。在本文中，我们在同伦类型论（HoTT）中构造非良基实质集合的模型，其中等式被解释为恒等类型。第一个模型满足 Scott 反基础公理（SAFA）并对迭代集合的构造进行了对偶化。第二个模型满足 Aczel 反基础公理（AFA），并通过将 Aczel–Mendler 终结余代数定理适配到类型论来构造，这需要命题重定尺寸。为了将余代数理论与反基础公理推广到更高类型层级，我们表述了 AFA 与 SAFA 的推广，并构造了一个满足 SAFA 推广的模型层级。这些推广建立在由其中两位作者先前发展的单值实质集合论框架之上。由于模型构造基于 M-类型，本文还包含了 M-类型的恒等类型作为索引 M-类型的刻画。我们的结果在证明辅助工具 Agda 中形式化。
引用
@article{arxiv.2001.06696,
title = {Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory},
author = {Håkon Robbestad Gylterud and Elisabeth Stenholm and Niccolò Veltri},
journal= {arXiv preprint arXiv:2001.06696},
year = {2025}
}