立方集合内的单纯集合
摘要：在最近的观察中，单形集的拓扑空间 $mathbf{sSet}$ 出现为立方集的拓扑空间 $mathbf{cSet}$ 的基本子拓扑空间。$mathbf{cSet}$ 是有限格和它们之间的单调映射的预层的范畴 $mathbf{FL}$ 上的源自 Cohen 等人立方模型类型理论的变体，旨在为验证 Voevodsky 的唯一性公理和具有计算含义的类型理论提供一个模型。 我们的贡献是在 $mathbf{cSet}$ 中构造了一种纤维完美的唯一性宇宙，适用于那些是层的类型。这使得我们可以将 $mathbf{sSet}$ 视为唯一性 Martin-L"of 类型理论中的子模型 $mathbf{cSet}$。 此外，我们解决了类型理论 Cisinski 模型结构在 $mathbf{cSet}$ 上是否与测试模型结构相一致的问题。我们没有回答这个开放问题，而是给出了一个以手头的伴随函子为基础的重述。
作者：Thomas Streicher, Jonathan Weinberger
论文ID：1911.09594
分类：Category Theory
分类简称：math.CT
提交时间：2021-03-15