同伦类型论与单价基础中的迭代集合范畴
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
AI总结：
本文将 Gylterud 的迭代集合类型 V0 构造为非单价严格范畴并证明其局部笛卡尔闭，从而在最小构造性直谓 HoTT/UF 中内部建模外延类型论，且结果已基本在 Agda 中形式化。
摘要：
在同伦类型论（Homotopy Type Theory）与单价基础（Univalent Foundations）中工作时，传统集合范畴 Set 的角色由同伦集合（h-sets）范畴 hSet 取代；所谓同伦集合，是指其恒等类型为 h-命题的类型。Set 的许多性质对 hSet 仍然成立，包括（余）完备性、正合性、局部笛卡尔闭性等。然而值得注意的是，单价公理意味着 Ob(hSet) 本身并不是一个 h-set，而是一个 h-groupoid。这在单价基础中是意料之中的，但有时拥有一个更严格的集合宇宙也很有用，例如在构造类型论的内部模型时。在本工作中，我们为 Gylterud（2018）提出的迭代集合类型 V0 赋予 Tarski 宇宙结构；V0 是对 Aczel（1978）关于类型论中集合宇宙开创性工作的精化。我们证明它满足 h-sets 的许多良好性质。特别地，我们将 V0 组织成一个（非单价的严格）范畴，并证明它是局部笛卡尔闭的。这使我们能够将其组织成一个带族范畴（category with families），并具备在 HoTT/UF 内部建模外延类型论所需的结构。我们是在一种相当最小的、带有 W-types 的单价类型论中完成这些工作的；特别是，我们不依赖任何 HITs 或类型论的其他复杂扩展。此外，V0 与该模型的构造完全是构造性且直谓性的，同时使用起来仍然非常方便，因为从 V0 到 h-sets 的解码对所有类型构造子都定义性地交换。论文几乎全部内容已使用单价数学的 agda-unimath 库在 Agda 中形式化。
英文摘要：
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set hold for hSet ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that Ob(hSet) is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example when constructing internal models of type theory. In this work, we equip the type of iterative sets V0, due to Gylterud (2018) as a refinement of the pioneering work of Aczel (1978) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize V0 into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of V0 and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from V0 into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in Agda using the agda-unimath library of univalent mathematics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
