笛卡尔立方体集合上的等变模型结构

《Advances in Mathematics》：The equivariant model structure on cartesian cubical sets

　　史蒂夫·阿沃迪（Steve Awodey）、埃文·卡瓦洛（Evan Cavallo）、蒂埃里·科坎德（Thierry Coquand）、艾米丽·里尔（Emily Riehl）、克里斯蒂安·萨特勒（Christian Sattler）
美国宾夕法尼亚州匹兹堡卡内基梅隆大学哲学与数学系，邮编15213

**摘要**
我们开发了一种在奎伦模型范畴（Quillen model category）中的同伦类型理论（homotopy type theory）的构造性模型，该模型经典地呈现了空间的同伦理论。我们的模型基于笛卡尔立方体范畴（cartesian cube category）上的预层（presheaves），这是一个行为良好的艾伦伯格-齐尔伯范畴（Eilenberg–Zilber category）。关键的创新在于立方体Kan纤维化（cubical Kan fibrations）规范中添加了一个等变条件，该条件可以描述为对称序列立方体集合范畴（symmetric sequences of cubical sets）中基于区间的均匀纤维化（uniform fibrations）类的拉回。我们模型开发中的主要技术结果已被形式化到一个计算机证明助手中。

**1. 引言**
**1.1. 解释同伦类型理论**
马丁-洛夫依赖类型理论（Martin-L?f dependent type theory）[68],[70]为构造性数学提供了基础。它既作为一种数学论证的形式语言，也作为一种编程语言：马丁-洛夫类型理论中的数学陈述的证明可以被看作是具有计算内容的函数或算法。在21世纪初，人们发现了马丁-洛夫类型理论的高维甚至同伦解释[54],[8],[22],[61]。这些解释的创新之处在于它们对恒等式的处理方式，即类型之间元素的恒等性被视为连接它们的路径或更高阶的单元。同伦类型理论（Homotopy Type Theory，HoTT）或单值基础（Univalent Foundations，UF）[91]是指通过沃沃德斯基的单值公理（Voevodsky’s univalence axiom）增强后的马丁-洛夫类型理论形式系统，该公理断言一个特定的规范映射是在宇宙U中类型A=UB（类型A和B之间的恒等关系）与类型A?B（类型A和B之间的同伦等价关系）之间的等价关系。

为了建立单值公理与马丁-洛夫类型理论规则的一致性（相对于数学其余部分的一致性），沃沃德斯基[61]使用单纯集（simplicial sets）中的标准同伦理论模型构建了一个同伦类型理论模型。该构造利用了单纯集上的奎伦模型结构[74]，该结构将该范畴作为一个抽象同伦理论的框架。特别是，依赖类型族被解释为这种模型结构的纤维化（Kan fibrations），类型形成器的解释依赖于该结构的已知属性；例如，Π-类型的解释基于该结构是右适当（right proper）的事实[61, 2.3.1]。

沃沃德斯基对模型的定义依赖于经典的推理原则，如排中律（law of excluded middle）和选择公理（axiom of choice），考虑到类型理论本身的构造性特征，这种依赖性是出人意料的。贝泽姆（Bezem）、科坎德（Coquand）和帕曼（Parmann）[16],[20],[72]表明，模型的组成部分实际上是本质上是非构造性的（尽管参见下文§1.7.3）。因此，人们也有兴趣找到仅使用构造性有效推理来定义的模型。这样的模型尤其可以构造出一个与映射（1.1.1）显式等价的逆映射，为调用单值公理的证明提供计算内容。

**1.2. 立方体解释**
朝着构造性模型的第一步是由贝泽姆（Bezem）、科坎德（Coquand）和胡贝尔（Huber）[17]迈出的，他们给出了同伦类型理论的部分构造性解释，后来在[18]中得到了完善。他们的解释用立方体集的形式替换了单纯集，即立方体范畴上的预层，从而避免了沃沃德斯基模型中的非构造性元素。科恩（Cohen）、科坎德（Coquand）、胡贝尔（Huber）和莫特伯格（M?rtberg）[29]在另一种高度结构化的立方体集形式中给出了完整的构造性解释；在这种背景下，他们还能够解释高阶归纳类型[31]。安朱利（Angiuli）、法沃尼亚（Favonia）和哈珀（Harper）[5]基于阿沃迪[9]提出的第三种立方体范畴——笛卡尔立方体（cartesian cubes），使用科坎德[36]为这些立方体集提出的纤维化定义，描述了一种计算解释。这项工作从CCHM模型中缩减了立方体范畴，只保留了对于解释高阶归纳类型显然必不可少的对角面映射。然后安朱利等人[1]将这种计算解释转化为立方体集解释。现在可以将CCHM和笛卡尔解释理解为适用于任何具有笛卡尔结构的立方体范畴的单一构造的实例[35]。

这些模型的灵感可以追溯到卡恩（Kan）早期关于立方体集中的抽象同伦理论的工作[60]。他的E-复形（现在称为立方体Kan复形）是奎伦模型结构中的纤维化对象，其纤维化是满足填写盒子属性（box-filling property）的映射[57, §3, 33, 8.4.38]。与单纯集相比，立方体集对于类型理论的构造性解释的一个关键特征似乎是立方体在对称单项积（symmetric monoidal product）下的封闭性——m-立方体和n-立方体的积是（m+n）-立方体——这在构造宇宙中起着关键作用。然而，卡恩立方体集中的单项积不是对称的，因此这些技术在这些立方体集中似乎无法产生构造性解释。然而，可以考虑多种对称立方体范畴（例如，参见Grandis和Mauri [44]以及Buchholtz和Morehouse [25]），因此产生了多种立方体解释。

**1.3. 立方体模型结构**
尽管HoTT/UF的立方体解释并非使用奎伦模型范畴引入的，但事后可以[80],[35],[12]将每种解释视为确定一种奎伦模型结构。
2. 给定一个以适当结构化的范畴形式存在的马丁-洛夫类型理论模型，其中包含家族[40]或自然模型[10]（如前述的立方体解释），我们考虑其上下文范畴（category of contexts）。在这个范畴上，我们有一类候选纤维化：与语义类型Γ?A相关联的上下文投影pA:Γ→Γ的收缩。我们还有一类候选平凡纤维化：那些根据HoTT [91, 3.11]从可缩语义类型派生的纤维化。

3. 一个奎伦模型结构完全由其纤维化和平凡纤维化类所决定，但并非每种选择都会形成一个奎伦模型结构。首先，每个类应形成一个弱分解系统（weak factorization system）的右类。如果是这种情况，我们就有了一个巴顿（Barton）[13]意义上的预模型结构（premodel structure）。一个预模型结构决定了一个候选的弱等价类，而一个预模型结构正是当这个类满足2-of-3性质时才是一个奎伦模型结构。当满足所述性质时，我们可以谈论与类型理论模型相关联的奎伦模型结构。

由于立方体解释中的语义类型是由右提升属性定义的，因此诱导出的纤维化和平凡纤维化类确实定义了一个预模型结构并不令人惊讶。主要的技术挑战在于检查2-of-3性质。在与沃沃德斯基单纯模型历史相反的情况下，该性质使用类型理论模型的组成部分来验证。特别是，用于解释宇宙的纤维化扩展属性（fibration extension property）和等价扩展属性（equivalence extension property），以及用于解释Π-类型的弗罗贝尼乌斯条件（Frobenius condition）[22, 3.3.3, 46]都直接发挥了作用。

**1.4. 标准同伦理论**
将每个立方体解释与一种奎伦模型结构相关联后，我们可以询问每种解释呈现了哪种同伦理论，即它们呈现的(∞,1)-范畴。特别是，我们想知道任何HoTT的构造性解释是否呈现了空间的(∞,1)-范畴（或同伦类型或∞-群胚），正如沃沃德斯基在单纯集中的经典模型所做的那样。虽然我们最终可能希望像舒尔曼（Shulman）在经典设置中完成的那样[85]在所有∞-拓扑中解释HoTT，但在空间中的解释是HoTT中合成同伦理论的基本动机。

在模型范畴语言中，我们寻找一个与立方体解释相关联的模型结构与已知呈现空间的某个模型范畴（如单纯集上的经典Kan–Quillen模型结构）之间的奎伦等价（或奎伦等价的之字形）。实际上，我们可以更直接地与现有的立方体集上的经典模型结构进行比较。Buchholtz和Morehouse [25]指出，用于建模类型理论的每种立方体范畴都是所谓的测试范畴（test category）。由Grothendieck [45]发起并由Maltsiniotis [66]和Cisinski [33]继续发展的测试范畴理论保证（使用经典逻辑），任何测试范畴上的预层范畴都允许一个呈现空间同伦理论的奎伦模型结构。因此，我们也可以询问与立方体解释相关的奎伦模型结构是否与测试模型结构一致。这是一个更强的条件，因为同一个底层范畴上可以存在多个等价但不相同的奎伦模型结构。

这些问题最初在2018年的豪斯多夫研究所季度会议上进行了讨论，并且许多负面结果成为了众所周知的，在同伦类型理论邮件列表[38]上进行了讨论，并在[81]中进行了概述。结果表明，许多立方体解释并不呈现空间，更不用说与相应的测试模型结构一致了。特别是，最小对称单项立方体范畴中的BCH模型并不呈现空间。后来的模型构造在任何具有笛卡尔积的立方体范畴中都产生了解释，因此这里有许多候选者需要考虑。然而，无论是带有连接和反转的德摩根立方体范畴[29]，还是在[1],[12]中考虑的最小笛卡尔立方体范畴，都没有给出空间的模型。一个悬而未决的问题是，在具有笛卡尔结构和连接的德德金立方体范畴（Dedekind cube category）中的解释是否呈现空间。

这引出了本文的主要结果，即构建了一个能够经典呈现空间同伦理论的立方体解释。

**1.5. 等变立方体模型**
我们通过修改安朱利等人[35]的原始笛卡尔立方体集模型，用更严格的等变纤维化类替换其纤维化，定义了一个新的HoTT模型，并关联了一个奎伦模型结构，即等变笛卡尔模型（equivalent cartesian model）。

**1.5.1. 问题**
我们对等变纤维化的定义是出于对原始奎伦模型结构中与笛卡尔立方体集类型理论模型[35], [12]相关的特定病理学的考虑，即立方体自同构商（automorphism quotients）的非可缩性。在笛卡尔立方体集中，可表示n-立方体In的自同构群是对称群Σn：唯一的自同构是立方体轴的排列。对于任何子群H?Σn，我们有一个商I/Hn∈cSet，它是将排列映射到In相应自同构的H索引图的上确界。当H是非平凡的时，I/Hn在这个模型结构中是不可缩的。

首先，为了理解为什么这是一个问题，让我们考虑一个与呈现空间同伦理论的模型范畴的自然比较：笛卡尔立方体和单纯集之间的伴随（adjunction），其左伴随是三角剖分（triangulation），它将n-立方体映射到1-单形（1-simplex）的n元笛卡尔积。这个伴随实际上是一个奎伦伴随，但TI/Hn∈sSet的所有三角剖分都是可缩的；例如，商I/Σ22同构于Δ2。由于奎伦等价的左伴随反映了余纤维化对象（cofibrant objects）的可缩性[52, 1.3.16]，如果I/Hn不可缩，这个伴随就不能是一个奎伦等价。当然，cSet上的模型结构可以呈现空间，而不需要这个特定的伴随是一个奎伦等价。然而，值得注意的是，三角剖分确实定义了从cSet上的测试模型结构到sSet上的Kan–Quillen模型结构的奎伦等价（见§6.3）。

其次，让我们解释一下为什么在[35], [12]的模型结构中I/Hn是不可缩的。我们回顾了上面提到的“均匀无偏填充”（uniform unbiased box-filling）对其纤维化的描述。简而言之，当映射f:Y?X在每个开盒包含（由子对象c:C?In和广义点ξ:In→I1确定）下都允许选择提升时，它是一个纤维化。在代数弱分解系统（algebraic weak factorization systems，awfs）的语言中，纤维化类由开盒包含的范畴和它们之间的拉回平方生成。实际上，这个开盒范畴生成了平凡余纤维化余代数（trivial cofibration coalgebras）和纤维化代数的范畴，根据加纳的代数小对象论证[42]，它们构成了一个awfs。然后存在一个底层的弱因子分解系统，其左映射和右映射分别是允许平凡余纤维化余代数和纤维化代数结构的映射的收缩。遗忘函子将平凡余纤维化余代数映射到其底层映射，从而创建余极限，而开盒范畴嵌入到余代数范畴中；因此，特别是任何开盒包含和拉回方形的图的余极限都是平凡余纤维化。根据这个定义，1-立方体是可缩的：端点0:1?I是由子对象??I0和点0:I0→I1形成的开盒，因此是一个平凡余纤维化。2-立方体是否可缩就不那么明显了：我们可以将0→:1→I2写成多个生成平凡余纤维化的复合，其中第二个映射是由??I1和常数映射0:I1→I1形成的开盒。我们可以归纳地继续证明，对于所有的n，0→:1→In都是平凡余纤维化，即n个生成平凡余纤维化的复合。然而，请注意，这种构造本质上是不对称的：我们首先沿着一个轴折叠2-立方体，然后再沿着另一个轴折叠。这阻止了我们例如通过取余极限来在0→:1→I/Σ22上推导出平凡余纤维化代数结构：将Σ2对应的单对象群体记为，图将对象发送到，并且σ∈Σ2发送到的图不提升为平凡余纤维化代数的图。实际上，可以证明，如果是一个平凡余纤维化，并且B包含一个非平凡（在适当意义上）的I/Σ22的副本，那么A也是[37, §4]：平凡余纤维化不能折叠I/Σ22的副本。因此I/Σ22是不可缩的[37, §5]；同样的论点也适用于更高立方体的商。1.5.2. 我们对这个问题的解决方案是要求在我们的纤维化上有一个更一般的等变均匀填充结构。首先，我们将1-立方体上的开盒包含推广为任意k-立方体上的点ξ:In→Ik，这样我们就要求提升。这种推广本身并不改变纤维化的类别。关键在于我们对均匀性条件的推广：对于每一个立方体的态射α:Im→In和自同构σ:Ik?Ik，由此产生的提升三角形必须交换。根据这个定义，顶点包含0→:1→In立即是一个平凡余纤维化：它是由??1和点0→:1→In形成的开盒。此外，对于任何H?Σn，图H→cSet2将对象发送到，并且σ∈H现在确实可以提升为平凡余纤维化代数的图；其余极限将点0→:1→I/Hn显示为一个平凡余纤维化，使得I/Hn是可缩的。这些观察结果促使我们在2019年夏天构造了等变模型结构下的余纤维化和平凡余纤维化的生成范畴。虽然我们相信这些范畴是规范的——因为我们通过两种不同的构造方法同时得出了它们的定义，一种是范畴论的，另一种是类型论的——但相应的模型结构感觉有些特设，不符合已知的同伦类型理论模型范畴构造范式。几年后，我们意识到等变预模型结构可以从立方体物种（即立方体集合的对称序列）的范畴上的预模型结构转移而来，在那里存在一个规范的等变区间对象I=(In)n≥1。在那里，生成余纤维化和平凡余纤维化适合于一个已知的范式，后者是在前者的基础上使用区间I的通用点定义的[1]，[35]，[12]。1.5.2. 结果我们的结果由以下定理总结。定理1.6.1存在一个在笛卡尔立方体集中可构造定义的HoTT模型，它具有一个相关的可构造定义的Quillen模型结构，该结构在经典上与单纯集上的Kan–Quillen模型结构等价。所谓相关的Quillen模型结构，我们指的是在§1.3中所说的模型结构，其纤维化是HoTT模型的上下文扩展的收缩，而其平凡纤维化是通过可缩类型的上下文扩展的收缩。所谓的HoTT模型，我们指的是一个验证等价公理的Martin-L?f类型理论模型，而所谓的Martin-L?f类型理论模型，我们指的是一个自然模型[10]，配备了Π型、Σ型、恒等型和在这些类型下封闭的宇宙。更准确地说，我们构造的是一个自然的伪模型，按照Shulman [85, §A]的意义，具有这种结构的弱稳定等价物（一类弱稳定的Π型等）；然后可以应用Lumsdaine和Warren的左伴随分裂一致性构造[65, [10]；[85, §A]来获得一个具有严格稳定结构的自然模型。具体来说，我们的上下文范畴是笛卡尔立方体集合的范畴cSet，指定类型和术语的自然伪模型是编码等变纤维化的纤维化结构（引理5.3.3）。类型形成器的解释如下：•弱稳定的Σ型和恒等型直接来自模型结构（例如，参见[65, §4.2]）。Σ型通过纤维化代数的复合来解释，而A?Γ上的恒等型通过其对角线A→A×ΓA的（平凡余纤维化，纤维化）分解来解释（如[8]中所述）。•弱稳定的Π型来自Frobenius条件[22, 3.3.3, 46]，即沿着纤维化的前推的闭合，这在中得到了验证。•宇宙通过分类器来解释，这些分类器用于编码对于足够大的不可达基数κ的κ-小等变纤维化的纤维化概念（命题5.3.7）。重要的是，这些分类器具有纤维化的基础对象（命题5.3.9）并且是等价的（命题5.3.8）。前一个属性与模型范畴的纤维化扩展属性（命题5.3.10）密切相关，后者与等价扩展属性（命题5.3.1）密切相关。主要的技术工作在于构造等价宇宙。在证明主定理的过程中，我们实际上构造了两个同伦类型理论模型及其相关的Quillen模型结构：一个在立方体物种的范畴上的模型，它不模拟经典同伦理论，另一个在cSet上的模型，它模拟了。为了避免重复，并考虑到未来的应用，我们在更一般的公理化设置中证明了将确立这些模型范畴必要属性的核心定理，证明了具有独立兴趣的结果。1.6.1. 大纲我们的发展过程如下：•在§2中，我们回顾了Shulman的纤维化结构概念，特别是包括从代数弱因子分解系统获得的右映射范畴。再次遵循Shulman的方法，我们定义了一个纤维化结构的宇宙，即通过非循环纤维化的“解析”。我们定义了第一种纤维化结构的例子，即均匀平凡纤维化，遵循[12]。•在§3中，我们在[83, 39, §3]中定义的圆柱形预模型结构的抽象设置中工作。我们分别建立了圆柱形预模型结构满足等价扩展属性的充分条件；-满足Frobenius条件；-支持纤维化和等价的纤维化宇宙；-定义了一个Quillen模型结构。这些构造构成了现有模型范畴立方体解释的支柱，并且可以通过来自[1]或[12]的适当输入来恢复已知的模型结构，例如在笛卡尔或De Morgan立方体集合上。在接下来的章节中，我们将它们应用于两种圆柱形预模型结构：首先应用于，然后应用于cSet本身。作为一个经验法则，仅依赖于纤维化闭合属性（如等价扩展属性）的性质直接在cSet中推导出来，而依赖于通过填充盒子生成纤维化的性质（如Frobenius条件）的性质首先在中证明，然后转移到cSet中。•在§4中，我们引入了立方体物种的范畴。我们定义了对称区间，并使用基本上与普通笛卡尔立方体集合模型[1]，[35]，[12]相同的构造，在上定义了一个HoTT模型和Quillen模型结构。•在§5中，我们通过常量函子将cSetΣ上的圆柱形预模型结构转移到cSet，定义等变（平凡）纤维化为通过Δ发送到的（平凡）纤维化。我们展示了这种预模型结构满足2-of-3，证明了定理1.6.1的第一部分：在cSet上存在一个可构造定义的HoTT模型及其相关的Quillen模型结构，其纤维化是等变纤维化。•在§6中，我们证明了定理1.6.1的第二部分，建立了cSet上的等变模型结构与sSet上的Kan–Quillen模型结构之间的Quillen等价。这种等价的左伴随是上述的三角化函子T:cSet→sSet；我们依赖于Reid Barton对T作为一个函子的限制的表征。证明的关键是和都是Eilenberg–Zilber范畴，这意味着它们各自的前层范畴中的单态射是边界包含到可表达对象的商的细胞复形。通过这种方式，T反映弱等价的事实归结为商I/Hn∈cSet的可缩性，我们在§1.5.2中已经看到了这一点，这是由等变纤维化的定义确保的。使用Quillen等价，我们还证明了我们在cSet上的模型结构与测试模型结构一致。最后，我们在附录（§A）中提供了关于在cSet上构造HoTT等变模型的第二种视角。在那里，我们概述了将HoTT翻译到立方体集合的内部扩展类型理论的方法，并增加了区间和余纤维化分类器的公理化，这在Agda证明助手[2]中得到了完整的形式化，遵循Orton和Pitts [71]的方法。这也表明，对于HoTT的立方体模型来说，通常不需要一致性构造来获得Martin-L?f类型理论模型：我们的类型具有足够的结构来直接解释严格稳定的结构（不需要例如选择提升）。1.6.2. 构造性本文的部分目的是描述一个构造性的HoTT模型。因此， §§2–5，最终在cSet上构造了等变HoTT模型和Quillen模型结构，可以完全构造化。然而，请注意，必须用逐层可决定的单态替换预层范畴中的单态的使用，即对于所有c∈C，mc同构于一个余积余射。从构造性上讲，Hofmann–Streicher分类器只有在进行了这种修改后才能在§2.3的意义上形成宇宙，正如在CCHM模型[29, 15]中使用的，并且Orton和Pitts [71, 8.4]明确指出的。请注意，这将子对象分类器替换为对应的筛选是可决定的子对象的分类器。这也使得发展成为谓词的。我们证明了我们在构造2.2.12、构造4.3.5、构造5.2.1、构造5.2.3中使用Garner的代数小对象论证的构造性。注意，笛卡尔立方体范畴的态射集合具有可决定的相等性。Eilenberg–Zilber范畴结构在上是可构造定义的，并且具有有限的面映射切片。通过归纳，我们展示了任何具有逐层可决定的包含到中的对象S都是紧凑的：如果这个映射包含的通用元素，那么是可表达的；否则，它是边界包含的有限细胞复形，其程度低于a。注意，任何双左伴随都保持紧凑对象。在立方体物种中生成的（平凡）纤维化是可表达对象的逐层可决定子对象。根据引理4.3.1，这些通过左Kan扩展从立方体集合中的逐层可决定子对象产生。然后，通过§5.1中的双左伴随L在立方体集合中创建了这些生成（平凡）纤维化。因此，我们每次使用代数小对象论证的所有生成范畴都由具有紧凑域的映射组成。这使得一步因子化的带有点的自函子在ω阶段收敛。关于构造性背景下的代数小对象论证的更多细节，我们参考了Henry [50, §C.2]。在单纯集上的Kan–Quillen模型是可构造定义的[50]，[47]。然而，我们在§6中对等变模型结构和Kan–Quillen模型结构之间证明的Quillen等价并不是构造性的。在其核心，它依赖于在cSet中（逐层可决定的）单态的非构造性呈现作为Reedy细胞复形。**建设性方面，只有Reedy可判定单态射——即那些锁定映射是可判定的单态射——才能以这种方式表示（参见[47，§1.4]）。虽然可能可以用Reedy可判定单态射作为余纤维化来定义等变纤维化模型结构的类似物（如[50]、[47]中对单纯集的处理），但这种选择会干扰用于解释HoTT的连贯性构造，正如Gambino和Henry在[43，8.5]中所发现的那样。更一般地说，如何从建设性角度判断一个同伦理论是否是“空间的同伦理论”目前尚不清楚。事实上，可能存在多个在建设性上不同的同伦理论，而这些理论在经典意义上都等价于Kan–Quillen模型结构。Shulman通过导子[86]对这个问题进行了一些初步分析。**

**1.7 相关和未来的工作**

**1.7.1 高阶拓扑中的HoTT模型**

Shulman已经证明，每一个Grothendieck ∞-topos都可以通过一个类型理论模型topos来表示，该模型topos具有足够的结构来解释HoTT [85]。他的设置使用的是经典逻辑，并且本质上是单纯性的：类型理论模型topos按定义就是一个单纯模型category。据我们所知，我们的模型结构并不属于这个框架：我们没有找到任何适合cSet的单纯丰富化。一个自然的候选定义是将X,Y∈cSet之间的映射空间视为三角剖分的内部同态T[X,Y]∈sSet，但这不会产生一个单纯模型结构，主要是因为T的左伴随（在§6中构造）不保持乘积。Shulman利用Grothendieck ∞-topos作为预层∞-topos的左精确局部化的描述，展示了类型理论模型topos的类别在构建左精确局部化和预层类别时是封闭的。基本情况是空间的∞-topos：具有Kan–Quillen模型结构的单纯集类别就是一个类型理论模型topos。我们的工作建议了一条未来的路径，即通过发展类型理论模型topos的立方概念，并使用cSet上的等变模型结构作为空间的基础模型。**

**1.7.2 其他立方模型**

2022年，第二和第五作者发现了类型理论的第二个立方解释，其相关的Quillen模型结构可以表示空间，这个解释是基于具有一个连接的笛卡尔立方体类别上的预层[39]。在这种情况下，没有必要引入等变纤维化的概念：应用原始的笛卡尔立方模型构造（如[1]、[35]、[12]中的），就可以得到一个表示空间的Quillen模型结构。这可以通过任何在这个立方体类别上的预层纤维化都是自动等变的这一事实来解释，正如[39，4.25]中所概述的（参见我们的命题6.1.7）。这种模型的一个缺点是，具有一个连接的立方体类别的行为不太好：虽然笛卡尔立方体类别是一个Eilenberg–Zilber类别[28，8.12(1)]，但具有一个连接的立方体类别不是一个Reedy类别[39，§A.1]。[39]的主要任务是开发一个可以在这种情况下使用的Eilenberg–Zilber类别的泛化。**

**等变性并不是一个万能的解决方案：我们不能随便取任何现有的立方解释并对纤维化施加等变条件来获得空间的模型。例如，在具有一个连接的情况下，Dedekind立方集（即在具有两个连接的笛卡尔立方体类别上）中的纤维化是自动等变的，但我们仍然不知道这个模型是否可以表示空间，主要是因为这个立方体类别甚至比具有一个连接的类别更远离Eilenberg–Zilber类别[39，§A.2]。在BCH立方体类别上，它是一个Eilenberg–Zilber类别[28，7.10]，添加等变性会导致立方体商I/Hn变得可缩，就像在笛卡尔立方体集中的情况一样。然而，从三角剖分的角度来看，这是可取的。不过请注意，在BCH立方体集的测试模型结构中，商I/Σ22是不可缩的，而是表示RP∞的悬挂。**

**1.7.3 建设性的单纯模型**

Kan–Quillen模型结构已经在单纯集上通过Henry [50]以及Gambino、Sattler和Szumi?o [47]的建设性方法得到了发展。然而，Bezem、Coquand和Parmann表明，Voevodsky在单纯集上的模型在本质上依赖于经典原理[16]、[20]、[72]。本质上，这是因为Kan–Quillen模型结构通常不能证明具有余纤维化对象；实际上，余纤维化对象是Reedy可判定对象，我们可以决定一个单元是否是退化的。特别是，Π类型的解释是有问题的：从建设性角度来看，即使X和Y都是Kan复合体，指数YX也不必是一个Kan复合体——需要X的余纤维性。**

如§1.6.2中提到的，Gambino和Henry [43]给出了Voevodsky在余纤维化单纯集上的HoTT模型的建设性重构。然而，对余纤维化对象的限制干扰了获得严格模型所需的连贯性构造，这意味着最终结果不如其经典等价物。Van den Berg和Faber [21]提出了另一种方法来建设性化Voevodsky的模型，用限制性的有效Kan纤维化概念替换Kan纤维化。与我们的工作类似，这个想法是对提升施加额外的统一性条件。尽管这种方法不需要将纤维化限制为Reedy可判定单态射，从而可能避免[43]中的连贯性问题，但它仍在进行中：据我们所知，到目前为止，既没有建立宇宙的解释，也没有建立Quillen模型结构。**

**1.7.4 立方类型理论**

Cohen、Coquand、Huber和M?rtberg [29]不仅提出了一个同伦类型理论的模型，还提出了一个立方类型理论，这是一个扩展了Martin-L?f类型理论的新判断和类型形成器，反映了De Morgan立方集模型的结构。Angiuli等人[5]、[1]同样设计了一个在笛卡尔立方体集上解释的立方类型理论。与[91]中制定的HoTT不同，这些理论具有规范性：任何封闭的自然数都可以定义性地计算为一个数字[5]、[56]。**

[1]中的笛卡尔立方类型理论也可以在等变笛卡尔模型中解释：每个等变纤维化特别是原始笛卡尔立方体集模型意义上的纤维化，因此解释了笛卡尔立方类型理论中的填充运算符（有时也称为组合运算符）[1，§1.2]。因此，笛卡尔立方类型理论有一个模型可以表示空间的同伦理论。人们可以想象通过引入一个等变填充运算符来扩展笛卡尔立方类型理论。这样的运算符可以通过以下规则引入：下载高分辨率图像（29KB）；下载全尺寸图像，它通过用任意k-立方Ik替换区间I以及通常的方程来直接推广普通的填充运算符comp?→.Ar→→s→[???→.u]u0=u[s→/?→]当?成立时；comp?→.Ar→→s→[???→.u]u0=u0当r→=s→，这些方程指定了comp的输出为输入盒的填充器。等变性表明，对于每个σ∈Σk，我们有方程????comp?→.Aσ?r→→σ?s→[???→.u]u0=comp?→.A[σ??→/?→]r→→s→[???→.u[σ??→/?→]]u0，其中?σ?是σ对I中项的k元组的作用。然而，我们不知道在立方类型理论中实际使用等变填充运算符有任何用途。在立方类型理论中工作的合成同伦理论家尚未发现例如笛卡尔立方类型理论和De Morgan立方类型理论之间，或者立方类型理论和[91]中的HoTT之间的表达能力有任何根本差异，情况似乎也是一样的。此外，类型检查等变填充运算符也会非常昂贵和复杂：比较两个k维comp项是否相等需要测试它们是否在k!个排列下一致。**

**1.8 致谢**

等变模型的发现是在挪威奥斯陆的挪威科学院高级研究中心（CAS）进行的，该研究项目是在2018-19学年关于同伦类型理论和单值基础的研究项目，由Marc Bezem和Bj?rn Dundas组织。我们非常感谢他们的支持。第一和第三作者还感谢Institut des Hautes études Scientifiques在2022年6月提供了两周非常愉快的讨论。**

**生成余纤维化和平凡余纤维化的类别作为由立方物种内部索引的观点（见§4.3）来自于与Andrew Swan的讨论。Reid Barton最近对三角剖分函子的洞察使我们能够大大简化§6中结果的证明。**

第一和第四作者得到了美国空军科学研究办公室在FA9550-21-1-0009号奖项下的支持，以及第一作者在FA9550-20-1-0305号奖项下的支持。第二作者得到了美国空军科学研究办公室在FA9550-19-1-0216号奖项下的支持，以及Knut和Alice Wallenberg Foundation在2020.0266号和2019.0116号奖项下的支持。第三作者得到了欧洲研究委员会高级奖项101053291号项目的支持。第四作者还得到了美国国家科学基金会在DMS-2204304号和DMS-2507077号奖项下的支持，以及约翰霍普金斯大学的President's Frontier Award的支持，后者支持了与其他作者的交流。第五作者得到了瑞典研究委员会在2019-03765号奖项下的支持，以及美国空军科学研究办公室在FA9550-24-1-0302号奖项下的支持。**

**2. 纤维结构和宇宙的概念**

一个（模型范畴）HoTT模型包含两类“正确”的映射：纤维化，它们模型化类型家族；以及平凡纤维化，它们模型化可缩类型家族。这两类映射的一个关键特征是它们在任意映射下的稳定性，这在类型理论中模型化了变量替换。在这一节中，我们抽象地考虑了这样的“纤维结构概念”，证明了将适用于我们构建的模型类别中的纤维化和平凡纤维化的一般结果。在§2.1中，我们回顾了“纤维结构概念”的精确技术含义，并探讨了当这种纤维结构在局部上是可表示时的含义。在§2.2中，我们专门讨论了基本拓扑，并展示了如何通过针对单态射的提升来定义局部可表示的纤维结构。在§2.3中，我们介绍了我们的宇宙概念，并在预层拓扑的情况下，从Hofmann–Streicher分类器构建了局部可表示的纤维结构的宇宙。**

**2.1 局部可表示和相对无环的纤维结构概念**

在带有拉回的1-范畴E中的映射组装成一个在E上的逆变群体值伪函子，将对象X映射到具有域X的大群体上。这个伪函子E被称为自我索引的核心——这里的“自我索引”指的是切片范畴E/X，“核心”指的是它们的群体核心。在[85，3.1]中，Shulman定义了在带有拉回的范畴E上的纤维结构概念，作为一个具有小纤维ψ:F→E的严格离散纤维化，在2-范畴的逆变群体值伪函子和它们之间的伪自然变换中。这里，严格离散纤维化是一个其组成部分是群体纤维化的严格自然变换。**

拆解这一点，纤维结构概念由以下内容给出：(i) 对于E中的每个映射f:Y→X，一组“纤维结构”；(ii) 对于每个拉回平方(2.1.0)，一个从f上的纤维结构集合到?g?f上的纤维结构集合的函数，该函数在拉回平方中是伪函子的。更多讨论见[85，§3]。遵循Shulman的方法，我们将与纤维结构概念F相关的“结构化纤维化”称为F-代数，然后将引出?g?f上的F-代数结构的拉回平方（2.1.1）称为F-态射。**

**定义2.1.1 [85，3.2]**

如果对于E中的每个对象X，F(X)→E(X)都是完全忠实的，则纤维结构概念ψ:F→E是满的。也就是说，如果每个F-代数之间的拉回平方都可以唯一地扩展为一个F-态射。然后Shulman为这种纤维结构概念制定了各种条件，这些条件可以用来构建分类宇宙。其中第一个条件是：**

**定义2.1.2 [85，3.10]**

如果逆变群体值伪函子类别中的每个拉回都是可表示的，则纤维结构概念F是局部可表示的。明确地说，每个映射 f:Y→X 都有一个分类器 ψf:F(f)→X，用于 f 上的 F-代数结构，这意味着对于所有 g:Z→X，?g?f 上的 F-代数结构与通过 ψf 提升的 g 之间一一对应。特别是，规范映射 ψf:F(f)→X 的截面唯一对应于 f:Y→X 上的 F-代数结构。引理 2.1.3 设 F 是一个局部可表型的纤维化结构概念。(i) 任何映射 f:Y→X 沿着 ψf:F(f)→X 的拉回都有一个规范的 F-代数结构。(ii) 如果 ?g?f 是沿 g 对 f 的拉回，则 ?F(g?f) 是沿 g 对 F(f) 的拉回，即 ??F(g?f)?g?F(f)。证明 拉回图中顶部的水平映射指定了映射 ?ψf?f 上的一个 F-代数结构 γf。由于拉回消除和 Yoneda 嵌入的完全忠实性，局部可表型意味着左侧的方形是一个逆变群体值伪函子的拉回，因此在 E 中也是。注释 2.1.4 回想一下，如 (ii) 中所述的 F-代数的拉回是一个 F-态射，当且仅当 ?g?f 上的 F-代数结构是从 f 上的 F-代数结构创建的。定义 2.1.3 中的自然条件告诉我们，当由相应截面的表示态射定义的方形可交换时，情况就是这样：[85, §3] 中考虑了大量局部可表型的纤维化结构概念的例子。我们仅提及一个例子，它将在下一节中应用。例子 2.1.5 [85, 3.7,3.14] 从 E 上的一个函子分解可以得到一个纤维化结构 F，其 F-代数是具有针对其左因子选择解决方案的映射：如果 E 是局部笛卡尔封闭的，并且函子分解是笛卡尔的，即函子将拉回方形映射到拉回方形，那么这种纤维化结构是局部可表型的。明确地说，jf 可以编码为 E/X 中从 Rf 到 f 的内部同态 ???[Rf,f]X?(Rf)?(Rf)?f 的一个元素，该元素沿着 Lf 限制在 Y 处为恒等映射。因此，我们定义 ψf:F(f)→X 为这个限制映射的拉回。

定义 2.1.6 [85, 5.11] 如果对于任何具有 F-代数结构 x 在 f 上和 x′ 在 f′ 上的拉回方形，存在一个 F-代数结构 x￣ 在 f 上使得该方形成为从 x′ 到 x￣ 的 F-态射，则纤维化结构概念 F 是相对无环的。回想一下 [85, 2.8] 中的二元范畴中的提升属性：当态射 i:A→B 和 f:Y→X 在 2-范畴 K 中具有提升属性时，如果映射 K(B,Y)→K(A,Y)×K(A,X)hK(B,X) 是本质满射，则它们具有提升属性，其中 ×h 是一个弱二元范畴拉回。定义 2.1.7 如果在 E 上的逆变群体值伪函子中的态射在 Yoneda 嵌入下可以右提升单项式的像，则它是无环纤维化。注释 2.1.8 对于在 E 上的逆变群体值伪函子中的严格离散纤维化，二元范畴右提升属性等价于范畴右提升属性 [85, 2.10]。特别是，这适用于纤维化结构概念及其拉回。引理 2.1.9 给定一个纤维化结构概念 ψ:F→E，以下条件是等价的：(i) ψ:F→E 是相对无环的，(ii) ψ 的每个核对投影都是无环纤维化。证明 对于图 (2.1.9)，f 和 f′ 上的一对 F-代数结构由一对映射 x:E(?,X)→F 和 x′:E(?,X′)→F 组成，使得外部方形可交换，即对应于针对 ψ 的核对的提升问题。这样的提升问题的解由映射 x￣:E(?,X)→F 确定，使得 x￣i=x′ 且 ψx￣=ψx，也就是说 f 上的一个 F-代数结构，使得 (2.1.11) 是从 x′ 到 x￣ 的 F-态射。□引理 2.1.10 当 F 是 E 上的一个局部可表型和相对无环的纤维化结构概念时，对于任何映射 f:Y→X，ψf:F(f)→X 中的核对中的映射都可以在 E 中提升单项式。证明 回想所讨论的映射的定义：由于拉回的核对是核对的拉回，因此可表示映射 ψf:E(?,F(f))→E(?,X) 的核对可以提升可表示的单项式。但是由于 Yoneda 嵌入是完全忠实的并且保持极限，这意味着映射 ψf:F(f)→X 的核对可以在 E 中提升单项式。□根据引理 2.1.10，一个完整的纤维化结构概念，如下例所示，自动是相对无环的。例子 2.1.11 [64, 6.1.6.4–7][85, 4.18] 对于任何局部可呈现且局部笛卡尔封闭的范畴 E，对于足够大的正则基数 κ，相对 κ-可呈现的态射形成一个局部可表型和相对无环的完整纤维化结构 Eκ。8 局部可表型的纤维化结构概念也可以通过各种方式从一个范畴转移到另一个范畴。这里我们利用了涉及 [79, §4–5] 中的莱布尼茨构造的转移结果。定义 2.1.12 考虑与一对范畴 D 和 E 相关联的应用双函子。假设 E 有推导和拉回，这诱导了莱布尼茨推导应用和莱布尼茨拉回应用双函子，它们分别将自然变换 α:F?G 和箭头 f:Y→X 发送到自然性方形中的诱导映射：引理 2.1.13 假设 D 和 E 分别有弱分解系统 (L,R) 和 (M,E)。那么自然变换 α:F?L 之间的莱布尼茨推导应用如果且仅如果共轭自然变换 α:R?U 之间的莱布尼茨拉回应用保持右类则保持左类。证明 记 Ladj(D,E)?ED 和 Radj(E,D)?DE 分别为由左伴随函子和右伴随函子张成的完整子范畴。注意我们有一个范畴等价 Ladj(D,E)op?Radj(E,D)，它交换左伴随和共轭变换。此外，通过这种等价，限制的应用双函子是参数化的伴随。因此，根据 [79, 4.10, 4.11]，莱布尼茨推导应用左伴随双函子和莱布尼茨拉回应用右伴随双函子是参数化的伴随，这在提升问题之间诱导了一种双射对应关系：对于 L 中的 ?:A→B 和 E 中的 e:Y→X。结论随之成立。引理 2.1.14 假设 E 和 E′ 有拉回，α:L?K:E′→E 是一个在保持拉回的函子之间的自然变换，并且 L 有一个索引右伴随：那么如果 E 有一个纤维化结构概念 F，则 E′ 有一个纤维化结构概念 F′，其中 F′-代数是从 F-代数在 α 的莱布尼茨拉回应用下创建的。此外，(i) 如果 F 是相对无环的，那么 F′ 也是；(ii) 如果 E 是局部笛卡尔封闭的并且 F 是局部可表的，那么 F′ 也是。证明 由于函子保持拉回，F′ 在 E′ 上定义了一个纤维化结构概念。由于 L 和 K 保持拉回，它们保持单项式，所以函子 α°?? 保持定义 2.1.7 中的单项式，因此如果 F 是相对无环的，那么 F′ 也是。剩下的是验证局部可表型。为此，考虑在 E′ 中诱导一个在 E 中的拉回，如下左所示：根据定义，F′-代数结构在 ?g?f 上对应于 F-代数结构在 ?α°?g?f 上。由于 F 是局部可表的，这些对应于截面，因此在引理 2.1.4 中构建的上面右的拉回方形中的提升。通过在投影 ?αX?Kf:KY×KXLX→LX 相关联的拉回 ? 推前伴随进行转置，这样的虚线提升与下面左的提升一一对应，由于 L 有一个索引右伴随 RX [73, B1.2.3]，这样的虚线提升与上面右的虚线提升一一对应。通过拉回的泛性质，我们可以将 ??ψg?f:F′(g?f)→Z 定义为上面右所示的拉回。□例子 2.1.15 例如，L:E′→E 可能有一个普通的右伴随，并且假设 E 有一个终端对象，K:E′→E 可以被取为终端函子。在这种设置中，莱布尼茨拉回应用简化为 L 的应用，引理 2.1.16 特化为 Shulman 的观察，即局部可表型的纤维化结构概念可以沿着保持拉回的左伴随被提升[85, 3.5, 3.12]，尽管对于该结果 E 只需要具有拉回，不需要是局部笛卡尔封闭的。例如，对于任何对象 X∈E，这样的伴随由沿 X→1 的拉回函子给出：因此，E 上的局部可表型的纤维化概念可以提升到其切片范畴。

2.2. 单项式和均匀平凡纤维化设 E 是一个基本拓扑，并写 ?:1→Ω 为其子对象分类器。我们考虑一类“平凡纤维化”，其特征是在单项式下具有右提升属性，并展示它构成了我们称之为均匀平凡纤维化结构的纤维化结构概念。然后我们展示这种纤维化结构概念是局部可表的。首先，由于基本拓扑特别地是局部笛卡尔封闭的，E 中的每个映射 f:X→Y 都诱导了一个函子三元组，其中 f! 是后组合，?f? 是拉回，而 ?f?（根据定义）是推前。此外，以下适用于 E：引理 2.2.1 在局部笛卡尔封闭的范畴中，沿着单项式 i 的拉回-推前伴随 ??i??i? 形成了一个反射嵌入。证明 当 ??i??i? 的余单位是其共轭，即 ?i!?i? 的单位是一个同构时，它是同构的，但后者是明显的，因为 i 沿其自身的拉回是一个同构。□我们注意到拓扑中单项式的以下封闭性质，以便以后使用：注释 2.2.2 由于基本拓扑是粘合的，单项式类在推导积下是封闭的，在切片范畴中也是如此：给定一对单项式 i:A?B 和 j:C?D，推导积是子对象 i×D:A×D?B×D 和 B×j:B×C?B×D 的并集 [63, 17]。我们现在使用子对象分类器来定义部分映射分类器（在 [73, §A.2.4] 中称为部分映射表示器）。反过来，这些将用于定义我们的平凡纤维化。以下两个命题在 [12, §3] 中得到证明（也见 [73, A2.4.7] 和 [46, 9.8–9]）：命题 2.2.3 对于任何 Y∈E，存在一个如下左所示的拉回方形，其中任何如下右所示的部分映射都由唯一映射 ζcy:Z→Y+ 分类，该映射定义了一个拉回方形。此外，对于任何 X∈E，同样的结果在 E/X 中也是成立的，并且这些分类方形在拉回下是稳定的。□我们将单项式 ηY:Y?Y+ 称为 Y 的部分映射分类器，因为从 Z 到 Y 的部分映射由（总）映射 Z→Y+ 分类。我们写 f+:Y+X→X 为（Y,f）∈E/X 的部分映射分类器的值域，这样我们就有 ηf:Y→Y+X。定义 2.2.4 在 f:Y→X 上的相对 +-代数结构是在 X 上到映射 ηf:Y?Y+X 的收缩：(2.2.4) 相对 +-代数的范畴以相对 +-代数为对象，以如下左所示的方形为态射，使得下面右的诱导图可交换：注释 2.2.5 提议 2.2.3 的相对版本定义了一个保持拉回的函子分解：满足示例 2.1.6 的假设。这定义了一个弱分解系统，其左映射是单项式，其右映射是允许相对 +-代数结构的映射。注释 2.2.6 部分映射分类器 ηY:Y?Y+ 是单位自然变换在（纤维化）自函子 (?)+:E→E 上的组成部分。因此对象 ?Y+=Ω!??Y 本身是一个（自由）+-代数。这可以用来展示注释 2.2.6 的函子分解构成了一个代数弱分解系统。详细信息见 [46, 9.5] 或 [12, §3]。通过以下命题，我们可以看到相对 +-代数结构由针对所有单项式的统一选择的提升组成。命题 2.2.7 相对 +-代数的范畴同构于其对象是映射 f:Y→X 与其在所有拉回方形中一致选择的提升配对：并且（ii）态射 f′→f 是与选择的提升兼容的交换方形。证明 根据命题 2.2.3，任何在单项式和映射 f 之间的提升问题都可以唯一分解为因此相对 +-代数唯一地为 f 配备了针对所有单项式的统一选择，反之亦然，这样的提升专门化以配备 f 与相对 +-代数。同样，方形 f′→f 与针对所有单项式的选择的提升的兼容性归结为与收缩 ρf′ 和 ρf 的兼容性。见 [12, 3.7] 和 [46, 9.9(i)]。□定义 2.2.8 写 TF 为通过应用示例 2.1.6 和注释 2.2.6 的部分映射分解在 E 上获得的纤维化结构概念。我们称 TF 为均匀平凡纤维化结构概念。然后 TF-代数正好是相对 +-代数，而 TF-态射是那些也是相对 +-代数态图的拉回方形。根据命题2.2.8，TF-代数等价于配备了在拉回平方中均匀地对所有单态射进行提升的选择的映射，当针对f′所选的提升是通过限制针对f的提升来确定的时，拉回平方f′→f是一个TF-态射。引理2.2.9指出，在一个基本拓扑系统中，纤维结构TF的概念是相对无环的并且是局部可表示的。证明由于注解2.2.6，函子分解保持了拉回，而我们的环境目录是局部笛卡尔封闭的，示例2.1.6告诉我们相对+-代数定义了一个局部可表示的纤维结构。相对无环性的证明通过适应Shulman的[85, 5.18]得到。在这种情况下，相对无周期性断言对于任何水平映射是单态射且垂直映射是如左下图所示的相对+-代数的实心箭头拉回平方，可以通过改变f的相对+-代数结构使得右下图中的虚线映射交换。当我们忽略结构并考虑TF下的映射类时，我们找到了另一个等价的特征。命题2.2.10以下条件对于在一个基本拓扑E中的映射f→X是等价的：(i)f是一个相对+-代数。(ii)f在所有单态射之间的拉回平方中均匀地提升。(iii)f提升所有单态射。证明(i)和(ii)之间的等价性来自于命题2.2.8。显然(ii)蕴含(i)，而(iii)蕴含(ii)，因为图表(2.2.5)是一个针对单态射的提升问题。定义2.2.11我们将满足命题2.2.11的等价条件的映射f称为平凡纤维化。在E的内部，相对+-代数可以看作是由通过子对象分类器Ω索引的映射家族?:1→Ω生成的。在E是一个预层拓扑的情况下，这可以被外化为通过一小类映射生成的。这两种观点都是Swan [89]关于在Grothendieck纤维化中的提升框架的实例：内部观点的陪域纤维化和外部观点的类别索引家族纤维化。构造2.2.12设E=SetCop是一个预层拓扑。在Ω上的切片类别中，映射?:1→Ω可以被视为一个子终端对象，它决定了由基础对象Ω内部索引的映射家族。这个家族可以外化为在Ω的元素类别上定义一个函子，通过将这个内部家族拉回到可表示对象上来实现。因此，笛卡尔函子I将Yoneda嵌入从与Ω的元素类别相关联的离散纤维化提升到E的陪域纤维化：它将一个元素映射到它分类的子对象，而∫Ω中的映射则被映射到子对象之间的拉回平方中：回想一下，对于任何索引类别I和到箭头类别的函子，都有一个相应的类别?I?，其对象是配备有针对I的对象的图像的选定提升的E中的箭头，这在I的映射中是自然的[23, 15]。特别是，当E=SetCop是一个预层拓扑时，类别?(∫Ω)?的一个对象是一个映射f:Y→X，它配备了在拉回平方中均匀的针对可表示对象的选定提升：命题2.2.13对于E=SetCop一个预层拓扑，相对+-代数的类别在?(∫Ω)?上是同构的。证明该声明断言在一个预层拓扑中，命题2.2.8的提升属性简化为只需针对可表示对象的子对象进行提升的情况。参见[46, 5.16]。注解2.2.14总结来说，在一个预层拓扑的设置中，我们有多个等价的相对+-代数类别和纤维结构TF的概念的表征。然而，请注意，这些视角提示了两个非同构的代数弱分解系统，提供了一个将映射分解为单态射的函子分解，然后是一个平凡纤维化。一方面，如注解2.2.7所描述的，相对+-代数分解是awfs的基础。另一方面，Garner的代数小对象论证应用于生成类别，得出的monad代数类别与?(∫Ω)?同构[42, 4.4]。根据命题2.2.14，第二个awfs的monad代数类别因此与第一个awfs的指向端函子代数类别同构，后者是定义2.2.4中的相对+-代数类别。实际上，相对+-代数分解是代数小对象论证的一步分解。另见[46, 9.5]中的讨论。2.3. 宇宙定义2.3.1固定一个纤维结构F的概念。F的一个宇宙是一个F-代数π:U˙→U，使得π:E(?,U)→F是一个无环纤维化，这意味着我们有针对Yoneda嵌入的单态射i:A?B的双范畴提升，如下所示：拆开来看，这要求对于任何一对F-代数p,q和F-映射（如下面的实心箭头平方所示），其中i:A?B是一个单态射，存在一个沿着i的h的扩展，它将后面的拉回平方分解为拉回的复合，并定义了一个从p到π的F-映射。命题2.3.2假设E具有由拉回沿任意映射保持的初始对象。给定一个具有宇宙π:U˙→U的相对无环纤维结构F的概念，每个F-代数都是π的一个拉回。证明假设p:E?B是一个F-代数。下面的图表中的后拉回平方在初始对象上给出了一个F-代数结构，并且由于相对无环性，F-代数p可以被赋予一个F-代数结构，使得左边的拉回成为一个F-映射。因为π:U˙→U是一个宇宙，p因此是π的一个拉回。我们现在专门针对一个预层拓扑E=SetCop和某个小索引类别C来给出一个宇宙的例子。对于任何足够大的正则基数κ，如果C是κ-小的，Hofmann–Streicher构造[54]，[11]提供了一个分类器?:V˙κ→Vκ，用于κ-小的家族，即那些组件具有κ-小纤维的映射。如示例2.1.13中所指出的，对于足够大的κ，这定义了一个局部可表示且相对无环的完整纤维结构Eκ。通过[34, 3.9]，[71, 8.4]或[11, 6]，分类器?:V˙κ→Vκ是Eκ的一个宇宙。现在考虑在预层拓扑E上的纤维结构F的概念。构造2.3.3如果F是局部可表示的，那么对于足够大的κ，我们可以如下定义一个κ-小的F-代数分类器π:U˙κ→Uκ。首先，我们定义了一个新的纤维结构Fκ的概念，其中Fκ-代数是一个κ-小的F-代数。如果F是局部可表示的或相对无环的，那么对于足够大的κ，使得示例2.1.13成立，Fκ继承了这些属性[85, 3.3, 3.11, 4.18, 5.14]。现在设置?Uκ?Fκ(?)并形成拉回作为引理2.1.4(i)的一个特例：引理2.3.4映射π:U˙κ→Uκ在规范上是一个Fκ-代数。命题2.3.5设F是在一个预层拓扑上的局部可表示的纤维结构。对于足够大的正则基数κ，Fκ-代数π:U˙κ→Uκ是Fκ的一个宇宙。证明构造2.3.3将Fκ-代数分类器定义为拉回注意，这个严格的拉回也是一个双范畴拉回，因为Fκ→Eκ是一个严格的离散纤维化。由于Hofmann–Streicher分类器?:V˙κ→Vκ是一个宇宙，右边的垂直映射是一个无环纤维化，因此它的双范畴拉回也是如此。由于大小原因，需要多个宇宙来分类属于给定纤维结构的所有映射。为了使由给定宇宙分类的映射在各种范畴运算下封闭，我们现在假设基数κ是不可访问的，以便相应的Hofmann–Streicher宇宙?:V˙κ可以被视为内化的Grothendieck宇宙。定义2.3.6在预层拓扑中，如果对于任何基数λ，存在一个不可访问的基数κ≥λ和一个宇宙π:U˙κ→Uκ，用于一个相对无环的纤维结构，其底层映射是P中的κ-小映射，那么一个拉回稳定的映射类P具有宇宙。特别是，P中的每个κ-小映射都是π:U˙κ→Uκ的一个拉回，根据命题2.3.2。我们现在做出一个永久假设，即存在任意大的不可访问基数。然后，命题2.3.5为预层拓扑上任何局部可表示和相对无环的纤维结构类别的映射类提供了宇宙。参见[85]或[48]，了解在更一般的范畴设置中宇宙级别的处理。 notation 2.3.7在定义2.3.6的设置中，通常不需要在索引宇宙级别的不可访问基数之间进行区分。因此，我们通常简单地将π:U˙→U写作分类器家族的一个通用成员，而不明确指定基数界限。3. 圆柱模型结构在本节中，我们为构建我们的两种同伦类型理论模型奠定了理论基础，证明了我们的结果在一般性方面确保它们可以应用于立方集合和立方物种，同时也使它们能够在其他地方使用。在§3.1中，我们引入了圆柱预模型结构83的概念，也在[39]中使用，它提供了在弱等价关系尚未满足2-of-3属性的设置中的抽象同伦理论的熟悉结构。特别是，这些公理提供了在切片下稳定的纤维化映射路径空间分解，我们在§3.2中建立了这些基本属性。在§3.3中，我们在一个局部笛卡尔封闭的圆柱预模型类别中陈述并证明了等价扩展属性，在该类别中，上纤维化是单态射，并且这些在所有切片中都稳定于推出产品。在§3.4中，我们引入了Frobenius条件并提到了一些后果。在§3.5中，我们将等价扩展属性与圆柱预模型结构上Frobenius条件下的单值性公理联系起来。在§3.6中，我们利用这一点来建立宇宙的纤维性，假设纤维化是通过标准构造之一从平凡纤维化定义的。在§3.7中，我们将宇宙的纤维性转化为纤维化扩展属性，这意味着圆柱预模型结构实际上是一个模型结构，这反过来也证明了本节的标题以及我们在此过程中使用的弱等价关系和非标准编码的正确性。3.1. 圆柱预模型结构根据Barton [13]，一个类别E上的预模型结构是一对弱分解系统，称为(平凡上纤维化，纤维化)和(上纤维化，平凡纤维化)弱分解系统，使得每个平凡上纤维化都是上纤维化（等价地，任何平凡纤维化都是纤维化）。我们还要求有限极限和余极限（实际上，通常只需要沿着纤维化的拉回和沿着上纤维化的推出）。我们用箭头表示平凡上纤维化，用?表示上纤维化，用?表示上纤维化，用表示平凡纤维化。在一个预模型结构中，定义一个映射为弱等价关系，如果它可以分解为一个平凡上纤维化后跟一个平凡纤维化的复合。特别是，平凡上纤维化和平凡纤维化允许这样的分解，因此这两个类别都包含在弱等价关系的类别中。相反，通过一个标准论证：引理3.1.1任何上纤维化和弱等价关系都是平凡上纤维化，任何纤维化和弱等价关系都是平凡纤维化。证明证明是相互的，并且是标准的。如果一个上纤维化分解为一个平凡上纤维化后跟一个平凡纤维化，这提出了一个提升问题，其解决方案将上纤维化表示为平凡上纤维化的收缩。因此，从Joyal–Tierney对（闭合的）Quillen模型结构的表征[59, 7.7–7.8]：命题3.1.2一个预模型结构定义了一个模型结构当且仅当弱等价关系满足2-of-3属性。注释3.1.3预模型结构提升到切片和余切片类别，所有由遗忘函子到基础类别创建的映射类别。对于一个一般的预模型结构，弱等价关系的2-of-3属性可能难以证明（并且通常是错误的）。一种方便的技术工具可以在需要时用来分析预模型结构中的弱等价关系，那就是下面介绍的伴随函子化圆柱体（adjoint functorial cylinder），它满足三个兼容性条件，使得预模型结构成为一个圆柱形的预模型结构。

定义3.1.4：在范畴E上的函子化同伦概念是指在从E到E的预备函子（profunctor）范畴中的同态双函子（hom-bifunctor）上的一个自反二元关系。对于任意对象对A、B∈E，我们将集合I(A,B)中的元素称为从A到B的映射之间的同伦。更准确地说，一对平行态射f、g:A?B上的纤维定义了从f到g的同伦集合。我们用α:f～g表示α∈I(A,B)f,g。映射?:E(A,B)→I(A,B)将每个f:A→B映射到一个恒定的同伦?f:f～f。

定义3.1.5：如果在范畴E上的同伦概念I可以通过函子P:E→E来协变表示，那么它就是可表示的（representable），这样的函子P定义了一个函子化余圆柱体I(A,B)?E(A,PB)；如果可以通过函子C:E→E来逆变表示，那么它就是可共表示的（corepresentable），这样的函子C定义了一个函子化圆柱体I(A,B)?E(CA,B)。在共表示的情况下，根据Yoneda引理，自然变换(?,?0,?1)确定了这些变换之间的关系。当I既是可表示的又是可共表示的时候，这些函子就是伴随函子，记为C?P，它们的自然变换是共轭的。如同引理2.1.15中所述，我们对共轭变换对使用相同的符号表示，例如?:C?id和?:id?P。我们遵循[39, 3.9]中的定义，将这种可表示的同伦概念称为伴随函子化圆柱体。

现在我们展示所有这些概念在切片操作（即通过某个对象X∈E得到E/X）和余切片操作（即通过EX/）下是稳定的。实际上，只需要考虑切片范畴，因为函子化同伦概念是自对偶的。

引理3.1.6：如果E具有函子化同伦概念I，那么对于任何X∈E，切片范畴E/X也具有函子化同伦概念IX。此外：
(i) 如果I是可共表示的，那么IX也是可共表示的；
(ii) 如果I是可表示的，并且E具有拉回（pullback）操作，那么IX也是可表示的。

证明：我们将一般情况留给读者处理，并在可表示的情况下构造函子化圆柱体和余圆柱体。

给定一个对象g:Y→X在切片范畴E/X中，其纤维化圆柱体分解可以通过遗忘函子（forgetful functor）到E来创建，而投影到X是通过在图中组合得到的。

注释3.1.7：定义3.1.4和定义3.1.5是自对偶的，因此引理3.1.6的对偶也适用于余切片范畴EX/。

定义3.1.8：如果E上的预模型结构允许一个伴随函子化圆柱体存在，那么该结构是圆柱形的，如果满足以下条件：
(i) ?:P?id×id的Leibniz拉回操作保持纤维化（fibrations）和平凡纤维化（trivial fibrations）；
(ii) ?0:P?id和?1:P?id的Leibniz拉回操作将纤维化映射为平凡纤维化。

根据引理2.1.15，这些条件也可以用共轭自然变换的Leibniz推出操作来对偶表述。如引理2.1.15所述，我们使用相同的符号表示共轭变换对，例如?:C?id和?:id?P。我们遵循[39, 3.9]中的定义，将这种可表示的同伦概念称为伴随函子化圆柱体。

我们现在证明所有这些概念在切片操作（通过任意对象X∈E得到E/X）和余切片操作（通过EX/）下是稳定的。实际上，只需考虑切片范畴，因为函子化同伦概念是自对偶的。

引理3.1.6：如果E具有函子化同伦概念I，那么对于任何X∈E，切片范畴E/X也具有函子化同伦概念IX。此外：
(i) 如果I是可共表示的，那么IX也是可共表示的；
(ii) 如果I是可表示的，并且E具有拉回操作，那么IX也是可表示的。

证明：我们将一般情况留给读者处理，并在可表示的情况下构造函子化圆柱体和余圆柱体。

给定一个对象g:Y→X在切片范畴E/X中，其纤维化圆柱体分解可以通过遗忘函子到E来创建，而投影到X是通过在图中组合得到的。

注释3.1.7：定义3.1.4和定义3.1.5是自对偶的，因此引理3.1.6的对偶也适用于余切片范畴EX/。

定义3.1.8：如果E上的预模型结构允许一个伴随函子化圆柱体存在，那么该结构是圆柱形的，如果满足以下条件：
(i) ?:P?id×id的Leibniz拉回操作保持纤维化（fibrations）和平凡纤维化（trivial fibrations）；
(ii) ?0:P?id和?1:P?id的Leibniz拉回操作将纤维化映射为平凡纤维化。

根据引理2.1.15，这些条件也可以用共轭自然变换的Leibniz推出操作来对偶表述。

引理3.1.9：如果E具有函子化同伦概念I，那么在其每一个余切片和切片范畴上也诱导出一个圆柱形的预模型结构。

证明：我们先证明切片范畴的情况，余切片的情况是对偶的。根据引理2.1.15，只需证明?:id+id?C的Leibniz推出操作保持余纤维化（cofibrations）和平凡余纤维化（trivial cofibrations），以及?0,?1:id?C的Leibniz推出操作将余纤维化映射为平凡余纤维化。但由于E是圆柱形的，这些结构和构造都是通过遗忘函子到E得到的，因此这是显而易见的。

圆柱形预模型结构的公理允许我们在不依赖于弱等价关系的2-of-3性质的情况下，推导出各种“类似2-of-3”的“无环”（acyclic）态射的性质。其中两个结果是：

引理3.1.10 [39, 3.19–20, 3.27]：在圆柱形预模型结构中，任何如下左图所示的图表中，纤维化都是平凡纤维化；如果通过沿着余纤维对象之间的拉回来检测平凡纤维化，那么如下右图所示的任何图表中也同样成立。第一个结论是通过使用公理3.1.8(ii)构造一个平凡纤维化并将其作为一个缩回（retract）来证明的。即使f不是纤维化，第二个结论也可以通过一个基本的 lifting 证明。

3.2. Brown 因子分解：圆柱形预模型结构的构造旨在提供在余切片和切片操作下稳定的纤维化映射圆柱体（fibred mapping cylinder）和映射路径空间分解（mapping path space factorization）。在本节中，我们关注映射路径空间的构造，我们将其称为“Brown 因子分解”（Brown factorization），这个概念来源于[26]，它将在下一节中用于建立等价扩展性质。

构造3.2.1：给定一个映射f:Z→Y在一个圆柱形预模型范畴中，其Brown 因子分解f=pf?sf是通过以下方式构造的：根据构造，f=pf?sf且1=qf?sf。

引理3.2.2：对于圆柱形预模型范畴中的映射f:Z→Y的Brown 因子分解：
(i) 如果Y是纤维化的，那么(qf,pf):Bf→Z×Y是一个纤维化；
(ii) 如果Y是纤维化的，那么qf:Bf→Z是一个平凡纤维化；
(iii) 如果Y和Z都是纤维化的，那么pf:Bf→Y是一个纤维化。

证明：如果Y是纤维化的，那么根据定义3.1.8，?:PY?Y×Y是一个纤维化，从而证明了前两个结论；如果Z是纤维化的，那么投影π:Z×Y?Y也是一个纤维化，从而证明了第三个结论。

注释3.2.3：根据引理3.1.9，构造3.2.1可以在切片范畴中实现。给定一个通过g:Y→X映射到X的映射f:Z→Y，其纤维化Brown 因子分解是通过在X的切片上实现Brown 因子分解构造来定义的。这将f的图（视为一个以Z×XY为陪域的态射）通过下图所示的纤维路径对象的拉回来分解：

通过交换构建Brown 因子分解的拉回操作和到X的切片的拉回操作，纤维化Brown 因子分解是图中右侧所示的非纤维化Brown 因子分解的拉回。这里的右侧矩形是通过将非纤维化Brown 因子分解应用于从f到X上的单位映射构成的交换-square得到的。

在这种情况下，引理3.2.2特别指出：
(i) 当g是一个纤维化时，(qf,pf):BXf→Z×XY是一个纤维化；
(ii) 当g是一个纤维化时，qf:BXf→Z是一个平凡纤维化；
(iii) 当g和gf都是纤维化时，pf:BXf→Y是一个纤维化。

引理3.2.4：纤维化Brown 因子分解在所有拉回操作下是稳定的。

证明：这是将(3.2.4)中右侧图描述中的纤维化Brown 因子分解与拉回操作相结合的结果。

定义3.2.5：如果在一个圆柱形预模型范畴中的纤维化对象Z→Y之间的映射f的Brown 因子分解中，右侧的因子pf:Bf→Y是一个平凡纤维化，那么称这个映射为可缩的（contractible）。在存在2-of-3性质的情况下，可缩映射与纤维化对象之间的弱等价关系是一致的。

引理3.2.6：在一个圆柱形模型范畴中，如果弱等价关系满足2-of-3性质，那么纤维化对象之间的映射是可缩的当且仅当它是一个弱等价关系。

证明：如果弱等价关系满足2-of-3性质，那么平凡纤维化qf的截面sf也是一个弱等价关系。因此，根据2-of-3性质，f是一个弱等价关系当且仅当纤维化pf是一个平凡纤维化。

为了强调，我们将在切片E/X中的可缩映射称为在X上的可缩映射。具体来说，一个在X上的纤维化映射f:Z→Y是可缩的，当且仅当它的定义域Z→X和陪域Y→X都是纤维化，并且引理3.2.3中的纤维化pf:BXf?Y是一个平凡纤维化。

3.3. 等价扩展性质：在本节中，我们展示在适当的假设下，圆柱形预模型范畴满足以下条件，其重要性将在后续部分解释。

定义3.3.1：如果一个圆柱形预模型结构允许任意的可缩映射e沿着任何余纤维化i:A?B扩展到B上的一个可缩映射f，并且f具有指定的陪域扩展了原始映射的陪域，那么该结构具有等价扩展性质。

定理3.3.2：设E是一个具有圆柱形预模型结构的局部笛卡尔封闭范畴（locally cartesian closed category），其中余纤维化是单射（monomorphisms），并且这些单射在所有切片下的推导积（pushout-products）下是稳定的。那么E具有等价扩展性质。

示例3.3.3：例如，根据注释2.2.2，在一个基本的拓扑范畴（elementary topos）中，如果余纤维化是单射，那么这些假设是满足的。此外，在一个预层拓扑范畴（presheaf topos）中，定理3.3.3中的所有构造都将尊重宇宙层次（universe levels）。

我们对等价扩展性质的处理遵循[80]中的方法，该方法使用可缩映射来表述。在一个圆柱形模型范畴中，如果弱等价关系满足2-of-3条件，根据引理3.2.7，这等同于使用弱等价关系来表述的等价扩展性质[61]、[84]。

定理3.3.3的证明占据了本节的其余部分。首先，在图(3.3.2)中，我们有?i?Y1?X1，根据假设，我们定义一个对象Y0及其映射f:Y0→Y1作为沿着i的给定纤维化映射e:X0→X1的推前（pushforward）的拉回：

根据引理2.2.1，?i?ηY1是可逆的。考虑(3.3.5)在保持拉回操作的函子?i?下的像，我们得出?i?f与??i?i?e?e同构。换句话说，f:Y0→Y1沿着i拉回得到原始映射e:X0→X1，形成了所需形式的图(3.3.2)。

剩下要证明的是q1f:Y0→B是一个纤维化，并且f:Y0→Y1是在B上的一个可缩映射。我们将在B的切片中证明这两点。

对于可缩性，考虑e和f的纤维化Brown 因子分解：根据引理3.2.5，f的纤维化Brown 因子分解沿着i拉回到e的因子分解，类似地，纤维路径对象?i?PBY1?PAX1（图未显示）。然而，e的纤维化Brown 因子分解与f的纤维化Brown 因子分解之间的关系更为复杂。要理解这一点，首先考虑由定义映射(qf,pf)的拉回平方和单位自然变换??η:id?i?i?得到的自然性立方体（naturality cube）：背面是构造3.2.1中的拉回，前面是其在右侧伴随?i?下的像，因此也是一个拉回。由于(3.3.5)是一个拉回，底部的平方也是一个拉回。通过拉回组合和取消，顶部的平方也是一个拉回。

现在考虑与pf和?1相关的交换立方体：顶部平方已经被证明是一个拉回，底部平方显然也是一个拉回。因此，当我们按照左侧和右侧面指示的方式形成拉回时，我们得到了pf作为映射?i?pe的拉回的因子分解。这种分解将pf显示为一个平凡纤维化，因为我们现在这样论证。

首先，由于e是在A上的一个可缩映射，其第二个Brown 因子pe是一个平凡纤维化。由于余纤维化是单射，因此在推导积下是稳定的，平凡纤维化在推前下也是稳定的，所以?i?pe是一个平凡纤维化。接下来，映射z可以描述为在B上的平凡纤维化上应用的单位η的Leibniz拉回。但这也是一个平凡纤维化，因为它是在B上的余纤维化对象i:A?B和平凡纤维化的Leibniz指数（Leibniz exponential），并且单射在切片下的推导积下是封闭的。因此pf作为平凡纤维化的复合也是平凡纤维化。所以，只要其定义域q1f:Y0→B是一个纤维化，映射f在B上是可缩的。但是 q1f 是 q1pf 的一个收缩：在这里，右边的矩形是交换的，因为在 f:Y0→Y1 的纤维化 Brown 分解中，pf 和 qf 都作用在 B 上，并且 pf 和 f 的目标都是 q1:Y1?B。我们刚刚证明了 pf 是一个（平凡的）纤维化，而 q1 被假设为一个纤维化；因此，收缩图表明 q1f:Y0→B 也是一个纤维化，正如所需的那样。这完成了定理 3.3.3.4 的证明。

Frobenius 条件在局部笛卡尔封闭范畴的设置中，自然会要求一个预模型结构满足 Frobenius 条件。定义 3.4.1：一个弱分解系统如果左映射在沿着右映射的拉回下是稳定的，则满足 Frobenius 条件。如果其两个弱分解系统都满足这一条件，则该预模型结构也满足 Frobenius 条件。当上纤维化是单射时，由于这些单射在所有拉回下都是稳定的，Frobenius 条件只需要证明平凡的上纤维化-纤维化弱分解系统。由于在局部笛卡尔封闭范畴中，这等价于纤维化在 pushforward 操作下是封闭的，这与类型论的 Π 类型构造相对应，因此这一条件已经在同伦类型论文献中被研究过。关于 Frobenius 条件的各种证明可以在 [29]、[46]、[12]、[53]、[14] 中找到，这取决于如何从平凡纤维化定义纤维化。对于在 §4 中引入的预模型结构，我们需要的结果是以下命题：命题 3.4.2 [1, 3.1.8]、[12, §6]、[53, §4]、[14, 8]：设 E 是一个具有预模型结构的局部笛卡尔封闭范畴，其中上纤维化是单射。假设存在一个对象 I，使得当其在 I 上的拉回的对角映射 δ:I→I×I 在切片预模型结构中是一个平凡纤维化时，映射才是一个纤维化。那么该预模型结构满足 Frobenius 条件。□

现在假设我们正在使用一个具有可局部表示且相对无环的纤维化概念 TF 的预模型结构，其中 TF-代数是平凡纤维化。根据引理 2.2.10，这些假设适用于上纤维化是单射的初等 topos 上的预模型结构。如果这个预模型结构满足 Frobenius 条件，那么平凡纤维化结构分类器具有以下重要性质：引理 3.4.3：考虑一个具有满足 Frobenius 条件的圆柱形预模型结构的局部笛卡尔封闭范畴，其中平凡纤维化是由上纤维化之间的上纤维化对象生成的。假设 TF 是一个可局部表示且相对无环的纤维化概念，其 TF-代数是平凡纤维化。那么如果 f:Y?X 是一个纤维化，那么 ?f:TF(f)?X 也是。证明：为了解决这种形式的提升问题，我们可以等价地解决沿着 B→X 的 ?f 的拉回诱导的提升问题。由于纤维化的拉回稳定性以及引理 2.1.4(ii)，因此只需解决形式为 (3.4.3) 的提升问题，其中是平凡的上纤维化，g:D?B 是一个纤维化。这相当于证明如果纤维化 g 沿着 t 拉回后成为一个 TF-代数，那么它具有一个 TF-代数结构，使得拉回图 (3.4.3) 成为一个 TF-映射。注意根据 Frobenius 条件，这个拉回图中的映射 s 也是一个平凡的上纤维化，因为它是沿着纤维化 g 的平凡上纤维化 t 的拉回。由于 ?t?g 是一个平凡纤维化（根据假设），因此推前 ???t?t?g:t?C→B 也是一个平凡纤维化。由于 t 是单射，引理 2.2.1 表明 ??t?t?g 沿着 t 拉回得到 ?t?g。同样由于 ??t?t?g 是一个（平凡的）纤维化，根据 Frobenius 条件，拉回图 s′ 也是一个平凡的上纤维化。因此，我们有一个 (平凡上纤维化，纤维化) 和一个 (平凡上纤维化，平凡纤维化) 对共同映射 ??g?s=t?t?g?s′ 的分解。在一个圆柱形预模型结构中，由此可以得出纤维化 g 是一个平凡纤维化。

在由一对分解定义的交换图中，形成拉回 P 并将图中的间隙映射分解为一个平凡上纤维化后跟一个纤维化：根据引理 3.1.10 的第一部分，虚线复合纤维化都是平凡纤维化，现在纤维化 g 是一个以 E 为顶点的平凡纤维化交换三角形的底边，所以根据该引理的第二部分，g 也是一个平凡纤维化。这证明了 g 具有一些 TF-代数结构。由于相对无环性，这个结构可以与 ?t?g 的结构对齐，使得图 (3.4.5) 成为一个 TF-映射。这种在 g 上指定新的 TF-代数结构最终解决了原始的提升问题 (3.4.4)。

在引理 3.4.3 的设定中，Voevodsky 构建了一个替代的可缩映射分类器，我们简要讨论一下这一点。讨论 3.4.4：在一个具有满足 Frobenius 条件的圆柱形预模型结构的局部笛卡尔封闭范畴中，对于任何纤维化 f:Y?X，存在一个纤维化 ?f:isContrXf?X，它通过前推然后对其纤维化路径空间纤维化求和来定义：根据构造，映射到 ?f:isContrX(f)?X 的截面对应于映射 s:X→Y 和一个纤维化同伦 s?f～XidY。正如我们的符号所暗示的，映射 ?f:isContrX(f)→X 和在基本 topos 上的预模型结构中构造的映射 ?f:TF(f)→X（其中上纤维化是单射）之间存在密切关系。对于纤维化 f:Y?X，这些定义了“逻辑等价的”纤维化概念，证明了 f 是一个平凡纤维化。实际上，如果 ?f:TF(f)→X 有一个截面，那么 f 是一个平凡纤维化，因为它承认一个截面 s:X→Y，因为所有对象都是上纤维化的。这些数据定义了一个提升问题，可以通过引理 3.1.9 中的 Axiom 3.1.8(i) 解决，构造了一个截面 (s,h) 的 ?f:isContrX(f)→X。相反，如果 ?f:isContrX(f)→X 有一个截面，那么这些数据定义了一个收缩图，展示了 f 作为 ?0 的一个收缩，这在引理 3.1.9 的设定中是一个平凡纤维化（根据 Axiom 3.1.8(ii)）。因此，?f:TF(f)→X 有一个截面。

3.5. 单值性：在一个满足 Frobenius 条件且其纤维化具有定义 2.3.6 中所说的宇宙的预模型结构中，定义 3.3.1 的等价扩展性质与 Voevodsky 的单值性公理有关。为了陈述这一点，我们需要以下构造。遵循符号 2.3.7，我们用 π:U˙→U 表示一个通用的分类宇宙，并将其称为“纤维化宇宙”，而不明确指定一个基数界限。引理 3.5.1：在一个具有满足 Frobenius 条件的圆柱形预模型结构的局部笛卡尔封闭范畴中，任何纤维化 π:U˙?U 都有一个对角线 U→U×U 的分解，使得 (i) (s,t):Eq(U˙)?U×U 是一个纤维化，以及 (ii) Eq(U˙)?U×U 沿着任何 e:Γ→U×U 的拉回分类了 Γ 上的（结构化的）可缩映射。在所述的假设下，这种构造是 Voevodsky 提出的，例如在 [84, §4] 中描述，并涉及他对可缩映射的分类器。如讨论 3.4.6 中所述，我们可以使用任何可局部表示且相对无环的平凡纤维化概念来证明引理 3.5.1。

引理 3.5.1 的证明：我们首先在下面形成左侧的拉回，然后在 U×U 上的切片内形成它们之间的内部同态，如右侧所示：根据 Frobenius 条件，这个映射是一个纤维化。counit?????:MapU×U(π1?U˙,π2?U˙)×U×Uπ1?U˙→π2?U˙ 等价于定义了一个映射?????:MapU×U(π1?U˙,π2?U˙)×U×UU˙×U→MapU×U(π1?U˙,π2?U˙)×U×UU×U˙，这是两个 π 的拉回之间的通用映射，即小纤维化。我们通过为这个 ? 提供 ??MapU×U(π1?U˙,π2?U˙) 上的可缩映射数据来定义 Eq(U˙)，通过取分类器 ????p?:TF(p?)→MapU×U(π1?U˙,π2?U˙)×U×Uπ2?U˙ 对平凡纤维结构，将其前推以获得一个在 ??MapU×U(π1?U˙,π2?U˙) 上的对象，然后求和以获得一个在 U×U 上的对象。因此，得到的映射 Eq(U˙)→U×U 在类型论中可以写作：Eq(U˙)=ΣA,B:UΣf:A→BΠb:BTF(fibf(b))→U×U。很容易看出它具有所述的分类性质 (ii)。根据 (i)，它是一个纤维化，因为映射 ????p?:TF(p?)→MapU×U(π1?U˙,π2?U˙)×U×Uπ2?U˙ 是一个纤维化。但这来自于引理 3.4.3，因为 fibf(b) 只是右边的 Brown 分解 ?????p?:BMapU(π1?U˙,π2?U˙)??Mapp?(π1?U˙,π2?U˙)×U×Uπ2?U˙，根据注释 3.2.3，这是一个纤维化。□

根据刚才给出的构造，纤维化 (s,t):Eq(U˙)?U 的分解如下：刚才构造的可缩映射分类器满足从 TF 的相对无环性继承的相对无环性属性的相对版本。

引理 3.5.2：在一个具有满足 Frobenius 条件的圆柱形预模型结构的局部笛卡尔封闭范畴中，使用可局部表示且相对无环的平凡纤维化概念 TF 定义的可缩映射结构可以沿着单射对齐，因为核对投影沿着单射是可提升的：证明：根据构造，映射 υ 是分类器????p?:TF(p?)→MapU×U(π1?U˙,π2?U˙)×U×Uπ2?U˙ 对平凡纤维结构的前推。由于纤维化 TF 是可局部表示且相对无环的，根据引理 2.1.12，?p? 的核对中的映射沿着单射是可提升的。由于单射在拉回下是稳定的，这个条件在推前下也是稳定的。

引理 3.5.1 的构造允许我们如下编码单值性。定义 3.5.3：如果映射 t:Eq(U˙)?U 是一个平凡纤维化，则纤维化 π:U˙?U 是单值的。注释 3.5.4：定义 3.5.3 与标准同伦类型论中对单值性公理的编码有关。根据引理 3.5.1，U 上的对角线通过映射 id:U→Eq(U˙) 拉升，分类恒等映射。这种对角线的分解可以与 cocylinder 的规范分解相关联，通过映射 u，如下所示：如果宇宙的底是上纤维化的，如下文 §3.6 中在温和假设下将证明的，那么映射 将是一个平凡纤维化，因此在 2-of-3 公理的存在下，t 是一个平凡纤维化当且仅当 u 是一个弱等价。

命题 3.5.5：考虑一个在满足 Frobenius 条件的预层 topos 上的圆柱形预模型结构，其中上纤维化是单射。如果预模型结构具有定义 2.3.6 中所说的宇宙，那么等价扩展性质成立当且仅当每个宇宙 π:U˙?U 是单值的。证明：为了假设单值性来证明等价扩展性质，选择一个足够大的单值宇宙来通过提升问题分类 (3.3.2) 中的数据。为此，我们首先选择分类映射 p￣0:A→U 和 q￣1:B→U，然后使用引理 3.5.1 将映射 (p￣0,q￣1i):A→U×U 扩展为映射 e￣:A→Eq(U˙) 来分类可缩映射 e。由于单值性，t 是一个平凡纤维化，所以这个提升问题有一个解 f￣，它分类了一个沿着 i 拉回到 e 的可缩映射 f。对于相反的情况，考虑上述的提升问题，并假设等价扩展性质成立。根据引理 3.5.1，映射 e￣ 分类了在 A 中的可缩映射 e，而 q￣1 分类了在 B 中的一个纤维化 q1，后者沿着 i 拉回到 e 的值域。根据等价扩展性质，等价性扩展到在相同宇宙级别上与 q1 的等价映射 f。使用给定的宇宙及其相关的纤维化概念的相对无环性，我们获得了一个分类映射 q￣1，使得分类映射的外矩形是交换的：实际上，由于纤维化 ????[π1?π,π2?π]U×U:MapU×U(π1?U˙,π2?U˙)?U×U 的泛性质和图 (3.3.2) 的交换性，图的内部也是交换的。因此，我们原来的提升问题可以按照如下方式解决：并且可以通过引理 3.5.2 解决，它将 f 上的等价结构与 e 上的对齐。

3.6. 上纤维化宇宙：接下来我们介绍一个公理化设置，允许我们使用命题 3.5.5 推断纤维化的宇宙 π:U→U 具有上纤维化的基底对象 U。我们的论点遵循 [1, 2.12] 中的论述。假设 E 具有一个 (上纤维化, 平凡纤维化) 弱分解系统，其中每个对象都是上纤维化的，并且让 P:E→E 是一个保持有限乘积的内射函子，配备了自然的收缩，即 ?:id?P 和 δ:P?id 使得 δ??=id。例如，P 可以是一个伴随函子圆柱的 cocylinder 部分，δ 可以是 ?0 或 ?1。例如：对于笛卡尔封闭范畴 E 中的任何对象 I，我们在切片 E/I 中有一个图，表示 I 拉回到切片上的终端对象作为一个收缩。这里 δ 是对角映射，? 是通过将 I→1 拉回到切片上得到的乘积投影。通过对这些对象进行指数运算，可以定义一个内函子 P:E/I→E/I，以及自然变换 ?:id?P 和 δ:P?id，使得 δ??=id。所谓对象 X 上的反射关系 R?X，我们指的是对角线的某种分解：注意我们不要求规范配对 (s,t):R→X×X 是单射。

**定义 3.6.2**：对于反射关系 R?X，一个 δ-收缩子是一个映射 c:PX→PR，它使得以下图表交换：

**注解 3.6.3**：为了直观理解这个定义，假设我们处于拓扑环境中，并且 PX=XI 是路径空间函子，? 是恒等路径操作，δ 在某个固定点 i∈I 处评估路径。δ-收缩子 c 接收一个从 x0 到 x1 的路径 p，并生成一个如下所示的正方形图，其中水平箭头代表路径，垂直箭头代表关系 R 的见证者，xi 是 p 在 i 处的值：

- 第一个图表确定了水平箭头：它要求 c 是一个将 p 与恒等路径 ?(xi) 相关联的见证者路径。
- 第二个图表要求 c 在 i 处的值（将 xi 与自身相关联）是关系 R 的反射性。

**引理 3.6.4**：设 R?X 是一个反射关系。如果 δ 对于 (s,t):R→X×X 的莱布尼茨拉回应用是一个平凡纤维化，则 R 有一个 δ-收缩子。

**证明**：3.6.2 中所需的图表可以重新打包成一个单一的提升问题。但是垂直映射是所述的莱布尼茨拉回应用 δ°?(s,t)，假设这是一个平凡纤维化，因此存在所指示的提升 c，因为所有对象都是余纤维化的。

**引理 3.6.5**：设 R?X 是一个具有 δ-收缩子的反射关系。将正方形图视为一个态射 t→!X。在这个态射下的莱布尼茨拉回应用的结果是一个分裂的全射。

**证明**：右边的规范正方形图允许一个截面。δ-收缩子的概念正是这样的一个截面。

**引理 3.6.6**：设 R?X 是一个反射关系，并且 δ 对 (s,t):R→X×X 和 t:R→X 的莱布尼茨拉回应用都是平凡纤维化。那么 δX:PX→X 也是一个平凡纤维化。

**证明**：注意到 δX:PX→X 是 δ 对 !X:X→1 的莱布尼茨拉回应用。根据引理 3.6.4 和引理 3.6.5，δ°?!X 是 (Pt,δR)=δ°?t 的一个收缩子，因此是一个平凡纤维化。

**当纤维化是以特定方式从平凡纤维化创建时，引理 3.6.6 可以用来证明允许适当反射关系的对象 X 的纤维性。为了后续使用，我们引入以下一般定义。**

**定义 3.6.7**：设 E 是一个（局部）笛卡尔封闭范畴，其中有一类平凡纤维化。
- 相对于区间对象 δ0，δ1:1→I 在 E 中，有偏纤维化是指那些通过 δ0 和 δ1 的莱布尼茨指数运算之后仍然是平凡纤维化的映射。
- 相对于对象 I∈E，无偏纤维化是指那些它们在 I 上的切片中的拉回通过对角线 δ:I→I×I 的莱布尼茨指数运算之后仍然是平凡纤维化的映射。

**命题 3.6.8**：设 E 是一个具有预模型结构的笛卡尔封闭范畴，其中的纤维化是相对于区间对象定义的有偏纤维化。那么如果对象 X 具有反射关系 s,t:R?X，使得 (s,t):R→X×X 和 t:R→X 都是纤维化，那么 X 是纤维化的。

**证明**：如例 3.6.1 中所述，通过区间的指数运算定义了一个内函子（?）I，并配备了自然收缩 ?:id?（?）I 和 δ0,δ1:(?)I?id。分别应用引理 3.6.6 到 δ0 和 δ1，我们可以看到 (δ0)X=δ0°?!X 和 (δ1)X=δ1°?!X 都是平凡纤维化，从而证明 X 是纤维化的。

**命题 3.6.9**：设 E 是一个具有预模型结构的笛卡尔封闭范畴，其中的纤维化是相对于对象 I 定义的无偏纤维化。那么如果对象 X 具有反射关系 s,t:R?X，使得 (s,t):R→X×X 和 t:R→X 都是纤维化，那么 X 是纤维化的。

**证明**：正如例 3.6.1 中所示，通过区间的指数运算定义了一个内函子（?）I。根据引理 3.6.4 和引理 3.6.5，δ°?!X 是 (Pt,δR)=δ°?t 的一个收缩子，因此是一个平凡纤维化。

**当我们从平凡纤维化以特定方式创建纤维化时，引理 3.6.6 可以用来证明允许适当反射关系的对象 X 的纤维性。为了后续使用，我们引入以下一般定义。**

**定义 3.6.7**：设 E 是一个（局部）笛卡尔封闭范畴，其中有一类平凡纤维化。
- 相对于区间对象 δ0,δ1:1→I 在 E 中，有偏纤维化是指那些通过 δ0 和 δ1 的莱布尼茨指数运算之后仍然是平凡纤维化的映射。
- 相对于对象 I∈E，无偏纤维化是指那些它们在 I 上的切片中的拉回通过对角线 δ:I→I×I 的莱布尼茨指数运算之后仍然是平凡纤维化的映射。

**命题 3.6.8**：设 E 是一个具有预模型结构的笛卡尔封闭范畴，其中的纤维化是相对于区间对象定义的有偏纤维化。那么如果对象 X 具有反射关系 s,t:R?X，使得 (s,t):R→X×X 和 t:R→X 都是纤维化，那么 X 是纤维化的。

**证明**：如例 3.6.1 中所述，通过区间的指数运算定义了一个内函子（?）I，并配备了自然收缩 ?:id?（?）I 和 δ0,δ1:(?)I?id。分别应用引理 3.6.6 到 δ0 和 δ1，我们可以看到 (δ0)X=δ0°?!X 和 (δ1)X=δ1°?!X 都是平凡纤维化，从而证明 X 是纤维化的。

**命题 3.6.9**：设 E 是一个具有预模型结构的笛卡尔封闭范畴，其中的纤维化是相对于对象 I 定义的无偏纤维化。那么如果对象 X 具有反射关系 s,t:R?X，使得 (s,t):R→X×X 和 t:R→X 都是纤维化，那么 X 是纤维化的。

**证明**：正如例 3.6.1 中所示，通过区间的指数运算定义了一个内函子（?）I。根据引理 3.6.4 和引理 3.6.5，δ°?!X 是 (Pt,δR)=δ°?t 的一个收缩子，因此是一个平凡纤维化。

**我们现在将这些观察结果与前一节的构造结合起来，以证明在这些假设的条件下，宇宙是一个纤维化对象。**

**命题 3.6.10**：假设 E 是一个具有圆柱形预模型结构的预层拓扑，其中余纤维化是单射。如果纤维化如命题 3.6.8 或 3.6.9 中所述，并且具有宇宙，则 universal 几何 π:U˙?U 的基底是纤维化对象。**

**证明**：根据引理 3.5.1，纤维化 π:U˙?U 产生了一个反射关系 Eq(U˙)?U，其配对 Eq(U˙)?U×U 是一个纤维化。根据定理 3.3.3，等价扩展性质成立，因此根据命题 3.5.5，映射 π:U˙?U 是一个平凡纤维化。现在，无论是命题 3.6.8 还是 3.6.9 都适用，可以得出 U 是纤维化的结论。

**3.7. 纤维化扩展性质和 2-of-3**：回顾定义 2.3.6，它介绍了预层拓扑上的预模型结构具有宇宙的含义。我们说一个预模型结构具有纤维化宇宙，如果对于每个足够大的不可达基数 κ，每个宇宙的基底都是纤维化的。

**本节的目的是将宇宙的纤维性与预模型结构的一个有用性质联系起来。**

**定义 3.7.1**：一个预层拓扑上的预模型结构满足纤维化扩展性质，当且仅当对于每个足够大的不可达基数 κ，任何 κ-小的纤维化 p:X?A 和平凡余纤维化，都存在一个在 B 上的 κ-小纤维化，它沿着 t: 重新拉回到 p。**

**纤维化扩展性质和宇宙的纤维性之间存在一种众所周知的联系 [84]，我们在此详细说明，因为我们在这里使用的是稍不同的公理化。**

**引理 3.7.2**：任何一个具有纤维化宇宙的预层拓扑上的预模型结构都具有纤维化扩展性质。反之，如果一个具有纤维化扩展性质的预模型结构具有宇宙，那么这些宇宙的基底对象是纤维化的。**

**我们首先证明纤维化宇宙意味着纤维化扩展性质。对于任何纤维化 p:X?A，我们有一个分类宇宙 π:U˙?U，其基底 U 是纤维化的。特别是，这个选择定义了一个分类映射，因此是一个有解的提升问题，因为 U 是纤维化的。π 沿着这个映射的拉回在 B 上定义了一个小纤维化。**

**引理 3.7.3**：任何一个具有纤维化宇宙的预层拓扑上的预模型结构都具有纤维化扩展性质。相反，如果一个具有纤维化扩展性质的预模型结构具有宇宙，那么这些宇宙的基底对象是纤维化的。**

**首先我们证明纤维化宇宙意味着纤维化扩展性质。对于任何纤维化 p:X?A，我们有一个分类宇宙 π:U˙?U，其基底 U 是纤维化的。特别是，这个选择定义了一个分类映射，因此是一个有解的提升问题，因为 U 是纤维化的。**

**现在我们可以利用 [39] 中的以下结果，其证明完全是公理化的。**

**命题 3.7.3 [39, 3.31]**：设 E 是一个所有对象都是余纤维化的圆柱形预模型范畴。如果纤维化扩展性质成立，那么弱等价关系满足 2-of-3 条件。**

**因此，从具有所有对象都是余纤维化的圆柱形预模型范畴构造同伦类型论模型和 Quillen 模型结构是相互交织的。首先检查等价扩展性质，这是解释不可交换性的核心。然后证明 Frobenius 条件，这提供了 Π-类型的解释，并与模型结构的正确性有关。等价扩展性质和 Frobenius 条件也可以在纤维化宇宙的构造中发挥作用。除了解释类型论的宇宙之外，纤维化宇宙还可以用来推导纤维化扩展性质，从而得到模型结构。在后续中，我们看到了这个故事的两个版本，都表明圆柱形预模型结构是一个模型结构，首先是在立方体物种中，然后是在立方体集合中。**

**4. 在立方体物种上的区间模型结构**：在一个具有适当区间对象的预层拓扑上，现在有一种众所周知的策略来定义一个模型结构，该结构模拟同伦类型论。余纤维化是单射，使得平凡纤维化是定义 2.2.12 中的那些。然后从平凡纤维化定义纤维化，作为有偏或无偏纤维化，如定义 3.6.7.9 中所述。前一节的结果适用于建立等价扩展性质、Frobenius 条件、纤维化扩展性质、宇宙的不可交换性和纤维性，并验证弱等价的 2-of-3 条件。**

**在这里，我们不是在立方体集合的范畴中应用这个大纲，而是在 §4.2 中引入的立方体物种的范畴中应用，该范畴具有适当的“对称”区间对象。立方体物种的范畴是一个以立方体集合为值的群体索引函子的范畴，因此在 §4.1 中我们首先讨论了一些关于子对象分类器、推进和微小对象的一般结果，这些结果适用于那种一般设置。在 §4.3 中，我们建立了立方体物种上的圆柱形预模型结构。然后在 §4.4 中，我们应用 §3 中的结果来证明这个预模型结构是一个模拟同伦类型论的模型结构。**

**4.1. 以群体索引的图表类别**：我们收集了一些关于以群体索引的图表类别的陈述。实际上，前几个结果更一般地适用于以类别索引的图表。**

**引理 4.1.1**：在一个基 category E 具有拉回的图表类别 EC 中，考虑一个笛卡尔自然变换 f:Y→X。在对象 c:1→C 处，评估函子 family ?c?:EC→E 创建了沿着 f 的推进。**

**证明**：EC 在 X 上的切片是索引在 c∈C 上的类别 E/X(c) 的松弛双极限，其函子作用由拉回给出，Y 也是如此。对于每个 u:c→d 在 C 中，存在规范同构 ????fc?Xu??Yu?fd?，在粘贴下保持一致性。因此，拉回函子 ?f?:E/X→E/Y 由沿 f 的组件的拉回的松弛双极限的函子性质给出。由于 f 在 u 处的自然性平方是一个拉回，其配对 ??(Yu)!fc?→fd?(Xu)! 是可逆的。由于伴随性，配对 ????Xu?(fd)?→(fc)?Yu? 也是可逆的，假设我们沿着 f 的组件有推进。因此，每个级别的拉回-推进伴随形成一个索引伴随。由于松弛双极限的双函子性质，这给出了沿着 f 的拉回的右伴随。**

**引理 4.1.2**：在一个基 category E 具有二元积的图表类别 EC 中，考虑一个具有可逆函子作用的图表 A。在对象 c:1→C 处，评估函子 family ?c?:EC→E 创建了与 A 的指数运算及其右伴随。**

**证明**：我们的论证与之前的证明类似。与 A 的积是通过在 c∈C 处的积和映射 (?)×A(c)→(?)×A(d) 对于 u:c→d 的可逆性给出的，假设 Au 是可逆的。假设逐级的指数运算，诱导的映射在右伴随 (?)A(d)→(?)A(c) 是可逆的。假设进一步增强右伴随 (?)A(c)?(?)A(c) 对于 c∈C，因此诱导的映射 (?)A(c)→(?)A(d) 也是可逆的。松弛双极限的双函子性质给出了所需的右伴随 (?)A 和 (?)A。**

**引理 4.1.3**：考虑一个具有拉回和子对象分类器 1→Ω 的类别 E，以及常量图表函子 Δ:E→EC。然后 Δ1→ΔΩ 分类了在 EC 中定义笛卡尔自然变换的单射。**

**证明**：注意笛卡尔自然变换在拉回下是封闭的，且所声称的分类器是其中的一个。给定一个逐组件的单射笛卡尔自然变换，其逐级的分类图通过拉回粘贴组装成一个（唯一的）分类图。由于 E 具有拉回，EC 中的单射是逐组件的单射。**

**对于一个群体 G，每个从 G 到 E 的函子都有可逆的函子作用，这些函子之间的每个自然变换都是笛卡尔的。因此：**

**推论 4.1.4**：考虑一个局部笛卡尔封闭的类别 E。对于每个群体 G，函子类别 EG 是局部笛卡尔封闭的。对于每个函子 F:G→H 在群体之间，限制 ?F?:EH→EG 保持推进。**

**推论 4.1.5**：考虑一个笛卡尔封闭的类别 E。对于每个群体 G，如果对象 A∈EC 是逐组件的微小的，那么 A 是微小的。对于每个群胚之间的函子 F:G→H，限制函子 ?F?:EH→EG 保持了对分量级小对象的自乘运算。□

推论 4.1.6 考虑一个具有子对象分类器的有限完备范畴 E。对于每个群胚 G，函子范畴 EG 都具有子对象分类器。对于每个群胚之间的函子 F:G→H，限制函子 ?F?:EH→EG 保持子对象分类器。□

4.2. 立方物种和对称区间
“立方”一词在“立方物种”中指的是下面定义的笛卡尔立方体范畴。在 Buchholtz 和 Morehouse 对立方体范畴的分类中 [25]，这是 C(wec,?)。

定义 4.2.1 笛卡尔立方体范畴是与有限严格双端点集和双端点映射的范畴相反的范畴。它的对象是形如 {⊥,1,…,n,?} 的双端点集，其中 n≥0。我们用 表示预层的拓扑，称其对象为（笛卡尔）立方体集。在 Yoneda 嵌入下，对象 {⊥,1,…,n,?} 被识别为 n 维立方体 In。根据 Yoneda 引理，态射 α:Im→In 对应于函数 α:{⊥,1,…,n,?}→{⊥,1,…,m,?}，这些函数保持基点 ⊥ 和 ?。

设 是立方体范畴中的最大子群胚，但不包括第 0 维立方体的恒等自同构（原因在注释 4.3.17 中解释）。这里 是与对称群 Σk 相关联的单元素群胚，它通过对索引进行排列来作用于 {⊥,1,…,k,?}，从而作用于可表示的立方体集 Ik。

定义 4.2.2 立方物种是一个在 上的值函子。

将立方物种表示为立方体集的对称序列是方便的，即表示为一个族 X=(Xk)k≥1 的立方体集，其中每个 Xk 都具有指定的 Σk-作用。实际上，作为一个范畴，如果在单个因子中非空的立方物种被称为在度数 k 上集中的。

设 是沿着 的左 Kan 扩展，它是函子 的左伴随函子，它将立方物种投影到第 k 个分量，并忘记作用：

定义 4.2.3 对于 k≥1，k-自由的立方物种是一个形式为 FkX 的立方物种，其中 X∈cSet。具体来说，k-自由的立方物种 FkX 在度数 k 上集中，并在立方体集 X×Σk 上具有自由的 Σk-作用。

我们强调两个特别重要的立方物种示例：

示例 4.2.4 由对象 对组成的可表示立方物种，是在度数 k 上集中的自由立方物种 FkIn，由立方体集 In×Σk 和自由的 Σk-作用给出。

示例 4.2.5 沿着包含关系 在陪域变量中的全双函子 的限制定义了一个立方物种 I，其第 k 个分量是几何 k-立方体 Ik 及其规则作用，即排列 k 个维度。

注释 4.2.6 对称区间 I 有 2ω 个点：对于任何可数的 0 和 1 的序列 v→，都有一个对应的点 选择每个分量中的初始或最终顶点。由于终端立方物种 在每个分量中的作用是平凡的，因此区间内的所有点都是对称群坐标作用的不动点。

引理 4.2.7 立方物种 I 是微小的。证明：回想一下 是可表示的。由于 具有二元乘积，在 cSet 中的可表示对象是微小的。现在根据推论 4.1.5，I 是微小的。□

4.3. 立方物种上的圆柱形预模型结构
我们确定了一对（代数的）弱分解系统，这些系统构成了立方物种上的预模型结构，并证明它是圆柱形的，其伴随函子圆柱体由区间对象表示，其中点 δ0,δ1 对应于注释 4.2.6 中的常数序列 0→,1→。

作为一个预层拓扑，范畴 具有子对象分类器，我们可以如下明确描述。

引理 4.3.1 对于 n,k∈N，k≥1，子对象分类器 的元素 与 n-立方体中的子对象 c:C?In 一一对应。证明：根据定义，一个元素 对应于可表示立方物种 FkIn 的一个子对象。由于 FkIn 在度数 k 上集中并且具有自由的 Σk-作用，它的子对象也必须具有这些属性。因此，我们看到子对象的形式为 Fkc:FkC?FkIn，其中 c 是 n-立方体中必然唯一的子对象。

定义 4.3.2 作为余纤维化，我们取单射，它们由子对象分类器 分类（直到等价）。然后平凡的纤维化是具有对所有单射的右提升性质的映射。

正如我们在 §2.2 中看到的，余纤维化和平凡纤维化构成了一个弱分解系统。根据引理 2.2.10，我们可以将平凡纤维识别为局部可表示和相对无环的纤维结构 TF 的基础类。

我们现在转向（平凡的余纤维化，纤维化）弱分解系统。纤维化将是定义 3.6.7(ii) 中的无偏纤维化——见定理 4.3.14——我们现在将它们明确描述。纤维化将由平凡纤维化决定，通过使用通用子对象 和“通用点” δ:I→I×I 的 Leibniz 拉回应用实现 ev:(?)I×I?(?)。等价地，我们可以将它们描述为通过使用通用子对象 和“通用点” δ:I→I×I 构建的生成平凡余纤维化的范畴的右提升得到的。

定义 4.3.3 作为切片范畴中的映射，对角线 δ:I→I×I 定义了 I 的一个额外点，称为通用点。

中的态射 和 δ:I→I×I 可以重新索引到共同的切片中。它们在那里的推出积定义了一族映射 ，这些映射由对象 内在索引：我们的生成平凡余纤维化范畴将通过外部化族 来给出。

注释 4.3.4 由于通常 ∫X1?X，并且元素范畴 λ 保持拉回，一个乘积的元素范畴是元素范畴的拉回：现在 I 是全双函子的限制，因此其元素范畴是扭曲箭头范畴的限制。因此， 中的元素是对 (c,ζ) 的对，如下垂直显示，而 (α,σ):(d,ξ)→(c,ζ) 在立方体集的图表交换时定义一个态射，顶部的平方是一个拉回：

(4.3.4) 如注释 4.3.4 所观察到的， 的元素与映射 一一对应，其中 分类了立方体集 In 的子对象 c:C?In，而 ζ:FkIn→I 通过伴随对应于映射 ζ:In→UkI?Ik。因此，我们将 中的元素视为可组合的立方体集映射对，我们称它们为三角形。

构造 4.3.5 由对象 内在索引的映射族可以外部化为由 的元素范畴外部索引的函子，并通过将给定的内部映射族拉回到可表示对象来定义。笛卡尔函子 J 将 Yoneda 嵌入 从与函子 的元素范畴相关联的离散纤维化提升到陪域纤维化：具体来说，函子 J 将元素 (c,ζ) 发送到沿着它的通用元素 ?×?δ 的拉回，如下所示：结果映射 ?J(c,ζ)=(χc,ζ)?(?×?δ) 也可以通过将子对象 Fkc:FkC?FkIn 和通用点 δ:I→I 作为映射在切片上的拉回到来计算。

注意映射 δ 沿着 (χc,ζ) 拉回以定义图表 (FkC,ζ?Fkc):FkC→FkC×I，类似地 也拉回以定义 ζ:FkIn→I 的图表。因此，对于任何映射 γ:A→B，我们将其图表 (A,γ) 写为 [γ]:A→A×B。

中的态射 对应于 (4.3.5) 中的 α:Im→In 和 σ∈Σk。函子 J 将这样的态射映射到下面的立方物种的拉回平方：

(4.3.5) 我们将 函数 J 在图像中的子对象称为开框，尽管将“盖子” FkIn 粘合到“箱子” FkC×I 的性质有些微妙，因为它涉及到映射 ζ:FkIn→I。开框本身是拉回乘积，根据以下一般引理。

引理 4.3.6 如果 i 是 X 上的切片中的态射，j 是 Y 上的切片中的态射，并且 (x,y):Z→X×Y，那么 i 和 j 在 X×Y 上的切片中的拉回产物沿着 (x,y) 拉回到在 Z 上的映射，作为 i 和 j 的明显拉回的拉回产物。

推论 4.3.7 开框是在 FkIn 上的映射的拉回产物。

注释 4.3.8 由于可表示对象集中在单一度数上，每个开框也是如此。下面左边的“三角形”立方体集——其中第一个映射是一个态射，第二个映射是在可表示对象之间的映射——产生了下面中心处的“开框”立方物种，在度数 k 上集中：这个映射的非空分量是上面右边的 Σk-立方体集的映射，由下面的拉回定义：这里 Σk 在 C 和 In 上的作用是平凡的；通过在 Σk 上的左乘；以及通过在 Ik 上排列维度——“规则”作用。映射 [ζΣk]:In×Σk→In×Σk×Ik 是 ζ:In×Σk→Ik 的扭曲版本的图表：顶部右边的映射类似定义。注意，在拉回图中，映射都是 Σk-等变的。

类似地，拉回平方 (4.3.7) 在度数 k 上集中，并且其形式为 ，其中 σ:Σk→Σk 是通过右乘定义的。注意这些定义使得映射 α×σ×1:Im×Σk×Ik→In×Σk×Ik 成为一个 Σk-等变映射。

定义 4.3.9 Garner 的代数小对象论证 [42] 在 上提供了一个代数弱分解系统，该系统在 上是代数自由的，即其单子代数范畴由 给出。特别是，一个右映射是具有对开框的统一提升的立方物种的态射 f:Y→X。

我们现在展示这些纤维化是无偏纤维化。

定义 4.3.10 给定一个映射 f:Y→X，通过在 I 上的切片中与 δ 形成 Leibniz 指数来定义参数化路径空间：'

(4.3.10) 其中 ev:YI×I→Y 是评估。等价地，映射 ev°?f 可以通过上面的拉回来定义，在 I 的切片中不是形成的。

根据这两种表征中的第二种，ev°?f 是评估自然变换对映射 f 的 Leibniz 拉回应用，这解释了我们的符号。这个函子不是右伴随的，因为它不保持终止对象。然而，根据分解，它是右伴随与遗忘函子 Σ 的组合。特别是，它保持拉回。

定理 4.3.11 统一纤维化范畴 是沿着参数化路径空间函子 的统一平凡纤维化范畴的拉回：特别是，如果一个立方物种的映射 f:Y→X 是一个无偏纤维化，那么它就是一个纤维化，即使参数化路径空间映射是一个平凡纤维化。

证明：统一纤维化范畴是由针对生成范畴的定义 2.2.13 中的箭头范畴的右提升定义的。根据构造 2.2.13，函子 J 是顶部水平复合：因此，根据伴随， 是一个统一纤维化当且仅当它在 上的右提升。由于切片范畴中的提升问题是通过遗忘函子创建的解决方案，如果 是一个统一平凡纤维化，那么情况就是这样。

定理 4.3.11 代数弱分解系统的左映射满足额外的封闭属性，这些属性源于余单子函子创建余极限 [23]。特别是，在箭头范畴中的余极限是通过生成范畴分解的图表是平凡的余纤维化。以下引理提供了这种范式的一个例子。

引理 4.3.12 对于 I 的任何 2ω 个点 ?→，映射 是一个平凡的余纤维化。

证明：对于任何顶点 v→∈Ik，我们有一个三角形 (4.3.12) 右边的 Σk-立方体集的映射将 σ∈Σk 发送到对 (σ,σ?v→)。然而，回想一下注释 4.2.6，I 的一个点是通过为每个分量选择点 0→:1→Ik 或 1→:1→Ik 来指定的。注意这些是 Σk-立方体集 Ik 中的唯一两个点，因为底层立方体集中的其他点是通过规则作用排列的。相比之下，由于这些点是固定的，我们对每个 σ∈Σk 有自同构。因此 Σkop 作用于开框 [0→]:Fk1?Fk1×I 和 [1→]:Fk1?Fk1×I，这些自同构位于生成范畴中。余极限产生了在 Σk-立方体集 Ik 中的映射 0→:1→Ik 和 1→:1→Ik，其中陪域具有规则作用。因此，这些映射是平凡的余纤维化。在每个组成部分中选择适当的平凡余纤维化，并在立方体物种中形成它们的余积，就得到了点包含映射 v→:1→I。□我们已经定义了（余纤维化，平凡纤维化）和（平凡余纤维化，纤维化）代数弱分解系统，每个系统都有明确的生成元范畴。根据命题2.2.11，平凡纤维化可以自然地提升到（平凡余纤维化，纤维化）awfs的生成范畴，因此平凡纤维化是纤维化，平凡余纤维化是余纤维化。这些底层弱分解系统因此为立方体物种的范畴配备了一个称为区间预模型结构的预模型结构。如§3.1中所述，我们定义立方体物种的弱等价映射为那些可以表示为平凡余纤维化后跟平凡纤维化的映射。

注4.3.13：如果我们 在定义中包括了0-立方体的恒等自同构，即在立方体物种中添加一个k=0的组成部分，我们也会得到类似的结果。如果我们这样做了，那么请注意，在k=0的组成部分中，所有的映射都是纤维化，因为（4.3.13）中的外部平方的组成部分都是拉回。因此，在k=0的组成部分中，唯一的平凡纤维化将是同构映射，这意味着弱等价类的集合将与其他组成部分中的平凡纤维化类的集合相同，后者被定义为能够提升到单射映射的映射。但是这个类显然不满足2-of-3的性质，因为它不满足左取消律，所以如果我们在定义中包含了k=0的组成部分，我们的预模型结构就无法定义一个模型结构。然而，预模型结构仍然足以在第5.1节中定义等变立方集的模型结构。

接下来，我们验证区间预模型结构是笛卡尔幺半群的。我们预期这个性质可以被结构化：即立方体物种的范畴上的笛卡尔闭结构可以定义两个变量伴随的代数弱分解系统[76]，但由于我们没有这个结果的应用，因此在这里不再继续探讨。

命题4.3.14：余纤维化的拉出积是余纤维化，而余纤维化与平凡余纤维化的拉出积是一个平凡余纤维化。证明：由于余纤维化在预层范畴中是单射，第一个性质根据注释2.2.2是成立的。剩余的陈述等价于断言，对于一个fiberation f:Y→X和一个单射 c:C?Z，其Leibniz指数 {c,f}? 是一个fiberation。根据定理4.3.14，这等价于断言在切片δ:I→I×I上的Leibniz指数 {c,f}?×I是一个平凡纤维化，并且这个平凡纤维化能够提升到切片I上的所有单射u:J→K。由于{c,f}? 在切片I上的拉回与在切片I上的c×I和f×I的拉回的Leibniz指数是同构的，因此我们等价于解决在切片I上c×I和u之间的提升问题，以及Leibniz指数?ev°?f?{δ,f×I}?I。由于假设f是一个fiberation，ev°?f是一个平凡纤维化，所以只需验证单射c×I和u在I上的拉出积是一个单射。这同样根据注释2.2.2是成立的。□最后，我们观察到区间预模型结构是圆柱形的，满足定义3.1.8的公理，使用伴随函子（?）×I?（?）I来定义一个伴随函子圆柱形。

引理4.3.15：立方体物种上的区间预模型结构是圆柱形的。证明：由于区间I的端点0→和1→是不相交的，因此余配对是一个单射，因此是一个余纤维化。根据引理4.3.15，单个端点的包含映射是平凡余纤维化。现在结果根据命题4.3.18得出。□

4.4. 立方体物种的模型同伦类型论：在本节中，我们应用第3节的结果来验证立方体物种上的区间预模型结构的类型论性质，这些性质表明它是一个具有同伦类型论模型所需额外特征的Quillen模型结构。区间预模型结构中的余纤维化正是单射，根据注释2.2.2，它们在所有切片中的拉出积下是封闭的。结合引理4.3.19，这验证了定理3.3.3的假设，因此：

命题4.4.1：立方体物种上的区间预模型结构满足等价扩展性质。□

同样，纤维化的定义符合命题3.4.2的形式，因此：

命题4.4.2：立方体物种上的区间预模型结构具有Frobenius性质。□

剩余的性质需要类（universes），我们现在将构造这些类。根据定理4.3.14，均匀纤维化被确定为平凡纤维化的某种拉回。我们使用这个结果来定义一个局部可表示且相对无环的纤维化结构F，并对均匀纤维化进行分类。

引理4.4.3：存在一个局部可表示且相对无环的纤维化结构F，即均匀纤维化结构，其底层映射类是纤维化类。证明：我们应用引理2.1.16。也就是说，我们定义f:Y→X上的一个均匀纤维化结构为ev°?f上的均匀平凡纤维化结构，ev°?f是评估自然变换的Leibniz拉回应用。由于区间I很小，函子X?XI×I有一个右伴随函子：由于引理2.2.10告诉我们纤维化结构TF是局部可表示且相对无环的，引理2.1.16告诉我们均匀纤维化也是如此。□

实例化构造2.3.3：构造4.4.4：对于足够大的κ，我们通过定义?Uκ?Fκ(?)并形成拉回来定义一个κ-小的纤维化分类器π:U˙κ→Uκ，其中?:V˙κ→Vκ是在预层topos中分类κ-小族的Hofmann–Streicher类。

根据命题2.3.5：

命题4.4.5：对于足够大的不可达基数κ，立方体物种上的区间预模型结构在纤维化分类器π:U˙κ→Uκ的意义上具有类（universes）。□

根据命题4.4.5和命题4.4.2，我们已经满足了命题3.5.5的假设，因此从命题4.4.1我们可以得出：

命题4.4.6：立方体物种上的区间预模型结构中的类（universes）是单价的。□

根据定义4.3.12和定理4.3.14，我们的纤维化按照命题3.6.9的要求进行了表征。因此命题3.6.10适用，我们可以得出：

命题4.4.7：立方体物种上的区间预模型结构的均匀纤维化的基础是纤维化对象。□

通过应用引理3.7.2，我们看到：

命题4.4.8：区间预模型结构满足纤维化扩展性质。□

这些结果构成了本节的主要定理。

定理4.4.9：立方体物种的范畴允许一个Quillen模型结构，在这个结构中，余纤维化是单射，而纤维化是3.6.7(ii)中的无偏纤维化。这个模型是圆柱形的且笛卡尔闭的，并满足Frobenius条件、等价扩展性质和纤维化扩展性质。此外，它具有基数是纤维化对象的单价类。证明：我们尚未证明的唯一结果是区间预模型结构实际上是一个模型结构，但这根据命题3.7.3、命题4.4.8以及所有对象都是余纤维化的事实可以正式得出。□

因此，立方体物种的topos上的区间模型结构是一个同伦类型论的模型。

5. 立方体集上的等变模型结构：在立方体物种的范畴上建立了模型结构后，我们现在将其转移到笛卡尔立方体集的范畴cSet上，形成一个模型结构和一个同伦类型论的模型。§4的结果既为这一节中的构造提供了概念上的依据，也简化了许多证明。在§5.1中，我们引入了立方体集和立方体物种之间的函子伴随三元组，并建立了这些函子的基本性质。在§5.2中，我们使用常量图函子将立方体物种上的圆柱形预模型结构提升到立方体集上，从而创建了纤维化和平凡纤维化。我们给出了这些类的明确表征，揭示了平凡纤维化再次是§2.2中的平凡纤维化，而纤维化是新颖的，定义了一类我们称之为等变纤维化的映射。

由于在立方体集上得到的预模型结构中的余纤维化仍然是单射，这些也是由函子Δ创建的，但是平凡余纤维化和弱等价不是，特别是证明右提升的预模型结构实际上定义了一个Quillen模型结构需要一些工作。这在§5.3中完成，证明了立方体集的定理4.4.9的类比。对于一些组成结果，证明是形式化的，专门化了§3的结果；对于其他陈述，该节的结果不适用，我们则利用了§4的结果。

5.1. 从立方体物种到等变立方体集：立方体集的范畴通过常量图函子忠实地嵌入到立方体物种的范畴中，尽管在整个范畴上只是忠实的。由于群胚是小的且cSet是bicomplete的，这个函子允许左伴随和右伴随：

左伴随L取群胚上的余极限，右伴随Γ取极限。具体来说，对于一个立方体物种X=(Xk)k≥1，我们有??L(X)??k≥1X/ΣkkΓ(X)?∏k≥1(Xk)Σk，其中X/Σkk是Σk-立方集Xk在其作用下的商，而(Xk)Σk是Σk-固定点的立方集。

作为由群胚作用下的范畴，topos在cSet上被认为是原子的，并且作为逻辑函子，它保持（co）极限、子对象分类器和局部笛卡尔闭结构。我们提供了一些具体的计算。

例5.1.1：对于n,k∈N且k≥1，我们有L(FkIn)?In，反映了左Kan扩张保持可表示对象的事实。更一般地，对于任何立方体集X，我们有L(FkX)?X，因为L?Fk是恒等函子的左伴随。

例5.1.2：我们计算L(I)??k≥1I/Σkk和Γ(I)?∏k≥1I?Iω，使用事实（Ik）Σk?I对所有k>0都成立。

左伴随L远非左精确的，因为它不保持拉回（因为群作用的1-范畴商不与拉回交换），甚至不保持有限积（因为余积不与有限积交换）；然而，它与涉及常量立方物种的某些有限极限交互得很好。

推论5.1.3：常量图函子保持向前和指数。证明：这是推论4.1.4的一个实例。□

引理5.1.4：常量图函子保持子对象分类器并创建单射。证明：保持子对象分类器是推论4.1.6的一个实例。关于创建单射，回想一下在中的单射是逐点定义的，并且Σ是可居住的。□

推论5.1.5：常量图函子保持第2.2节中的（相对）部分映射分类器ηX:X→X+，因此也保持（相对）+-代数。由于它是忠实的，Δ也反映了后者。□

5.2. 立方体集上的圆柱形预模型结构：通过一个众所周知的转移程序，我们可以通过沿着右伴随将立方体物种上的预模型结构转移到立方体集上得到一个预模型结构：我们说f在cSet中是一个（平凡）纤维化，如果Δf在中的是一个（平凡）纤维化。转移程序给出了左右类以及生成范畴，即原始弱分解系统的生成范畴在左伴随下的像。然而，请注意，我们不是机械地从中的纤维化得到cSet中的纤维化；我们必须“手工”构造这些，特别是我们希望以构造性的方式来做。

构造5.2.1：cSet中的平凡纤维化由构造2.2.1中的类别和顶部复合函子（5.2.1）生成。具体来说，根据例5.1.1，复合函子将一个元素发送到对应的子对象c:C?In，根据引理4.3.1，而中的形态作为下方左侧被带到子对象之间的拉回平方：注意函子在两个对象和形态上的像与参数无关。引理5.1.4的同构诱导了类别之间的同构，并且根据刚刚的观察，函子LI可以通过投影。因此，(5.2.2)中的复合矩形也可以如下分解：由于投影是一个满射，因此可以在cSet上给出一个平凡纤维化的生成范畴，该范畴可以更简单地表示为由cSet中的子对象分类器?:1?Ω内部索引的范畴。根据注释2.2.6和命题2.2.14，我们现在可以得出结论：余纤维化正好是单态射，而平凡纤维化是相对+-代数，即带有点的多项式自函子+X:cSet/X→cSet/X的代数，这也可以从推论5.1.5中看出。特别是，我们有一个（余纤维化，平凡纤维化）弱分解系统，其函子分解由注释2.2.6中的偏映射分解给出。接下来，我们将转移（平凡余纤维化，纤维化）弱分解系统。然而，这种情况更为微妙，因为平凡余纤维化的左类不能简单地通过常量图函子来反映。为了描述生成范畴中的映射，我们暂停观察一个有助于我们计算轨道的结果。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将对(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=?(e,g?1?s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

构造5.2.3 在cSet中的纤维化，我们称之为等变纤维化，是由范畴在复合下的像生成的：回想一下，根据注释4.3.4，该范畴的对象是成对的(c,ζ)，如下垂直显示，而(α,σ):(d,ξ)→(c,ζ)定义了一个态射，当且仅当立方体集合的图是交换的，并且顶部方块是一个拉回时：函子J将一个元素(c,ζ)发送到由立方体种类的推出来定义的立方体种类的态射，这对应于由Σk-立方体集合的推出来：左图在L下的像是通过传递到Σk-立方体集合图中的轨道来给出的，这可以使用引理5.2.3来计算。我们再次将函子J的像中的子对象称为开放盒子，尽管将“盖子”In粘贴到“盒子”C×Ik的性质有些微妙，因为它涉及到映射ζ:In→Ik。

函子J将态射(4.3.5)发送到立方体种类的拉回方块，这对应于Σk-立方体集合的拉回方块：使用引理5.2.3传递到轨道，这就得到了立方体集合的拉回图。我们再次将函子J的像中的子对象称为开放盒子，尽管将“盖子”In粘贴到“盒子”C×Ik的性质有些微妙，因为它涉及到映射ζ:In→Ik。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将对(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=?(e,g?1?s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

构造5.2.3 在cSet中的纤维化，我们称之为等变纤维化，是由范畴在复合下的像生成的：回想一下，根据注释4.3.4，该范畴的对象是成对的(c,ζ)，如下垂直显示，而(α,σ):(d,ξ)→(c,ζ)定义了一个态射，当且仅当立方体集合的图是交换的，并且顶部方块是一个拉回时：函子J将一个元素(c,ζ)发送到由立方体种类的推出来定义的立方体种类的态射，这对应于由Σk-立方体集合的推出来：左图在L下的像是通过传递到Σk-立方体集合图中的轨道来给出的，这可以使用引理5.2.3来计算。我们再次将函子J的像中的子对象称为开放盒子，尽管将“盖子”In粘贴到“盒子”C×Ik的性质有些微妙，因为它涉及到映射ζ:In→Ik。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将对(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=?(e,g?1?s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=?(e,g?1?s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

构造5.2.3 在cSet中的纤维化，我们称之为等变纤维化，是由范畴在复合下的像生成的：回想一下，根据注释4.3.4，该范畴的对象是成对的(c,ζ)，如下垂直显示，而(α,σ):(d,ξ)→(c,ζ)定义了一个态射，当且仅当立方体集合的图是交换的，并且顶部方块是一个拉回时：函子J将一个元素(c,ζ)发送到由立方体种类的推出来定义的立方体种类的态射，这对应于由Σk-立方体集合的推出来：左图在L下的像是通过传递到Σk-立方体集合图中的轨道来给出的，这可以使用引理5.2.3来计算。我们再次将函子J的像中的子对象称为开放盒子，尽管将“盖子”In粘贴到“盒子”C×Ik的性质有些微妙，因为它涉及到映射ζ:In→Ik。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=?(e,g?1?s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=?(e,g?1?s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么映射将集合S展示为G×S中的G-轨道的集合。
证明
首先观察到声明中的映射在由G集合G×S定义的G索引的集合图中定义了一个锥。对于任何g,h∈G和s∈S，h的作用将(g,s)发送到(h?g,h?s)，并且τ(h?g,h?s)=(h?g)?1?(h?s)=g?1?s=τ(g,s)。给定任何其他映射?:G×S→X，它在定义域中的G-轨道上是常量，我们通过τ定义了一个分解：由于(g,s)和(e,g?1?s)在同一个轨道上，?(g,s)=ψ?τ(g,s)。这种分解的唯一性是显而易见的，因为τ是一个满射。

引理5.2.2 设G是一个群，S是一个G-集合。考虑G集合G×S，其中G在G上自由作用，并通过其在S上指定的作用。那么这个论点运用了经典推理方法；参见上文第1.6.2节。我们的证明核心利用了这样一个事实：索引范畴和是Eilenberg–Zilber范畴，这是一种由Berger和Moerdijk [24]引入的特殊类别的（广义）Reedy范畴。为此，我们在第6.2节发展了一些关于Eilenberg–Zilber范畴的通用理论。特别是，在推论6.2.16中，我们证明了要检查一个以cSet或sSet为定义域的左Quillen函子之间的自然变换是否为自然弱等价，只需检查那些由它们的自同构群的商空间索引的组成部分。实际上，根据“两个中的三个”性质，如果这些对象是弱可缩的——就像在cSet上的等变模型结构和sSet上的经典模型结构中那样——那么这一点将自动成立。这些结果使得很容易证明一对对立的左Quillen函子在sSet和cSet之间定义了一个派生等价关系，因此我们寻求一个从sSet到cSet的左Quillen函子来定义三角化的候选逆函子。我们最初的证明是沿着以下思路进行的。在[82]中，Sattler观察到Dedekind立方体范畴的幂等化——即Cat中的一个完全子范畴，它包含在集合{0<1}n上（对于n≥0），并且为笛卡尔立方体添加了连接——是一个其对象为有限有界格，其态射为它们之间的单调映射的范畴。因此，预层范畴?Set与Dedekind立方体上的预层范畴是等价的，我们可以根据[29]为?Set配备模型结构。这一结果的实用性在于，有限序数[n]={0<11>?>n>?}的对偶，对于n≥0，其中⊥≠?，并且保持端点的有序映射的逆变同构。严格区间范畴显然是有限双点集的一个子范畴，因此定义了。函子i将外面映射δ0,δn:[n?1]→[n]映射到分别固定第一个立方坐标为?和最后一个立方坐标为⊥的面映射In?1→In。内面映射δi:[n?1]→[n]被映射到对角映射In?1→In，它将第i个和第(i+1)个坐标识别起来。退化映射σi:[n+1]→[n]被映射到从第(i+1)个坐标去除的投影In+1→In。

Barton随后观察到：
**引理6.1.1 Barton**
沿着i的限制定义了三角化函子?i?:cSet→sSet。证明
三角化函子是唯一的共连续函子，它将保持乘积的函子扩展到将中的区间映射到sSet中的区间映射：限制函子?i?:cSet→sSet是共连续的并且保持乘积的，Yoneda嵌入也是如此，因此只需证明?i?(I1)=Δ1，对于区间映射也是如此。由于?i[1]?{⊥,1,?}，?i?(I1)就是那个函子。现在结论成立，因为包含映射在带有[1]作为码域的映射上是完全忠实的，因为在任何以{⊥,1,?}为定义域的双点集之间的映射都是保持顺序的。

作为右伴随函子，?i?(I0)=Δ0，并且通过检查，?i?将中的映射0,1:I0→I1和!:I1→I0映射到涉及Δ1的相应映射。因此?i?与三角化函子一致，正如所声称的。

□
我们现在验证伴随三元组中的两个左伴随函子都是Left Quillen函子。为了分析左Kan扩展i!，建立i及其增强类似物之间的关系将是有用的。设和表示通过自由添加初始对象得到的增强单纯形和增强立方体范畴，并用表示由i诱导的保持它们的函子。写作和。

**引理6.1.2**
下面左边的交换方形是精确的，定义了下面右边函子方形中的一个规范自然同构：
证明
这里上面右边方形中的同构是与上面左边方形中的恒等自然变换相关联的Beck–Chevalley变换，因此当方形是精确的时候是可逆的[49]。这个方形的精确性来自于一个一般观察：对于任何函子k:C→D，任何形式的交换方形都是精确的：这反过来可以通过将精确的方形粘贴到任何一组共同满射到中的函子上来检测[67, 2.8，其中W=W0]，例如由左右包含和形成的对。为此，我们注意到其中左手方形和复合矩形都是逗号方形，因此是精确的。同样，下面粘贴方程中的左手和右手方形是精确的，因为函子ι是完全忠实的，而平凡的方形是平凡精确的。

□
使用这个，我们现在证明：
**引理6.1.3**
这些函子保持单态射。证明
对于右伴随函子?i?来说这是直接的。对于左伴随函子i!，我们观察到????i!?i!ι?ι??ι?(i+)!ι?，根据引理6.1.2和的完全忠实性。因此，要证明i!保持单态射，只需证明(i+)!也保持单态射。

在sSet+中的单态射可以规范地分解为形式为?Δn?Δn的映射的余积的序列余极限。作为左伴随函子，(i+)!保持单元复合体，因此只需证明这个函子将这些生成映射保持为单态射。每个边界包含是映射δ:Δm?Δn的族的共同图像，这些映射由集合中的单态射δ:[m]?[n]索引，且其码域为[n]。因此，只需证明(i+)!保持表示之间单态射的共同图像。在Grothendieck topos中，单态射(mi:Ai?B)i∈I的共同图像是由在B上的切片中的以下平行对映射的余等化给出的，因此一个在Grothendieck topos之间的共连续函子将保持单态射族的共同图像，如果它保持族中余 Span的拉回。在函子(i+)!和单态射族(δi:Δmi?Δn)i的情况下，我们将通过展示具有面映射的拉回并且保持它们来证明这一点。

函子是函子i+:FinInt→Fin⊥,?的相反函子，后者是从有限区间范畴{⊥>1>?>n>?}（现在可能允许⊙=⊙）到有限双点集范畴的函子，现在不再要求基点是不同的。我们必须证明FinInt具有，并且i+:FinInt→Fin⊥,?保持满射的余积，或者等价于对于任何有限区间A，逗号范畴A↓FinInt具有，并且遗忘函子i+:A↓FinInt→i+A↓Fin⊥,?保持满射的二元余积。由于满射–单态射正交分解系统，只需限制到满射的子范畴FinIntepi和Fin⊥,?epi，并证明在A↓FinIntepi中存在二元余积，并且被遗忘函子i+:A↓FinIntepi→i+A↓Fin⊥,?epi保持。对于有限区间A，范畴A↓FinIntepi是其在A的底层集合上的等价关系的poset，其等价类是A的子区间（其中子区间的包含不必保持端点）。范畴i+A↓Fin⊥,?epi是其对象是在A的底层集合上的等价关系的poset。使用这些描述，我们看到函子i+:A↓FinIntepi→i+A↓Fin⊥,?epi是一个核心反射嵌入，其右伴随将A的底层集合上的等价关系映射到如果且仅如果由这些元素张成的闭子区间属于单个等价类时的等价关系。特别是，这个遗忘函子创建了在i+A↓Fin⊥,?epi中存在的余积，这证明了我们需要证明的内容。

**注释6.1.4**
[82, 3.5]中密切相关的准则不足以证明i!或(i+)!保持单态射，因为在中由保持初始和终端元素指定的映射的拉回不被映射到笛卡尔立方体范畴中的包含保持。然而，请注意，在原始余跨度中的映射中只有一个单态射。刚刚给出的证明证明了在中的一对单态射的拉回是存在的，并且被i+保持。

**引理6.1.5**
函子i!:sSet→cSet定义了一个从经典模型结构到等变模型结构的Left Quillen函子。证明
如同[82, 3.6]中所述，只需证明i!将广义角包含——即从余维数为一的面集合的并集到单纯形的包含——映射到平凡的余纤维化。这样的广义角包含要么具有面映射δ:Δn?1→Δn的形式，要么是具有少一个面和一个更小维度的广义角包含的余积。因此，根据2-of-3性质和对广义角包含的维数和面数的归纳，只需证明对于每个n都有i!Δn?In是弱可缩的，这是成立的，因为根据推论5.2.7，立方体在等变模型结构中是弱可缩的。

□
我们通过首先证明一个独立感兴趣的结果来证明另一个左伴随函子?i?:sSet→cSet是Left Quillen的：即单纯形集的Kan纤维化也是等变纤维化，我们定义如下。

**定义6.1.6**
设E是一个带有保持乘积的函子的局部笛卡尔封闭范畴，该函子从笛卡尔立方体范畴限制到定义了一个对称序列，为所有k≥1指定了E中的k-立方体Ik以及每个σ∈Σk的自同构。那么等变纤维化是一个映射f:Y→X，其在常量图函子下的像是无偏的均匀纤维化，即具有如下左边的定义中的均匀提升属性的映射：

当E是一个预层范畴时，只需考虑针对具有可表示码域的单态射的均匀提升。

**命题6.1.7**
单纯形集的Kan纤维化是等变纤维化。
证明
由于单纯形集上的经典模型结构是笛卡尔封闭的，任何Kan纤维化f:Y?X都承认作为偏向均匀纤维化的结构，如定义3.6.7i中所述，相对于区间Δ1；参见[46, §9]。实际上，当f:Y?X是一个Kan纤维化时，它也承认作为无偏均匀纤维化的结构[39, 4.22–23]。

拆解这一点意味着Kan纤维化f:Y?X可以配备一个均匀提升函数ic,ζ，如下所示：

我们的任务是将均匀纤维化(f:Y?X,ic,e)配备为等变纤维化的结构。为此，我们使用一个映射?γ∧:Ik×I→Ikγ∧(x1,…,xk,e)?(x1∧e,…,xk∧e)，它沿着{0}?I限制到0→∈Ik的常量映射，并沿着{1}?I限制到恒等映射。这个“最小连接”存在是因为我们正在处理的是单纯形集合中的三角化立方体，而不是笛卡尔立方体。

对于任何ζ:A→Ik，复合映射定义了一个从常量映射0→:A→Ik到ζ的同伦。我们的任务是为均匀纤维化(f:Y?X,ic,e)配备等变纤维化的结构。为此，我们使用一个映射?γ∧:Ik×I→Ikγ∧(x1,…,xk,e)?(x1∧e,…,xk∧e)，它沿着{0}?I限制到0→∈Ik的常量映射，并沿着{1}?I限制到恒等映射。这种“最小连接”存在是因为我们正在处理的是单纯形集合中的三角化立方体，而不是笛卡尔立方体。

**引理6.1.6**
下面的交换方形是精确的，定义了下面右边函子方形中的一个规范自然同构：
证明
这里上面右边方形中的同构是与上面左边方形中的恒等自然变换相关联的Beck–Chevalley变换，因此当方形是精确的时候是可逆的[49]。这个方形的精确性来自于一个一般观察：对于任何函子k:C→D，任何形式的交换方形都是精确的：这反过来可以通过将精确的方形粘贴到到中的任何一组共同满射的函子上来检测[67, 2.8，其中W=W0]，例如由左右包含和组成的对。为此，我们观察到其中左手方形和复合矩形都是逗号方形，因此是精确的。同样，下面粘贴方程中的左手和右手方形也是精确的，因为函子ι是完全忠实的，而平凡的方形是平凡精确的。

**引理6.1.7**
这些函子保持单态射。证明
对于右伴随函子?i?来说这是直接的。对于左伴随函子i!，我们观察到????i!?i!ι?ι??ι?(i+)!ι?，根据引理6.1.2和的完全忠实性。因此，要证明i!保持单态射，只需证明(i+)!也保持单态射。

在sSet+中的单态射可以规范地分解为形式为?Δn?Δn的映射的余积的序列余极限。作为左伴随函子，(i+)!保持单元复合体，因此只需证明这个函子将这些生成映射保持为单态射。每个边界包含是映射δ:Δm?Δn的族的共同图像，这些映射由集合中的单态射δ:[m]?[n]索引，且其码域为[n]。因此，只需证明(i+)!保持表示之间单态射的共同图像。在Grothendieck topos中，单态射(mi:Ai?B)i∈I的共同图像是由在B上的切片中的以下平行对映射的余等化给出的，因此一个在Grothendieck topos之间的共连续函子将保持单态射族的共同图像，如果它保持族中余 Span的拉回。在函子(i+)!和单态射族(δi:Δmi?Δn)i的情况下，我们将通过展示具有面映射的拉回并且保持它们来证明这一点。

函子是函子i+:FinInt→Fin⊥,?的相反函子，后者是从有限区间范畴{⊥>1>?>n>?}（现在可能允许⊙=⊙）到有限双点集范畴的函子，现在不再要求基点是不同的。我们必须证明FinInt具有，并且i+:FinInt→Fin⊥,?保持满射的余积，或者等价于对于任何有限区间A，逗号范畴A↓FinInt具有，并且遗忘函子i+:A↓FinInt→i+A↓Fin⊥,?保持满射的二元余积。由于满射–单态射正交分解系统，只需限制到满射的子范畴FinIntepi和Fin⊥,?epi，并证明在A↓FinIntepi中存在二元余积，并且被遗忘函子i+:A↓FinIntepi→i+A↓Fin⊥,?epi保持。对于有限区间A，范畴A↓FinIntepi是其对象是在A的底层集合上的等价关系的poset，其等价类是A的子区间（其中子区间的包含不必保持端点）。范畴i+A↓Fin⊥,?epi是其对象是在A的底层集合上的等价关系的poset。使用这些描述，我们看到函子i+:A↓FinIntepi→i+A↓Fin⊥,?epi是一个核心反射嵌入，其右伴随将A的底层集合上的等价关系映射到如果且仅如果由这些元素张成的闭子区间属于单个等价类时的等价关系。特别是，这个遗忘函子创建了在i+A↓Fin⊥,?epi中存在的余积，这证明了我们需要证明的内容。

**注释6.1.4**
[82, 3.5]中密切相关的分界标准不足以证明i!或(i+)!保持单态射，因为在中的映射的拉回并没有被映射到笛卡尔立方体范畴中的包含保持。然而，请注意，在原始余跨度中只有一个映射是单态射。刚刚给出的证明证明了在中的一对单态射的拉回是存在的，并且被i+保持。

**引理6.1.5**
函子i!:sSet→cSet定义了一个从经典模型结构到等变模型结构的Left Quill请注意，由于立方体的交换性质，我们可以按照任一顺序执行计算jc,ζ(y,z,x)?(α×σ?1)所需的这两个限制。因此：jc,ζ(y,z,x)?(α×σ?1)=i〈c×Ik,[ζ]〉,0(ic,1(y,zγ∧→ζc,xγ∧→ζ)!,xγ∧)?(A×Ik×?1)?(α×σ?1)=i〈c×Ik,[ζ]〉,0(ic,1(y,zγ∧→ζc,xγ∧→ζ)!,xγ∧)?(α×σ?1×I)?(B×Ik×?1)。另外，请注意，这个立方体的前面是一个拉回（pullback），因为它是由后面与?1:{1}?I的拉回（pushout）的乘积产生的。由于(f,i)在这个拉回方形中的均匀性：=i〈d×Ik,[σζα]〉,0(ic,1(y,zγ∧→ζc,xγ∧→ζ)(α×I)!,xγ∧(α×σ?1))?(B×Ik×?1)，根据上述的均匀性计算，这些提升问题的定义域是一致的。因此：=i〈d×Ik,[σζα]〉,0(id,1(yα,z(α×σ?1)γ∧→σζαd,x(α×σ?1)γ∧→σζα)!,x(α×σ?1)γ∧)?(B×Ik×?1)=jd,σζα(yα,z(α×σ?1),x(α×σ?1))，这就是所需的等变均匀性条件。□引理6.1.8函子?i?:cSet→sSet定义了一个从等变模型结构到经典模型结构的左Quillen函子。为了证明三角剖分（triangulation）是左Quillen的，只需证明右伴随函子?i?将Kan纤维化（Kan fibrations）映射到立方集的等变纤维化（equivalent fibrations），而这又只需证明Kan纤维化在函子?i?下能够提升到生成范畴（generating category）的像。通过上述的均匀性计算，这些提升问题的定义域是一致的。□为了证明引理6.1.5和6.1.8中的左Quillen函子定义了Quillen等价（Quillen equivalences），我们借鉴了Eilenberg–Zilber范畴的一般理论，现在我们对其进行回顾。6.2. Eilenberg–Zilber范畴这两个范畴都是Reedy范畴——前者是按照Dan Kan的原始“严格”定义，后者是按照[24]中的“广义”定义——并且它们也是Eilenberg–Zilber范畴，具体定义如下。这些属性使得我们可以对sSet和cSet这两个预层范畴（presheaf categories）中的单射（monomorphisms）进行归纳论证。一个Reedy范畴A配备了“度数递减”和“度数递增”的映射类，这些映射类是相对于一个度数函数deg:obA→N来定义的。在下面定义的Eilenberg–Zilber范畴中，度数递减的映射是分裂的满射（split epimorphisms），而度数递增的映射是单射（monomorphisms）。定义6.2.1 [24, 6.7]一个Eilenberg–Zilber范畴是一个小范畴A，它配备了一个度数函数deg:obA→N，使得：(i)同构（isomorphisms）保持度数不变，而非可逆的单射或分裂的满射在从定义域移动到值域时分别严格提高和降低度数；(ii)每个f∈morA都可以分解为一个分裂的满射后跟一个单射；(iii)任何具有相同定义域的分裂满射对都有一个绝对的拉回（absolute pushout）：在A中保持不变的Yoneda嵌入。Berger和Moerdijk指出[24, 6.8]，笛卡尔立方体范畴（cartesian cube category）也是一个Eilenberg–Zilber范畴[28, Theorem 8.12(1)]。我们回顾了一些来自一般Reedy范畴理论[79], [75]的结果，然后解释Eilenberg–Zilber范畴的特殊之处。设A是一个Eilenberg–Zilber范畴，并用A∈SetAop×A表示A中箭头的同态双函子（hom bifunctor）。让kknA?A∈SetAop×A表示度数最多为n的箭头的子函子，我们指的是通过度数为n的对象分解的箭头。定义6.2.2 可表示函子的边界（Boundaries of representable functors）对于a∈A，用Aa∈SetA和Aa∈SetAop表示协变和逆变的可表示函子（co- and contravariant representable functors）。如果a∈A的度数为n，用???←Aa?skn?1Aa∈SetA和?→Aa?skn?1Aa∈SetAop表示。外部（逐点）积（external (pointwise) product）定义了一个双函子SetA×SetAop→?×_?SetAop×A。对于任何a∈A，外部莱布尼茨积（external Leibniz product）(6.2.2)定义了一对形如h?g的态射的子函子，其中dom(h)=cod(g)=a，并且g和h中至少有一个的度数小于a的度数。存在一个自然的“复合”映射，其定义域是逆变和协变可表示函子的外部积(6.2.2)Aa×_Aa→°A。它的像是A中通过a分解的箭头的子函子，但(6.2.4)通常不是单射：例如，当a有非恒等自同构时就是这种情况。根据定义6.2.1(i)，Reedy范畴的群体核心G?A可以分解为余积G=?n∈NG(n)，其中G(n)是度数为n的对象之间的同构的子群体。A中的任何同构都以显而易见的方式限制在相应可表示函子边界的自然同构上，这些边界因此组装成函子?←An?An∈SetG(n)op×A和?→An?An∈SetAop×G(n)。当我们在G(n)上复合这些函子时，我们得到了一个从A到A的函子，它是附加到形式sknA的“广义单元”[75, §4]。定理6.2.3包含??A有一个作为广义单元复合体的标准表示：即，作为外部莱布尼茨积的余积的复合体?(?←An?An)×_?G(n)(?→An?An)?∫a∈G(n)(?←Aa?Aa)×_?(?→Aa?Aa)，在第n阶段附加。□作为定理6.2.5的一个推论，任何在cocomplete范畴E中取值的自然变换f:X→Y∈EAop都有一个作为广义单元复合体的标准表示，这是通过对加权余极限函子??A:SetAop×A×EAop→EAop应用莱布尼茨构造得到的。推论6.2.4设A是一个Reedy范畴，设E是bicomplete的。任何态射f:X→Y∈EAop都是一个广义单元复合体X→X∪sk0Xsk0Y→?→X∪skn?1Xskn?1Y→X∪sknXsknY→?→colim?Y，在第n阶段附加了广义单元(6.2.4)?(?→An?An)??G(n)??nf。□这里??nf∈EG(n)op是由f和?←An?An的莱布尼茨加权余极限形成的图表。它在度数为n的a处的分量是相对锁定映射（relative latching map），由映射??Laf??←Aa?Af的余极限定义。我们现在专门讨论E=Set的情况，并对A施加Eilenberg–Zilber假设。设X是一个在Eilenberg–Zilber范畴A上的预层。如果存在一个非可逆的分裂满射π:a?b和一个y∈Xb使得x=yπ，则称元素x为退化的；否则是非退化的。对于退化的x，我们将x=yπ的分解称为x的Eilenberg–Zilber分解。正如[24, 6.9–10]中所观察到的，定义6.2.1的公理意味着Eilenberg–Zilber分解本质上是唯一的，这意味着锁定映射LaX?Xa是单射，其像是退化的元素。此外，以下这个结果的相对 versions 是成立的：引理6.2.5设A是一个Eilenberg–Zilber范畴。那么对于所有f:X→Y∈SetAop，每个相对锁定映射??af是单射当且仅当每个分量fa:Xa?Ya是单射，并且每个假设都意味着对于每个a∈A，下面的锁定方形是一个拉回：证明当f:X→Y是单射时，锁定方形中的每个映射都是单射，很容易看出锁定方形是一个拉回。只需证明LaX映射到拉回Xa×YaLaY上。如果x∈Xa的像是退化的，其中f(x)=y′??，那么我们可以选择一个?的截面δ，并观察到x和x?δ??在f下的像是相同的，从而证明x是退化的。因此锁定方形是一个拉回，那么相对锁定映射是一个单射，是Ya的子对象的并集。对于没有Eilenberg–Zilber假设的一般Reedy范畴，逆向蕴含也是成立的[75, §8]。□引理6.2.8可以概括为：当A是一个Eilenberg–Zilber范畴时，下面定义的注入Reedy单射（injective Reedy monomorphisms）就是逐点的单射。定义6.2.6 在SetAop中的映射f:X→Y是一个注入Reedy单射，如果对于所有a∈A，映射??af是单射。注入Reedy单射形成了一个弱分解系统的左类，这个系统沿着下面的左伴随??•?从（单射，等变分裂满射）弱分解系统在SetGop上左提升，而后者又是（单射，分裂满射）弱分解系统在SetobA上的“注入”或左提升：当A是一个Eilenberg–Zilber范畴时，推论6.2.6告诉我们任何单射f都可以分解为形式为(6.2.7)的映射的无限复合体，其中??nf∈SetG(n)op是单射。度数为n的对象之间的同构的群体G(n)等价于与Aut(a)的自同构群相关的1-对象群体（1-object groupoids）的不交并集。因此，SetG(n)op等价于形式为SetAut(a)op的范畴的乘积，其中deg(a)=n。因此，我们研究了在右G-集合（right G-sets）的范畴SetGop上的（注入单射，注入分裂满射）弱分解系统，对于G是一个群。在这个范畴中，注入单射就是单射，而注入分裂满射是G-分裂满射：允许G-等变截面的右G-集合的映射。引理6.2.7在SetGop中的单射是映射{??G/H}H?G的余积的拉回，其中右G-集合是所有子群H的右陪集G/H的集合。证明在右G-集合的范畴SetGop中的对象可以分解为轨道的余积，G在这些轨道上可传递地作用。每个轨道都G-等变地同构于G/H，即右G-集合的右陪集H。这些轨道中的元素的稳定子群与H共轭。由于G-等变性，这个范畴中的单射附加了新的轨道。因此，每个单射可以表示为形式为??G/H的映射的拉回，对于每个稳定子群H不在定义域的像中的轨道。□综上所述，我们得到以下结果：命题6.2.8任何在由Eilenberg–Zilber范畴A索引的预层之间定义的单射f:X→Y∈SetAop都是广义单元复合体X→X∪sk0Xsk0Y→?→X∪skn?1Xskn?1Y→X∪sknXsknY→?→colim?Y，在第n阶段附加了形式为(6.2.8)?→A/Ha?A/Ha的单元。证明根据引理6.2.10，相对锁定映射??nf∈SetG(n)op是形式为??G(n)/Ha的映射的余积的拉回，其中a∈G(n)，H?Aut(a)，并且G(n)a是逆变可表示的。由于加权余极限函子的cocontinuity和coYoneda引理，(6.2.7)中的单元?(?→An?An)??G(n)??nf是形式为?(?→An?An)??G(n)(??G(n)/Ha)??→A/Ha的单元的余积的拉回。因此，根据推论6.2.6，X∪skn?1Xskn?1Y?X∪sknXsknY是一个这种形式的单元的余积的拉回。□引理6.2.9设A是一个Eilenberg–Zilber范畴。那么在SetAop中的单射是由在某个a∈A的表示层（representable prelayer）的 quotient 上的任意子群H的值映射?→A/Ha生成的。证明根据命题6.2.11，单射是在余积、拉回和顺序复合下由映射?→A/Ha→A/Ha生成的。在单射之间的右取消下，这些映射是由形式为??A/Ha和???→A/Ha的单射生成的。我们通过归纳在a∈A的度数下证明后者类是由前者在余积、拉回和顺序复合以及单射之间的右取消下生成的。当a的度数为零时，?→Aa是空的，覆盖了归纳的基情况。所以我们可以假设a的度数为n，我们的任务是证明???→A/Ha可以在余积、拉回、无限复合和单射之间的右取消下由形式为??A/Hb的映射生成，其中deg(b)≤n。根据归纳假设，当deg(b)我们结合了组合下的闭合性来展示这一点，因为这些是最微妙的闭合性质。考虑一对可组合的单态射及其莱布尼茨应用：图表显示α°ˇhg可以看作是α°ˇg后跟α°ˇh的推出。当g∈N且h是一个余纤维化时，我们的假设意味着α°ˇg的推出是在余纤维化对象之间一个弱等价的推出，因此也是一个弱等价。因此，根据弱等价的2-3性质，h∈N当且仅当hg∈N。□

推论6.2.12 设A是一个Eilenberg–Zilber范畴，并考虑一对在模型范畴M中取值的函子U,V：SetAop→M，以及一个自然变换α：U?V。假设U和V保留余极限，并将K中的单态射映射到M中的余纤维化。那么如果α在由其自同构群的子群所表示的商对象上的分量是弱等价的，那么α的所有分量都是弱等价的。证明 注意α在预层X上的分量是通过在单态射?→X上应用α得到的莱布尼茨应用得到的。现在通过结合引理6.2.13（它表明SetAop中的单态射可以通过并集、推出、超穷组合和右消除由映射?→A/Ha生成）和引理6.2.15（它表明莱布尼茨应用是弱等价的单态射类具有这些闭合性质）就可以得出结果。□

推论6.2.13 设A是一个Eilenberg–Zilber范畴，其中SetAop承认一个模型结构，其余纤维化是那些其自同构群的子群的商A/Ha是弱可缩的单态射。那么如果U,V：SetAop→M定义了一对保留终止对象的左Quillen函子，那么任何自然变换α：U?V都是一个自然的弱等价。证明 根据Ken Brown的引理，保留终止对象的左Quillen函子保留弱可缩的余纤维化对象。现在从与弱可缩余纤维化对象X相关的自然性正方形和2-3性质，我们看到αX的分量是一个弱等价。根据推论6.2.16，如果α在表示对象的商上的分量是弱等价的，那么α是一个自然的弱等价。因此结果随之成立。□ 注意作为一个右伴随，?i?保留终止对象，i!也是如此，因为在其定义域和值域中它都是可表示的，并且?i[0]?[0,1]0。

命题6.2.14 这些函子是左Quillen等价。证明 这些伴随的单位和余单位各自定义了在保留终止对象的左Quillen伴随之间的自然变换。由于这些函子的定义域和值域是配备了模型结构的Eilenberg–Zilber范畴的预层范畴，其中所有对象都是余纤维化的，并且表示对象的商是可缩的，因此推论6.2.17适用于证明单位和余单位都是自然的弱等价。□

6.3. 等变模型结构是测试模型结构 最后，我们展示了等变模型结构与测试模型结构是一致的。笛卡尔立方体范畴是一个严格的测试范畴[25]，因此笛卡尔立方体集承认一个模型结构，这个结构被Grothendieck[45]猜测存在，并由Cisinski[33]在这样的一般性水平上确立，它呈现了经典的同伦理论。在Cisinski关于测试范畴上预层的模型结构中——下面称为测试模型结构——余纤维化是单态射，弱等价是那些预层映射f:X→Y，它们通过应用函子Nel（该函子取元素的神经）定义的单纯集映射是一个弱同伦等价。定义6.3.1 如果一个范畴的神经在Quillen模型结构中是弱可缩的，那么这个范畴就是非球面的。如果一个函子u:A→B在小范畴之间是等价的，那么对于B中的每个b，逗号范畴u↓b也是非球面的。如果一个预层在小范畴上是非球面的，那么它的元素范畴是非球面的。注意，根据定义，一个在测试范畴上的预层是非球面的当且仅当它在测试模型结构中是弱可缩的。

评论6.3.2 [39, 7.14] sSet上的测试模型结构是Kan–Quillen模型结构。特别地，一个单纯集是非球面的当且仅当它在Kan–Quillen模型结构中是弱可缩的。现在我们可以使用非球面函子的机制来关联cSet上的测试模型结构与Kan–Quillen模型结构。

命题6.3.3 [33, 4.2.24] 设u:A→B是测试范畴之间的一个非球面函子。那么这个伴随在测试模型结构之间定义了一个Quillen等价。

命题6.3.4 [33, 4.2.23] 一个函子u:A→B在小范畴之间是非球面的当且仅当对于B中的每个b，相应的都是非球面的。证明 的元素范畴等同于逗号范畴u↓b。□

推论6.3.5 函子 是非球面的。证明 根据命题6.3.4，我们想要证明对于每个n∈N，?i?In∈sSet是一个非球面预层。根据评论6.3.2，这意味着需要证明?i?In在Kan–Quillen模型结构中是可缩的。我们有?i?In?(Δ1)n根据引理6.1.1，所以情况确实如此。□

定理6.3.6 cSet上的等变模型结构与测试模型结构是一致的。证明 这两种模型结构有相同的余纤维化，因此只需证明它们有相同的弱等价。回想一下，一个左Quillen等价保留并反映余纤维化对象之间的弱等价。因此，根据命题6.2.18，如果一个映射f在等变模型结构中是一个弱等价，那么?i?f也是一个弱等价。但是根据命题6.3.3和推论6.3.5，f在测试模型结构中也是一个弱等价当且仅当?i?f是一个弱等价。因此，等变模型结构和测试模型结构的弱等价是一致的。□