单值基础的单纯模型（基于 Voevodsky 的工作）
逻辑
2026-02-06 v5 代数拓扑
范畴论
摘要
我们展示了 Voevodsky 在单纯集范畴中构建的单值类型论模型。为此，我们首先给出一种构建依赖类型论范畴模型的通用技术，利用宇宙（universes）来获得相干性。接着，我们构建了一个（弱）通用 Kan 纤维化，并利用它在单纯集中展示了一个模型。最后，我们引入了单值公理（Univalence Axiom）的几种等价表述，并证明了它在我们构建的模型中成立。作为推论，我们得出结论：具有一个单值宇宙（用上下文范畴表述）的 Martin-L"of 类型论，其一致性至少等同于带有两个不可达基数的 ZFC 集合论。
引用
@article{arxiv.1211.2851,
title = {The Simplicial Model of Univalent Foundations (after Voevodsky)},
author = {Chris Kapulkin and Peter LeFanu Lumsdaine},
journal= {arXiv preprint arXiv:1211.2851},
year = {2026}
}
备注
50 pages. V5: final journal version, to appear in Journal of the European Mathematical Society; no change in theorem numbering. Homotopy-theoretic portions appear also in the note "Univalence in Simplicial Sets", arXiv:1203.2553