同伦类型论与单值基础中的迭代集合范畴
计算机科学中的逻辑
2025-02-19 v1 逻辑
摘要
在同伦类型论和单值基础中工作时，集合范畴Set的传统角色被同伦集合（h-set）的范畴hSet所取代；即具有h-命题同一类型的类型。Set的许多性质对hSet成立（（余）完备性、正合性、局部笛卡尔闭性等）。然而值得注意的是，单值公理意味着Ob(hSet)本身不是一个h-set，而是一个h-groupoid。这在单值基础中是预期的，但在构造类型论的内部模型时，有时拥有一个更严格的集合宇宙也是有用的。在这项工作中，我们将Gylterud（2018）作为Aczel（1978）在类型论中关于集合宇宙的开创性工作的改进而提出的迭代集合V0的类型，配备以Tarski宇宙的结构，并证明它满足h-set的许多良好性质。特别地，我们将V0组织成一个（非单值严格的）范畴，并证明它是局部笛卡尔闭的。这使我们能够将其组织成一个带有族结构的范畴，该结构具有在HoTT/UF内部建模外延类型论所需的结构。我们在一个相当最小的、带有W类型的单值类型论中完成此工作，特别地，我们不依赖于任何高阶归纳类型（HIT）或其他复杂的类型论扩展。此外，V0和模型的构造是完全构造性和谓词性的，同时由于从V0到h-set的解码对所有类型构造子都是定义性交换的，因此使用起来非常方便。本文几乎所有内容都已使用agda-unimath单值数学库在Agda中形式化。
引用
@article{arxiv.2402.04893,
title = {The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations},
author = {Daniel Gratzer and Håkon Gylterud and Anders Mörtberg and Elisabeth Stenholm},
journal= {arXiv preprint arXiv:2402.04893},
year = {2025}
}