---
title: "累积层级是 ZF 与 ZFC 的模型"
module: V.Model
lang: zh
site: "Bedrock"
description: "累积层级是 ZF 与 ZFC 的模型"
stage: "环境层级"
reading_order: 22
canonical: https://bedrock.institute/zh/V.Model.html
html: V.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Model.lagda.md
prerequisites: [Base.Prelude, Base.Impredicativity, Base.Classical, Base.Choice, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.ZFModel, V.Hierarchy, V.Smallness]
routes: [ambient-model]
translations: [https://bedrock.institute/en/V.Model.md, https://bedrock.institute/ja/V.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 累积层级是 ZF 与 ZFC 的模型

本章在固定的一个宇宙层级 `ℓ` 上，于累积层级内部逐条实现 ZF 的公理。对于要求集合存在的公理，任务是构造这样的集合，并证明其成员关系作为真值的路径恰是该公理所要求的描述。所涉假设值得先分开陈述。层级中已有的构造，即空集、配对与并，只花层级自身集合构造子的代价；替换同样如此，它直接从该构造子的成员规则读出。全分离需要命题降级，使每个满足命题获得低一层宇宙的代表。幂集需要一个命题的小分类器，即 `HPropSmallness`。降层与分类器打包为 `Impredicativity`，装配出的 ZF 定理 `V⊨ZF` 恰假设 `LEM (ℓ-suc ℓ)`，打包由它导出。ZFC 部分另以 `ℓ-suc ℓ` 层的集合层选择为假设；由 Diaconescu 定理，它蕴含 ZF 部分所用的排中律，而降低一层宇宙后又供给选择集公理。本章的工作就是把层级已有的构造逐一转换成公理所要求的精确形状，直至得出这两个定理。

宇宙层级的账目是精确的，值得读一遍。模型的载体是层级 `ℓ` 上的 `S`，它本身居于 `Type (ℓ-suc ℓ)`。充当模型等词与成员关系的真值住在 `hProp (ℓ-suc ℓ)`。打包 `Impredicativity ℓ` 联结下文用到的两个小性原理：该真值层上的 `resizing`，以及小分类器 `HPropSmallness ℓ`，即与整个 `hProp ℓ` 等价的一个小类型。选择引理消耗层级 `ℓ` 上的集合层选择，而最终两条推论分别假设 `LEM (ℓ-suc ℓ)` 与 `SetChoice (ℓ-suc ℓ)`。因此没有哪一层统一层级支配所有假设；每条原理都恰在其陈述有意义之处取用。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

module V.Model {ℓ : Level} where

open import Base.Impredicativity using ( HPropSmallness; Impredicativity )
```

「层级满足一条公理」在形式上是什么意思？一阶逻辑诸章供给了术语。一个结构是作为 h-集合的载体，其等词与成员关系取真值，而非某个固定二元类型中的布尔值。公式是对象语言语法的元素，公理模式对它的自由变元槽量化。满足关系在载体元素的环境下读出公式，返回一个真值。下面将逐一按这些术语重新导出 ZF 的公理。

```agda
open import Base.Classical using ( LEM; lem→impredicativity )
open import Base.Choice using ( SetChoice; choice→lem; lowerSetChoice )
open import FOL.ZFStructure using ( ZFStructure )
open import FOL.Syntax using ( Formula )
import FOL.Semantics
```

层级给出结构 `𝒮ᵥ`：其等词是高阶归纳类型 `V ℓ` 的路径类型，其成员关系是层级原生的 `∈`。该结构的外延性与正则性已在层级一章证明，此处引用而非重证。另有一个从小性一章带来的工具：从「每个取值都小」的谓词构造集合的适配器；一旦降层供给小性，它就成为全分离。全文中，命题之间的双向蕴含经标准改写 `⇔toPath` 变成真值之间的路径；下文几乎每条规格都以这一步收尾。

```agda
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import V.Smallness {ℓ} using ( separateFromSmall )

open import Cubical.Foundations.Equiv using ( equivFun; invEq; secEq )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

三条 cubical 一般事实塑造了后面的证明。到相等类型为命题的类型的嵌入是单射，当需要说明回收到的索引是唯一可能时这一点就要用上。第二分量为命题的依值对之间的路径由第一投影之间的路径决定。此外，像集的成员陈述通常是截断的存在式：用 `∣_∣₁` 引入，用 `PT.rec` 消入取命题值的目标；矛盾则交给空类型处理。

```agda
open import Cubical.Functions.Embedding
  using ( Embedding-into-isSet→isSet; isEmbedding→Inj )
open import Cubical.Data.Sigma using ( Σ≡Prop )
import Cubical.Data.Sum as Sum
import Cubical.Data.Empty as Empty
```

核心构造是集合构造子 `sett`：从小索引类型 `X` 与族 `X → S` 造出像集，而 `y ∈ sett X ix` 恰在纯粹地存在某个索引呈现 `y` 时成立。替换直接从这条成员规则读出。层级是 h-集合这一点 (由 `setIsSet` 记录) 使路径类型 `x ≡ y` 成为命题，从而成为结构等词的合法真值。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base
  using ( sett; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

成员关系有两种形态，全章都在二者之间移动。每个集合 `a` 都有小索引类型 `⟪ a ⟫`，配一个像恰为 `a` 的嵌入 `⟪ a ⟫↪`；小隶属 `x ∈ₛ a` 说某个索引呈现 `x`。等价 `∈∈ₛ` 在两个方向上逐点互换小隶属与普通隶属；`∈-asFiber` 则更进一步：从 `x ∈ a` 的证明返回实际的不加截断的对 (一个索引加一条呈现路径)。正是这种不加截断性使索引回收成为函数而非选择。所需的基本集合也已备好：带反驳 `∅-empty` 的空集、配对 `⁅ a , b ⁆` 与 `pairing-ax`、并 `⋃ a` 与 `union-ax`、带分类的单点集 `⁅ a ⁆s`，以及二元并 `_∪_`。

```agda
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber
        ; identityPrinciple; _⊆_; extensionality )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; ⁅_⁆s; _∪_
        ; SingletonPackage; module InfinitySet )
```

一个具体的转换展示了所有规格证明都用的方法。对配对，库的 `pairing-ax` 陈述 `x ∈ₛ ⁅ a , b ⁆` 与析取 `x ≡ₕ a ⊔ x ≡ₕ b` 之间的双向蕴含；对当前结构，`≡ₕ u v` 就是路径类型 `u ≡ v`，与结构的 `≈ˢ u v` 按定义相同。于是下一节证明的配对规格只是把 `⇔toPath` 应用于 `pairing-ax`，并在每个方向穿过一层 `∈∈ₛ`：正向把普通隶属转成分类所消耗的小隶属，反向把所得析取转回普通隶属。同样的三步转换空集、并，以及 (多一层截断) 索引族之并的成员关系。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
open InfinitySet using ( sucV; #_; ω )

open ZFStructure 𝒮ᵥ
```

所有这些转换的目标是 record `isZFModel`，其字段即 ZF 公理：外延性、正则性、空集、配对、并、分离、替换、幂集，以及经数码链及其两条固定方程表述的强无穷。每个存在性字段要求 `isContr (SetOf Q)`：实现类 `Q` 的集合加上唯一性数据，唯一性由外延性提供；`isZFCModel` 再加选择集字段。深嵌入公式的满足关系在此结构上实例化：`(y ∷ x ∷ []) ⊨ φ` 表示在把 `y` 赋给第一个自由变元槽、`x` 赋给第二个的环境下读出元数为 2 的公式 `φ`。各公理模式都作为其参数的函数给出，因此对每个公式的每个实例都一次成立。

```agda
module Model = FOL.ZFModel 𝒮ᵥ
open Model using ( SetOf; _⊆ˢ_; setOf-unique; isZFModel; isZFCModel )

module SemanticsV = FOL.Semantics 𝒮ᵥ
open SemanticsV.At S id using ( _⊨_ )
```

## 基本集合

空集、配对与并是最容易兑现的字段，因为这些构造及其分类在层级库中已经存在。剩下的只是改变陈述的形状。模型 record 的规格是真值的相等，而且是一条路径：对载体的每个元素 `x`，真值 `x ∈ˢ b` 必须作为路径等于类描述 `Q x`。库通过小隶属 `∈ₛ` 陈述其公理，于是每次转换都用同样三步：`∈∈ₛ` 逐点互换小隶属与普通隶属，库的分类给出相应的双向蕴含，`⇔toPath` 把该双向蕴含改写成所需的路径。配对最贴近：库的「等于 `a` 或等于 `b`」与字段的 `(x ≈ˢ a) ⊔ (x ≈ˢ b)` 按定义相同，真正的工作只剩一层 `∈∈ₛ`。

空集的规格要求：对载体的每个元素 `x`，真值 `x ∈ˢ ∅` 作为路径恰等于假值 `⊥` 的像。这是本章基本转换的缩影。库所证明的是 `∅` 在小隶属 `∈ₛ` 意义下没有成员，所以先要逐点交换两种隶属。正向，`∈∈ₛ` 把 `x ∈ˢ ∅` 的证明变成被 `∅-empty` 驳斥的小隶属；由这一矛盾，空类型有元素，这正蕴含所需的结论。反向则无需构造任何东西，因为 `⊥` 没有元素可给。`⇔toPath` 最后把所得的命题间双向蕴含转换成规格要求的真值路径。

```agda
empty-spec : (x : S) → (x ∈ˢ ∅) ≡ ⊥
empty-spec x = ⇔toPath
  (λ x∈ → Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈)))
  (λ ())

pair-spec : (a b x : S) → (x ∈ˢ ⁅ a , b ⁆) ≡ ((x ≈ˢ a) ⊔ (x ≈ˢ b))
```

配对要求：`⁅ a , b ⁆` 中的成员关系等于「与 `a` 相等或与 `b` 相等」的析取，其中相等按结构的 `≈ˢ` 读出。库的 `pairing-ax` 给出小隶属 `x ∈ₛ ⁅ a , b ⁆` 与「与 `a` 或 `b` 小相等」的析取之间的双向蕴含，其命题部分已与目标形状一致。正向，`∈∈ₛ` 的一次应用把普通成员资格 `x ∈ˢ ⁅ a , b ⁆` 转成 `pairing-ax` 所消耗的小形式，其第一方向返回该析取。反向，`pairing-ax` 的第二方向给出小隶属，`∈∈ₛ` 的另一半再把它提升回普通成员资格。每个方向都是一次库结果的应用，外面只包一层隶属记号的交换。

```agda
pair-spec a b x = ⇔toPath
  (λ x∈ → pairing-ax a b x .fst (∈∈ₛ {a = x} {b = ⁅ a , b ⁆} .fst x∈))
  (λ h → ∈∈ₛ {a = x} {b = ⁅ a , b ⁆} .snd (pairing-ax a b x .snd h))

union-spec : (a x : S) → (x ∈ˢ (⋃ a)) ≡ (∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y))
union-spec a x = ⇔toPath
```

并是第一个带存在形状的规格：`⋃ a` 中的成员关系应等于「某个 `y` 属于 `a` 且 `x` 属于 `y`」的截断陈述。正向，`union-ax` 给出的正是这样的截断三元组 `(v , v ∈ a , x ∈ v)`，只是两个成员资格都是小形式。改写发生在命题截断内部，而目标仍是命题，所以 `PT.map` 就地改写见证：`∈∈ₛ` 把 `v ∈ₛ a` 变成 `a` 的普通成员，把 `x ∈ₛ v` 变成 `v` 的普通成员。结果是带索引析取 `∃[ x ] P x 的一个见证，即`hProp` 上对载体的纯粹存在陈述，并且不选出任何成员。

```agda
  (λ x∈ → PT.map
    (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .snd va
                           , ∈∈ₛ {a = x} {b = v} .snd xv })
    (union-ax a x .fst (∈∈ₛ {a = x} {b = ⋃ a} .fst x∈)))
  (λ h → ∈∈ₛ {a = x} {b = ⋃ a} .snd (union-ax a x .snd (PT.map
```

反向把同一交换倒过来做。从带索引析取的截断见证出发，`PT.map` 对每个情形 `(v , v ∈ a , x ∈ v)` 用 `∈∈ₛ` 的另一方向重建 `union-ax` 所消耗的小形式三元组；其第二方向给出 `⋃ a` 中的小隶属，再由 `∈∈ₛ` 的另一半提升为普通成员资格。两个方向合起来给出规格所需的真值路径，都来自同一个库分类加上逐点的隶属记号交换。

```agda
    (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .fst va
                           , ∈∈ₛ {a = x} {b = v} .fst xv })
    h)))
```

本章的目标是在累积层级内部实现 ZF 的每条公理，全程固定在同一个宇宙层级 `ℓ` 上：结构 `𝒮ᵥ` 带有取真值的等词与成员关系的载体 `S`，模型 record 对每条公理都要求一个集合，其成员关系按路径等于所规定的描述。各部分所需假设并不均匀，值得分开列出。层级中已有的构造，即空集、配对、并与无穷，以及整个替换论证，完全不需要额外假设。全分离需要命题降级，使每条公式的满足逐点成为小命题。幂集需要小分类器 `HPropSmallness`，一个与整个 `hProp ℓ` 等价的小类型。打包的推论记录合并后的代价：`V⊨ZF` 恰假设 `LEM (ℓ-suc ℓ)`，`V⊨ZFC` 恰假设 `SetChoice (ℓ-suc ℓ)`。本节停留在无需假设的一侧，先为一个集合的并、再为索引族 `f : X → S` 的并展开基本成员规格。集合 `⋃ (sett X f)` 经由一个中间集合收拢族的取值，值得把属于这个并直接读作属于某个族元。展开 `union-spec` 得到对并的成员 `v` 的截断存在式，而每个这样的 `v` 又由 `sett` 的一个索引呈现，于是上面还叠着第二层截断。下面两条引理在两个方向上把各层合而为一。

内向引理把一个具体的成员资格 `x ∈ f i` 变成整个并的成员资格。见证是直接写出而非寻找的：中间元素就是 `f i` 本身，由索引 `i` 经自反路径呈现，`h` 证明 `x` 在其中。由于 `union-spec` 是真值的相等，`subst ⟨_⟩` 沿反向的规格搬运该见证，使这个截断三元组恰以并的特征化所期望的形状被消耗。除 `union-spec` 本身外不进入任何东西。

```agda
union-family-in : (X : Type ℓ) (f : X → S) (i : X) (x : S)
                → ⟨ x ∈ˢ f i ⟩ → ⟨ x ∈ˢ (⋃ (sett X f)) ⟩
union-family-in X f i x h = subst ⟨_⟩ (sym (union-spec (sett X f) x))
  ∣ f i , ∣ i , refl ∣₁ , h ∣₁

union-family-out : (X : Type ℓ) (f : X → S) (x : S)
```

外向引理从「属于并」恢复出：纯粹地存在某个含 `x` 的族元。展开 `union-spec` 得到截断的三元组 `(v , v 在并中 , x 在 v 中)`；第二分量说 `v` 由某个索引呈现，于是在截断内部再作一次 `PT.map`，抽出 `(i , q)` 使 `f i ≡ v`。然后把 `x` 在 `v` 中的成员资格沿 `q` 的反向搬运，落进 `f i`。目标保持截断，因此消去用 `PT.rec` 进入 `∥ Σ[ i ] ⟨ x ∈ˢ f i ⟩ ∥₁`，以 `squash₁` 为命题性证据；结论仍是纯粹存在：某个族元含 `x`，而不选出任何族元。

```agda
                 → ⟨ x ∈ˢ (⋃ (sett X f)) ⟩ → ∥ Σ[ i ∈ X ] ⟨ x ∈ˢ f i ⟩ ∥₁
union-family-out X f x h = PT.rec PT.squash₁
  (λ { (v , hv , hx) → PT.map
    (λ { (i , q) → i , subst (λ w → ⟨ x ∈ˢ w ⟩) (sym q) hx }) hv })
  (subst ⟨_⟩ (union-spec (sett X f) x) h)
```

## 无需新增公理的替换

替换是一条模式公理：在通常集合论中，对每个集合 `a` 与在 `a` 上函数性的公式 `φ`，像的存在性必须被公理化地断言。这里由层级自身给出构造，并且不调用任何选择原理。函数性假设以紧缩性陈述：对 `a` 的每个成员 `x`，满足 `(y ∷ x ∷ []) ⊨ φ` 的 `y` 构成的类型是紧缩的，于是中心值带有「其他任何值都与它等同」的证明。由于紧缩性提供实际数据，这个中心值可以被读出并用于构造像。但 `a` 的成员只通过小呈现给出：每个成员都以 `⟪ a ⟫↪ m` 的形式出现，`m` 是类型 `⟪ a ⟫` 的某个索引。因此构造以 `⟪ a ⟫` 本身为像编索引；可能精细的一步，即从成员资格回收索引，是函数而非选择，因为 `∈-asFiber` 的呈现纤维不加截断。需要核对的是：所得集合的成员关系恰有模式所要求的真值。正向只是读出像自身提供的资料；反向从外部成员资格回收一个索引，然后用一次函数性假设的紧缩，把外部给定的值与构造在回收索引处选定的值等同起来。

一个预备事实贯穿下文：若 `m` 是 `a` 的呈现中的一个索引，则它呈现的元素 `⟪ a ⟫↪ m` 确实是 `a` 的成员。小成员资格 `⟪ a ⟫↪ m ∈ₛ a` 按呈现的定义成立，`∈∈ₛ` 把它提升为结构性成员资格。本节随后取定数据：集合 `a`、有两个自由变元槽的公式 `φ`，以及函数性假设 `fc`，它对每个 `x ∈ a` 断言满足 `(y ∷ x ∷ []) ⊨ φ` 的 `y` 构成的类型是紧缩的。紧缩性是数据，即一个中心加上一个收缩，因此 `a` 的每个成员的中心值可供计算使用，无需任何选择原理。

```agda
private
  memb : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ˢ a ⟩
  memb a m = ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)

module _ (a : S) (φ : Formula S 2)
         (fc : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where
```

像集于是是直接的组装：`replaceImage` 是索引类型 `⟪ a ⟫` 上的 `sett`，把每个索引 `m` 映到 `fc` 为成员 `⟪ a ⟫↪ m` 提供的中心值。其规格说：属于 `replaceImage` 等于对所有 `x` 析取 `(x ∈ a) ⊓ φ(y, x)` 得到的真值。这正是语义形式的替换模式：`y` 属于像，当且仅当它是 `φ` 在 `a` 的某个成员处取的值。与本章其他地方一样，`⇔toPath` 把两个蕴含转换成规格要求的真值路径。

```agda
  replaceImage : S
  replaceImage = sett ⟪ a ⟫ (λ m → fc (⟪ a ⟫↪ m) (memb a m) .fst .fst)

  replaceImage-spec : ∀ y → (y ∈ˢ replaceImage)
                    ≡ (∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))
  replaceImage-spec y = ⇔toPath fwd bwd
```

规格的正向方向从像中的成员资格出发。由于 `replaceImage` 是以 `a` 的呈现类型为索引的 `sett`，这样的成员资格带有 `⟪ a ⟫` 的一个索引 `m`，以及一条从被呈现元素 `⟪ a ⟫↪ m` 到 `y` 的路径 `q`。右侧的见证就由这一个索引组装而成。第一，由预备事实 `memb`，被呈现元素是 `a` 的成员。第二，`fc` 在该成员处给出值以及 `φ` 对该值与该成员成立的证明；沿 `q` 传递该证明，就把公式的第二个自由变元槽从被呈现元素移到 `y`。这一方向不使用 `fc` 的任何唯一性内容：无论像以何种方式呈现 `y`，都得到 `a` 中使 `φ(y, x)` 成立的某个成员。

```agda
    where
    fwd : ⟨ y ∈ˢ replaceImage ⟩ → ⟨ ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ) ⟩
    fwd = PT.map λ { (m , q) →
        ⟪ a ⟫↪ m , memb a m
      , subst (λ v → ⟨ (v ∷ ⟪ a ⟫↪ m ∷ []) ⊨ φ ⟩) q
```

后向方向正是表面上离不开选择原理之处。它收到截断的见证 `(x , x∈a , hφ)`，必须给出像的一个索引，而且该索引要呈现 `a` 中使 `φ(y, x)` 成立的那个成员 `x` 本身。于是必须把「`x` 是成员」这一事实转化为呈现它的索引。小性一章给出的恰是这个：`∈-asFiber` 以普通的不加截断的数据返回实际的对 `mf`，由一个索引加一条从被呈现元素回到 `x` 的路径组成。回收是函数，因此并没有在可能的索引之间作任何选取。随后把满足证明 `hφ` 沿路径 `mf .snd` 的逆传递，把第二个自由变元槽从 `x` 移到被呈现元素，与前提 `fc` 被陈述的形状一致。

```agda
              (fc (⟪ a ⟫↪ m) (memb a m) .fst .snd) }
    bwd : ⟨ ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ) ⟩ → ⟨ y ∈ˢ replaceImage ⟩
    bwd = PT.map λ { (x , x∈a , hφ) →
      let mf = ∈-asFiber {a = x} {b = a} x∈a
          hφ' = subst (λ v → ⟨ (y ∷ v ∷ []) ⊨ φ ⟩) (sym (mf .snd)) hφ
```

回收的索引还须变成像中的成员资格，这正是唯一性唯一进入之处。在索引 `mf .fst` 处，函数性假设说合适值构成的类型是紧缩的，于是把外部给定的对 `(y , hφ')` 与选定中心比较：紧缩给出中心及一条到它的路径，该路径的第一投影把 `y` 与构造赋给被呈现成员的值等同起来，而后者就是 `replaceImage` 的一个索引。因此唯一性恰好用了一次，用来把外部给定的值 `y` 认作内部选出的像值之一。与呈现索引 `mf .fst` 合起来，就得到 `y` 在像中的成员资格。

```agda
      in mf .fst
       , cong fst (fc (⟪ a ⟫↪ (mf .fst)) (memb a (mf .fst)) .snd (y , hφ')) }
```

## 数码链与 ω

强无穷是库几乎完整供给的字段。库的 `ω` 是在 `Lift ℕ` 上、以数码 `#` 为族的 `sett`，所以 `x` 属于 `ω` 恰当它仅仅被某个 `#` 命中。但 record 的要求是通过模型自身的数码链表述的：零必须是空的，每个后继的成员必须恰为前驱的成员再加上前驱本身。因此工作在于对齐两条取后继方式不同的链：模型链取 `a ∪ ⁅ a , a ⁆`，库链取 `sucV a = a ∪ ⁅ a ⁆s`。两个元素相同的对集 `⁅ a , a ⁆` 与单点集 `⁅ a ⁆s` 有相同的元素，外延性把它变成一条路径；有了这一次等同，两条链便逐级一致，`ω` 的成员特征化就成为 record 的强无穷。

等同 `⁅ a , a ⁆ ≡ ⁅ a ⁆s` 是集合之间的路径，所以外延性把它化归为两个成员收纳。第一个收纳说两个元素相同的对集的每个元素都是单点集的元素。其输入是 `⁅ a , a ⁆` 中的成员资格，配对公理把这样的成员资格展开为截断的析取：该元素经由配对的左分支或右分支等于 `a`。

```agda
pair-singleton : (a : S) → ⁅ a , a ⁆ ≡ ⁅ a ⁆s
pair-singleton a = extensionality ⁅ a , a ⁆ ⁅ a ⁆s (s1 , s2)
  where
  singl-cls = SetPackage.classification (SingletonPackage a)
  s1 : ⟨ ⁅ a , a ⁆ ⊆ ⁅ a ⁆s ⟩
```

两个析取支要求的是同一件事：属于 `⁅ a ⁆s`。于是先把截断的析取消入命题 `x ≡ a` (其命题性来自层级是 h-集合)，每个分支给出自己的路径，而两个结果恰由该命题性等同。这里消耗的是单点集分类的反向：从路径 `x ≡ a` 走到小隶属 `x ∈ₛ ⁅ a ⁆s`；注意它与反向包含将要使用的方向恰好相反。

```agda
  s1 x x∈ₛ = singl-cls x .snd
    (PT.rec (setIsSet x a)
            (λ { (Sum.inl e) → e ; (Sum.inr e) → e })
            (pairing-ax a a x .fst x∈ₛ))
  s2 : ⟨ ⁅ a ⁆s ⊆ ⁅ a , a ⁆ ⟩
```

反向包含则朝另一方向进行：分类的正向分量把成员资格 `x ∈ₛ ⁅ a ⁆s` 变成路径 `x ≡ a`，把该路径作为左析取支注入后，配对公理把它转成 `⁅ a , a ⁆` 中的成员资格。两个集合等同之后，模型的数码链按 `ℕ` 递归定义：`numeralV zero` 是空集，`numeralV (suc n)` 在第 `n` 阶段上并上一个两个元素都是该阶段的对集。经等同，由于两个元素相同的对集与单点集成员相同，这正是冯·诺伊曼后继步骤 `n ∪ ⁅ n ⁆s`。

```agda
  s2 x x∈ₛ = pairing-ax a a x .snd ∣ Sum.inl (singl-cls x .fst x∈ₛ) ∣₁

numeralV : ℕ → S
numeralV zero    = ∅
numeralV (suc n) = numeralV n ∪ ⁅ numeralV n , numeralV n ⁆

numeralV≡# : (n : ℕ) → numeralV n ≡ # n
```

两条链的一致按 `ℕ` 归纳证明。在零处两边都化归为空集，路径是 `refl`。后继步在同一个「配对再取并」的形状下用共质性改写两边，并在配对内部应用等同 `pair-singleton`，这正是消耗外延性结果之处。链对齐后，剩下的任务是用模型的语言读 `ω` 的成员关系。陈述 `ω-specV` 说：`ω` 中的成员关系等于带索引的析取「`x` 等于某个 `numeralV`」，索引取遍 `Lift ℕ`，其元素是提升的自然数。右边的相等是 `≈ˢ`，即结构的集合外延相等，因此该陈述是关于集合 `x` 的，而非关于某个被选呈现。

```agda
numeralV≡# zero    = refl
numeralV≡# (suc n) = cong₂ (λ u v → ⋃ ⁅ u , v ⁆) (numeralV≡# n)
  (cong (λ u → ⁅ u , u ⁆) (numeralV≡# n) ∙ pair-singleton (# n))

ω-specV : (x : S)
        → (x ∈ˢ ω) ≡ (∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralV (lower n))
```

证明用 `⇔toPath` 把成员关系的两种描述转成路径。前向：见证 `(i , p)` 是一个提升的索引，加一条从 `x` 到库数码 `# (lower i)` 的路径 `p`；把 `p` 与对齐路径的逆逐段复合，就得到从 `x` 到 `numeralV (lower i)` 的路径。后向：同一套路径代数沿反方向进行，从 `x` 到 `numeralV` 的路径经对齐改写为到相应 `#` 的路径。`lift` 与 `lower` 的转换只是把自然数跨过 `Lift` 移动；两个方向的数学内容都是对齐 `numeralV≡#` 及其周围的路径代数。

```agda
ω-specV x = ⇔toPath
  (PT.map (λ { (i , p) → lift (lower i)
             , sym p ∙ sym (numeralV≡# (lower i)) }))
  (PT.map (λ { (n , q) → lift (lower n)
             , sym (q ∙ numeralV≡# (lower n)) }))
```

record 的两条固定方程描述的是后继阶段的成员关系，因此本章需要对 `sucV` 本身的分情形分析：`sucV A` 的成员，纯粹地，要么是 `A` 的成员、要么等于 `A`，且两个方向的收纳都成立。由于库数码按 `sucV` 取后继，这使得任何与库对齐的数码链都能继承固定方程。该分析把 `sucV A` 沿并与配对公理展开一次；第二个析取支，即属于单点集 `⁅ A ⁆s` 的成员资格，由单点集的分类收尾。

分析从上一节的一条事实出发，值得把它单独抽出：`x` 属于单点集 `⁅ A ⁆s` 强制路径 `x ≡ A`。这是单点集分类的前半，此处记为 `singl≡`。消去原则 `∈sucV-elim` 随后把分情形分析变成可用的形式：给定命题 `P`、由「`x` 属于 `A`」得 `P` 的证明、由「`x` 等于 `A`」得 `P` 的证明，以及 `sucV A` 的一个成员，它就给出 `P` 的证明。要求 `P` 是命题，恰好是把截断的分情形消入它的依据。

```agda
private
  singl≡ : (A x : S) → ⟨ x ∈ₛ ⁅ A ⁆s ⟩ → x ≡ A
  singl≡ A x = SetPackage.classification (SingletonPackage A) x .fst

∈sucV-elim : {A x : S} {P : Type (ℓ-suc ℓ)} → isProp P → ⟨ x ∈ˢ sucV A ⟩
           → (⟨ x ∈ˢ A ⟩ → P) → (x ≡ A → P) → P
```

数学上，`sucV A` 是配对 `⁅ A , ⁅ A ⁆s ⁆` 的并，所以它的成员是该对某个分量的成员。分析因此分两步。并公理先纯粹地给出配对的一个分量 `v`，且 `x` 是 `v` 的成员；配对公理再把「`v` 属于这对」分裂为截断的析取 `v ≡ A` 或 `v ≡ ⁅ A ⁆s`。左支中，沿 `v ≡ A` 传递 `x ∈ v` 即得 `A` 中的普通成员资格，恰是第一个前提所期望的。

```agda
∈sucV-elim {A} {x} pP x∈ kA k≡ =
  PT.rec pP
    (λ { (v , (v∈₂ , x∈v)) → PT.rec pP
      (λ { (Sum.inl v≡A) →
             kA (∈∈ₛ {a = x} {b = A} .snd (subst (λ w → ⟨ x ∈ₛ w ⟩) v≡A x∈v))
```

右支中，沿 `v ≡ ⁅ A ⁆s` 传递得到单点集中的成员资格，`singl≡` 把它变成路径 `x ≡ A`，正是第二个前提所期望的。两次截断消去都落入命题 `P`，因而合法，两个情形合起来完成分析。第一个收纳也单独记录：`∈sucV-inl` 陈述 `A` 的成员是 `sucV A` 的成员。

```agda
         ; (Sum.inr v≡s) →
             k≡ (singl≡ A x (subst (λ w → ⟨ x ∈ₛ w ⟩) v≡s x∈v)) })
      (pairing-ax A ⁅ A ⁆s v .fst v∈₂) })
    (union-ax ⁅ A , ⁅ A ⁆s ⁆ x .fst (∈∈ₛ {a = x} {b = sucV A} .fst x∈))

∈sucV-inl : {A x : S} → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ sucV A ⟩
```

`∈sucV-inl` 的证明是构造而非分析：从假设的「`x` 属于 `A`」出发，组装出属于并的见证。在截断内部，配对的分量 `A` 经配对公理以带自反路径的左析取支呈现；`x` 属于 `A` 的成员资格则转成并公理所消耗的小形式。外层交换再把整个小形式见证提升为 `sucV A` 中的成员资格。

```agda
∈sucV-inl {A} {x} x∈A = ∈∈ₛ {a = x} {b = sucV A} .snd
  (union-ax ⁅ A , ⁅ A ⁆s ⁆ x .snd
    ∣ A , (pairing-ax A ⁅ A ⁆s A .snd ∣ Sum.inl refl ∣₁
         , ∈∈ₛ {a = x} {b = A} .fst x∈A) ∣₁)

self∈sucV : (a : S) → ⟨ a ∈ˢ sucV a ⟩
```

伴随的 `self∈sucV` 证明第二个收纳：每个集合 `a` 属于它自己的后继。这次的见证是配对的另一分量 `⁅ a ⁆s`，经右析取支呈现；它包含 `a` 这一事实是单点集分类的后半应用于自反路径。两条引理合起来给出固定方程所需的内容：`sucV A` 的成员，仅仅是 `A` 的成员再加上 `A` 本身。

```agda
self∈sucV a = ∈∈ₛ {a = a} {b = sucV a} .snd
  (union-ax ⁅ a , ⁅ a ⁆s ⁆ a .snd
    ∣ ⁅ a ⁆s , (pairing-ax a ⁅ a ⁆s ⁅ a ⁆s .snd ∣ Sum.inr refl ∣₁
              , SetPackage.classification (SingletonPackage a) a .snd refl) ∣₁)
```

任意与库对齐的链的两条固定方程。record 要求：第零个数码没有成员；每个后继数码的成员恰为其前驱的成员加上前驱本身。这两条陈述都关乎给定链中的成员资格，而上一节的分情形分析谈的是 `sucV` 中的成员资格；对齐 `q : a n ≡ # n` 是桥梁，关于链中成员资格的陈述都可沿 `q` 搬运为关于库数码的相应陈述。该模块把链与对齐作为参数，因此同样的引理既服务模型的链，也服务任何其他链。

第零条方程较简单。若 `z` 是链的第零处的成员，沿 `q zero` 搬运便使它成为库空集的成员；经 `∈∈ₛ` 交换后，`∅-empty` 以小隶属形式驳斥它，结果是空类型的元素。注意并未主张什么：这里没有证明模型数码单独意义上的空性，只证明「属于它蕴含矛盾」，而固定方程要求的恰是这些。

```agda
module NumPin (a : ℕ → S) (q : (n : ℕ) → a n ≡ # n) where
  pinZero : (z : S) → ⟨ z ∈ˢ a zero ⟩ → Empty.⊥
  pinZero z z∈ = ∅-empty z
    (∈∈ₛ {a = z} {b = ∅} .fst (subst (λ w → ⟨ z ∈ˢ w ⟩) (q zero) z∈))

  pinSuc : (n : ℕ) (z : S)
```

后继方程是「属于 `a (suc n)`」与「属于 `a n` 或等于 `a n` 的截断析取」之间的一对转换，正是 record 字段规定的形状。第二个析取支中的相等是 `≈ˢ`，即结构的等词，所以对齐路径可直接作用于它。析取的命题性在证明中显式给出，因为截断陈述的消去器需要它。

```agda
         → (⟨ z ∈ˢ a (suc n) ⟩ → ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩)
         × (⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ → ⟨ z ∈ˢ a (suc n) ⟩)
  pinSuc n z = fwd , bwd
    where
    fwd : ⟨ z ∈ˢ a (suc n) ⟩ → ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩
```

正向，先把链中的成员资格搬到 `# (suc n)` 的成员资格，从那里适用 `sucV` 分析，消入结论的析取。第一分支中，`# n` 中的成员资格沿第 `n` 处的对齐搬回 `a n` 中的成员资格，用左注入引入截断析取。第二分支中，`z` 到 `# n` 的路径与反向对齐复合，得到 `z` 到 `a n` 的路径，取右注入。两个分支都产生截断见证，因此结果仍是纯粹的析取，绝不是已判定的情形。

```agda
    fwd z∈ = ∈sucV-elim {A = # n} {x = z}
      (snd ((z ∈ˢ a n) ⊔ (z ≈ˢ a n)))
      (subst (λ w → ⟨ z ∈ˢ w ⟩) (q (suc n)) z∈)
      (λ z∈#n → ∣ Sum.inl (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q n)) z∈#n) ∣₁)
      (λ z≡#n → ∣ Sum.inr (z≡#n ∙ sym (q n)) ∣₁)
```

反向要处理两个截断情形，因此消去器进入 `a (suc n)` 的成员命题。第一情形中，`a n` 的成员被搬到 `# n`，引理 `∈sucV-inl` 把它放进库后继，再沿后继处的对齐搬回。对齐在每一步都被双向使用，这正是把它作为对所有 `n` 一并给出的假设的原因。

```agda
    bwd : ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ → ⟨ z ∈ˢ a (suc n) ⟩
    bwd = PT.rec (snd (z ∈ˢ a (suc n)))
      (λ { (Sum.inl z∈n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n)))
             (∈sucV-inl {A = # n} (subst (λ w → ⟨ z ∈ˢ w ⟩) (q n) z∈n))
         ; (Sum.inr z≡n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n)))
```

第二情形处理右析取支，这里正是「后继包含自身」这条事实的用武之地。假设是从 `z` 到模型前驱的路径 `z ≡ a n`；把它与对齐 `q n` 复合，得到路径 `z ≡ # n`。该路径把已存的事实 `self∈sucV (# n)`，即 `# n` 属于自己的库后继，搬运为「`z` 属于 `sucV (# n)`」的陈述，最后沿后继处的对齐搬运回到链上。两个分支合起来给出完整的反向转换，为每条对齐的链完成后继固定方程。

```agda
             (subst (λ w → ⟨ w ∈ˢ sucV (# n) ⟩) (sym (z≡n ∙ q n))
               (self∈sucV (# n))) })
```

## 其余公理所需的假设

还剩两个字段，全分离与幂集，它们提出的是两个不同的小性问题。全分离要把任意的满足命题 `(y ∷ []) ⊨ φ` (住在 `Type (ℓ-suc ℓ)`) 变小，而没有 Δ₀ 见证可以徒手完成；所需的是非直谓性中的 `resizing` 分量，它逐点地为每个这样的命题给出小代表，从而使小性适配器 `separateFromSmall` 得以应用。幂集提出的是另一类问题：`a` 的候选子集是以 `⟪ a ⟫` 为索引的成员命题族，要从它造出集合，每条命题必须编码进一个固定的小类型。`hPropSmallness` 分量恰好供给这一点：一个与整个 `hProp ℓ` 等价的小类型 `Ω'`，充当命题的分类器。两个构造都不使用整个 `Impredicativity` 打包；各自只消耗它的一个分量，后面的装配把该打包作为参数，经典情形经 `lem→impredicativity` 得到。

## 幂集

幂集是库文件头明确声明不提供的那一件构造，而小分类器正是构造它的材料。`a` 的候选子集由进入分类器小载体的特征函数 `⟪ a ⟫ → Ω'` 描述；解码每个值 `χ m` 便得到索引 `m` 上的命题，凡该命题成立的索引所呈现的元素由 `sett` 收集成集合。证明建立两个收纳：函数选中的都落在给定子集内，子集的每个成员都被选中；第二个方向使用命题上「先编码再解码」的往返，再由外延性收尾。

幂集构造恰以该打包的一个成分为前提：`HPropSmallness ℓ` 的见证 `sΩ`，即 `Type ℓ` 中的小类型 `Ω'` 连同到 `hProp ℓ` 的等价。此外不假设任何东西。由该等价提取两个读法。正向映射 `decode` 把小真值变成打包在 `hProp ℓ` 中的普通命题；正是这个方向使特征函数可被读作索引上的谓词。

```agda
module Power (sΩ : HPropSmallness ℓ) where

  private
    decode : sΩ .fst → hProp ℓ
    decode = equivFun (sΩ .snd)

    encode : hProp ℓ → sΩ .fst
```

反向映射 `encode` 把 `hProp ℓ` 的命题送入小载体，而往返 `decode∘encode` 是等价的 `secEq` 一侧：把命题的编码再解码，得到指向恰该命题的路径。分类器就位后，实现族 `F` 是直接的：对特征函数 `χ`，取「索引 `m` 加上 `decode (χ m)` 成立的证明」的对，把所呈现的元素作成 `sett`。被选中的成员恰是其编码真值解码出带证明命题的那些。

```agda
    encode = invEq (sΩ .snd)

    decode∘encode : (P : hProp ℓ) → decode (encode P) ≡ P
    decode∘encode = secEq (sΩ .snd)

    F : (a : S) → (⟪ a ⟫ → sΩ .fst) → S
    F a χ = sett (Σ[ m ∈ ⟪ a ⟫ ] ⟨ decode (χ m) ⟩) (λ p → ⟪ a ⟫↪ (p .fst))
```

幂集运算本身就是一次 `sett`：索引类型是从 `⟪ a ⟫` 到小载体 `Ω'` 的函数类型，族把每个特征函数实现为上文选出的集合。于是属于 `𝒫V a` 仅仅是属于某个实现的集合：成员以「特征函数加一条从它所选集合到 `x` 的路径」的截断对出现。规格的正向表明这样的 `x` 在环境意义下是 `a` 的子集，即层级库的包含 `⊆`，而非结构的关系 `⊆ˢ`；两者的换算被分开处理，留到最后。

```agda
  𝒫V : S → S
  𝒫V a = sett (⟪ a ⟫ → sΩ .fst) (F a)

  private
    fwd : (a x : S) → ⟨ x ∈ˢ 𝒫V a ⟩ → ⟨ x ⊆ a ⟩
    fwd a x = PT.rec ((x ⊆ a) .snd) λ { (χ , p) y y∈ₛx →
```

`x ⊆ a` 的证明逐成员进行，先消去属于幂集的截断成员资格。沿呈现路径把 `y` 在 `x` 中的成员资格搬回后，它变成在所选集合 `F a χ` 中的小隶属；经 `∈∈ₛ` 转换后得到呈现纤维：索引 `m` 加上 `decode (χ m)` 成立的证明，以及一条把 `y` 与被呈现元素 `⟪ a ⟫↪ m` 等同的路径。

```agda
      PT.rec ((y ∈ₛ a) .snd)
             (λ { ((m , _) , q) → subst (λ v → ⟨ v ∈ₛ a ⟩) q (∈ₛ⟪ a ⟫↪ m) })
             (∈∈ₛ {a = y} {b = F a χ} .snd
               (subst (λ v → ⟨ y ∈ₛ v ⟩) (sym p) y∈ₛx)) }

    bwd : (a x : S) → ⟨ x ⊆ a ⟩ → ⟨ x ∈ˢ 𝒫V a ⟩
```

剩下的工作是把该纤维变成 `y` 在 `a` 中的成员资格，沿路径的搬运正好完成这一点，因为 `a` 的被呈现元素按构造就是 `a` 的成员。目标始终取命题值，所以两次截断消去都是合法的。于是幂集的任何成员，无论怎样呈现，都只收集 `a` 的成员。

反向为属于幂集构造见证，且无需选择。特征函数 `χₓ` 被显式回收：索引 `m` 被送到被呈现元素 `⟪ a ⟫↪ m` 在 `x` 中的小隶属的编码 `encode`。这是函数操作而非选择，因为嵌入的小隶属纤维不加截断。截断的对随后把 `χₓ` 与「`χₓ` 所选的集合等于 `x`」的断言打包，该断言由两个收纳 `s1`、`s2` 经外延性建立。

```agda
    bwd a x sub = ∣ χₓ , extensionality (F a χₓ) x (s1 , s2) ∣₁
      where
      χₓ : ⟪ a ⟫ → sΩ .fst
      χₓ m = encode (⟪ a ⟫↪ m ∈ₛ x)
      s1 : ⟨ F a χₓ ⊆ x ⟩
```

第一个收纳表明 `χₓ` 所选的集合没有超出 `x` 的东西。`F a χₓ` 的小成员带有索引 `m`、`decode (χₓ m)` 成立的证明，以及一条呈现路径。由于 `χₓ m` 本就定义为成员资格 `⟪ a ⟫↪ m ∈ₛ x` 的编码，往返 `decode∘encode` 把解码后的证明改写回恰是该成员资格，呈现路径再把它搬运到 `y` 上。于是所选集合的每个成员都是 `x` 的成员。

```agda
      s1 y y∈ₛF = PT.rec ((y ∈ₛ x) .snd)
        (λ { ((m , h) , q) →
          subst (λ v → ⟨ v ∈ₛ x ⟩) q
            (subst ⟨_⟩ (decode∘encode (⟪ a ⟫↪ m ∈ₛ x)) h) })
        (∈∈ₛ {a = y} {b = F a χₓ} .snd y∈ₛF)
```

第二个收纳要反向进行：从 `x` 的任意成员 `y`，造出 `F a χₓ` 的一个小成员。收纳前提 `sub` 先给出 `y` 在 `a` 中的呈现纤维，其第二分量证明被呈现元素与 `y` 有相同的成员。这里双向使用嵌入的呈现，因此无需选取任何东西：纤维是不加截断的数据，抽出 `⟪ a ⟫↪ m₀ ≡ y` 的路径 `q` 将作为普通项可用。

```agda
      s2 : ⟨ x ⊆ F a χₓ ⟩
      s2 y y∈ₛx = ∈∈ₛ {a = y} {b = F a χₓ} .fst ∣ (m₀ , h) , q ∣₁
        where
        m₀ = sub y y∈ₛx .fst
        q : ⟪ a ⟫↪ m₀ ≡ y
```

路径 `q` 由对收纳前提的等成员数据应用 `identityPrinciple` 得到，于是被呈现元素 `⟪ a ⟫↪ m₀` 等于 `y`。把 `y` 在 `x` 中的成员资格沿 `q` 反向搬运，落到被呈现元素上；由往返，这恰是 `decode (χₓ m₀)` 解码出的命题：`χₓ m₀` 本就定义为恰好这个成员资格的编码。于是索引与搬运后证明构成的对 `(m₀ , h)` 居于定义 `F a χₓ` 的类型中，见证 `y` 在所选集合里。两个收纳就位后，`power-spec` 把这条等价与「环境包含 `⊆` 与结构的子集关系 `⊆ˢ` 之间逐点交换」复合，为字段 `hasPower` 给出一个集合，其隶属作为真值等于 record 所陈述的子集关系。

```agda
        q = equivFun identityPrinciple (sub y y∈ₛx .snd)
        h : ⟨ decode (χₓ m₀) ⟩
        h = subst ⟨_⟩ (sym (decode∘encode (⟪ a ⟫↪ m₀ ∈ₛ x)))
                  (subst (λ v → ⟨ v ∈ₛ x ⟩) (sym q) y∈ₛx)

  power-spec : (a x : S) → (x ∈ˢ 𝒫V a) ≡ (x ⊆ˢ a)
```

规格 `power-spec` 复合两个真值等式。第一个是刚证的主等价：属于 `𝒫V a` 等于环境意义下的包含 `x ⊆ a`，后者量化于实际成员之上，不加截断。第二个把环境包含转换成结构自己的子集关系 `x ⊆ˢ a`，它经由结构的成员关系 `∈ˢ` 陈述：给定把 `x` 的每个普通成员送到 `a` 的普通成员的函数，`∈∈ₛ` 的两个方向逐点互换两种隶属记号。复合所得正是幂集字段收到的数据：集合 `𝒫V a` 的隶属作为真值恰是 record 所述的子集关系。也请注意各小性输入进入之处：分离逐点消耗 `resizing`，而幂集仅由 `hPropSmallness` 构成。

```agda
  power-spec a x =
    ⇔toPath {P = x ∈ˢ 𝒫V a} {Q = x ⊆ a} (fwd a x) (bwd a x)
    ∙ ⇔toPath {P = x ⊆ a} {Q = x ⊆ˢ a}
      (λ s y y∈x → ∈∈ₛ {a = y} {b = a} .snd (s y (∈∈ₛ {a = y} {b = x} .fst y∈x)))
      (λ f y y∈ₛx → ∈∈ₛ {a = y} {b = a} .fst (f y (∈∈ₛ {a = y} {b = x} .snd y∈ₛx)))
```

## 证明 V ⊨ ZF

模型 record 的每个字段如今都有了见证；本节把它们组装成单个数学定理：累积层级满足 ZF。公理按其来源分组。空集、配对与并是章首转换过的所需的基本集合。全分离与幂集是两个小性结果，各自消耗非直谓性打包的一个分量：分离用 `resizing` 使每个满足命题变小，从而 `separateFromSmall` 得以应用；幂集只用小分类器。替换是由不加截断的纤维造出的像；无穷是库中的 `ω` 连同数码对齐。剩下的是一步打包，但其中有一个真正的数学输入：`isZFModel` 的每个字段要求 `isContr (SetOf Q)`，即实现集合连同把一切实现者收缩到它的紧缩，而外延性经 `setOf-unique` 恰好给出这个紧缩。定理 `V⊨ZF-impredicative` 假设打包 `Impredicativity ℓ`；定理 `V⊨ZF` 改为假设 `LEM (ℓ-suc ℓ)`，并经 `lem→impredicativity` 导出该打包。

组装以打包 `Impredicativity ℓ` 为参数，其两个字段分别供给两个小性构造：`hPropSmallness` 交给上一节的幂集构造，那里只用分类器；`resizing` 则是分离所用的。全分离直接陈述：给定集合 `a` 与带一个自由变元槽的公式 `φ`，给出集合 `s`，使得对每个 `y`，真值 `y ∈ˢ s` 按路径等于「`y ∈ˢ a`」与「`φ` 在单元环境 `y ∷ []` 下满足」的合取。这正是模型 record 所要求分离规格的形状。

```agda
module VModel (imp : Impredicativity ℓ) where
  open Impredicativity imp
  open Power hPropSmallness public

  separateFull : (a : S) (φ : Formula S 1)
               → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ)))
```

分离是小性一章的适配器的一次应用。`separateFromSmall` 取 `a` 上的谓词 `P : S → hProp (ℓ-suc ℓ)` 与每个取值的小性见证，返回带路径规格 `y ∈ˢ s ≡ (y ∈ˢ a) ⊓ P y` 的集合 `s`。这里的谓词是 `λ y → (y ∷ []) ⊨ φ`，即 `φ` 在每个单元环境下的满足；其在各点的小性就是在该点应用的 `resizing`。对 `φ` 的形状无需任何前提：无论公式是什么，降层都为每个满足命题指派一个小代表。有了 `separateFull`，便可从已证的见证组装出类型为 `isZFModel` 的定理 `V⊨ZF-impredicative`。

```agda
  separateFull a φ =
    separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → resizing ((y ∷ []) ⊨ φ))

  V⊨ZF-impredicative : isZFModel
  V⊨ZF-impredicative = record
    { extensional    = extensionalV
```

第一组条目复用章首的转换。空集、配对与并的显式实现者分别是库集合 `∅`、`⁅ a , b ⁆`、`⋃ a`，连同在那里证明的规格；`extensional` 与 `regularity` 两项引用层级一章所证的见证。分离的实现者是 `separateFull a φ`，即分离集与规格组成的对，已恰为字段要求的形状。每个字段都是其参数的函数，所以模式的每个实例、对每个公式都一次给出。

```agda
    ; regularity     = regularityV
    ; hasEmpty       = one _ (∅ , empty-spec)
    ; hasPair        = λ a b → one _ (⁅ a , b ⁆ , pair-spec a b)
    ; hasUnion       = λ a → one _ (⋃ a , union-spec a)
    ; hasSeparation  = λ a φ → one _ (separateFull a φ)
```

接下来两个条目消费中段的构造。替换字段接收函数性前提 `fc`，以像 `replaceImage` 及其规格为实现者；幂集字段取 `𝒫V a` 及 `power-spec`，即仅由小分类器造出的构造。数码链占据三项：运算 `numeralV` 本身，以及两条固定方程，`numeral-zero` 说没有元素居于 `numeralV zero`，`numeral-suc` 给出 `numeralV (suc n)` 的「成员或前驱」二分。两条方程都来自把 `NumPin` 引理应用于对齐 `numeralV≡#`，因此其内容恰是该对齐加上 `sucV` 分情形分析。

```agda
    ; hasReplacement = λ a φ fc → one _ (replaceImage a φ fc , replaceImage-spec a φ fc)
    ; hasPower       = λ a → one _ (𝒫V a , power-spec a)
    ; numeral        = numeralV
    ; numeral-zero   = NumPin.pinZero numeralV numeralV≡#
    ; numeral-suc    = NumPin.pinSuc numeralV numeralV≡#
```

最后一个字段是强无穷，由 `ω` 及其规格实现：`ω` 的每个成员都仅仅是某个模型数码，这正是 record 的要求。辅助定义 `one` 用一行记录收尾所有存在性字段的一般原则。对任何类 `Q : S → hProp (ℓ-suc ℓ)`，`SetOf Q` 的一个元素，即实现集合连同其规格，已足以确定 `isContr (SetOf Q)` 的元素，因为把 `setOf-unique` 应用于外延性，就能把一切实现者收缩到给定者。于是上面每个显式实现者都变成其字段所需的紧缩数据，外延性在 `one` 中引用一次，而不必在每个条目里重复。

```agda
    ; hasInfinity    = one _ (ω , ω-specV) }
    where
    one : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q)
    one = setOf-unique extensionalV
```

定理 `V⊨ZF-impredicative` 陈述：在单一假设 `Impredicativity ℓ` 下，累积层级满足 ZF。两个模式字段都是接受一切公式的函数，因此分离与替换对所有公式一次成立，其中用到一阶逻辑诸章对对象语言的深嵌入。第二个定理把打包换成标准经典假设：`V⊨ZF` 取 `LEM (ℓ-suc ℓ)`，并从中导出该打包。所证的是在所述假设下的模型构造，而非无条件的无矛盾性断言。

`V⊨ZF` 的定义是一次复合：排中律实例经 `lem→impredicativity` 转为打包，其结果交给 `VModel.V⊨ZF-impredicative`。在该转换 (来自经典一章) 中，降层字段在其自身层级使用 `lem`，而分类器字段先用 `lowerLEM` 把实例下降一个后继步，再构造以 `Lift Bool` 呈现 `hProp ℓ` 的等价。于是后继层上的一条假设同时到达模型消耗的两个字段：分离经由降层，幂集经由分类器。

```agda
V⊨ZF : LEM (ℓ-suc ℓ) → isZFModel
V⊨ZF lem = VModel.V⊨ZF-impredicative (lem→impredicativity lem)
```

## 另行假设选择公理

排中律推不出选择，因此 ZFC 的最后一条公理被另立为假设，选择集公理由它证明。接口是 `SetChoice`：对 h-集合 `X : Type ℓ` 与族 `B : X → Type ℓ`，若每个纤维仅仅居有，则整个 `X` 上存在选择函数，以截断的形式给出。下面的引理假设该接口在层级 `ℓ` 的一个实例，连同固定层级结构 `𝒮ᵥ` 上的一个 `isZFModel`，并从中使用交 `∩` 及其规格。被施加选择的族是一个小呈现：索引类型是 `⟪ a ⟫`，它是一个 h-集合；索引 `m` 上的纤维是 `m` 所呈现的集合 `⟪ ⟪ a ⟫↪ m ⟫`。因此选择选出的是呈现索引，而非集合的元素。由被选索引经一次 `sett` 造出集合 `c`；再由两两不交前提 `disj`，经由模型的交证明 `c` 与 `a` 的每个成员的交是可缩从而唯一的点集。截断在设计上是不对称的：选择集本身仅仅是存在，而每个交都携带显式的 `isContr` 数据。最终定理把一个 `SetChoice (ℓ-suc ℓ)` 实例用两次：`choice→lem` 把它转为 `LEM (ℓ-suc ℓ)` 供 ZF 部分使用，`lowerSetChoice` 把它降到 `SetChoice ℓ` 供选择引理使用。所以 `V⊨ZFC` 单凭选择而证；排中律由选择经 Diaconescu 定理回收，而非相反。

选择集构造要用到两条预备事实。第一条关乎施加选择的索引类型。每个呈现类型 `⟪ a ⟫` 都是 h-集合：它经 `⟪ a ⟫↪` 嵌入层级，而嵌入性质 `isEmb⟪ a ⟫↪` 在引入该呈现时已记录；层级本身由 `setIsSet` 是 h-集合。cubical 的一般结果 `Embedding-into-isSet→isSet` 沿嵌入把 h-集合性传回，于是对每个集合 `a` 都有 `isSet⟪ a ⟫`。索引之间的相等类型因此都是命题，这正是 `SetChoice` 对其选择对象类型所要求的条件。

```agda
private
  isSet⟪_⟫ : (a : S) → isSet ⟪ a ⟫
  isSet⟪ a ⟫ = Embedding-into-isSet→isSet (⟪ a ⟫↪ , isEmb⟪ a ⟫↪) setIsSet

  isContrΣ-fromCenter : {P : S → hProp (ℓ-suc ℓ)} (z₀ : S) (p₀ : z₀ ∈ᶜ P)
                      → ((z : S) → z ∈ᶜ P → z₀ ≡ z)
```

第二条事实把唯一性论证打包成紧缩性数据。对载体上的类 `P`，假设有中心 `z₀` 及其实现 `p₀`，并有紧缩把每个实现 `z` 送到路径 `z₀ ≡ z`。那么「集合加 `P` 的实现」的序对类型是紧缩的，中心为 `(z₀ , p₀)`。序对之间的紧缩用 `Σ≡Prop` 构造：只需给出第一分量间的路径，因为每个 `P v` 是命题，第二分量随之确定。选择集结论恰是这种形状：一个交点，在 `isContr` 意义下唯一。引理的前提随之取定：它假设固定结构 `𝒮ᵥ` 上任意一个 `isZFModel`，只从中使用模型的交 `∩` 及其规格 `∩-spec`，再加上 `SetChoice ℓ` 的一个实例。

```agda
                      → isContr (Σ[ z ∈ S ] (z ∈ᶜ P))
  isContrΣ-fromCenter {P} z₀ p₀ u =
    (z₀ , p₀) , λ w → Σ≡Prop (λ v → snd (P v)) (u (w .fst) (w .snd))

module ChoiceLemma (zf : isZFModel) (ac : SetChoice ℓ) where
  open Model.isZFModel zf using ( _∩_; ∩-spec )
```

引理 `choice` 陈述经典的选择集情形。前提是：`inh` 说 `a` 的每个成员 `x` 仅仅居有，故族由非空集组成；`disj` 说 `a` 的两个成员哪怕仅仅共享一个元素就已相等，故族两两不交。结论是一个**仅仅存在**的集合 `c`，使得对 `a` 的每个成员 `x`，与 `c ∩ x` 相交的点的类型是紧缩的。截断是不对称的：选择集本身不作为数据给出，只有其截断居有；而每个交点的唯一性却是显式的 `isContr` 数据。

```agda
  choice : (a : S)
         → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
         → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
              → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
         → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
```

证明把选择实例施加在族的小呈现上，而非族本身。索引类型是 `⟪ a ⟫`，由第一条预备事实它是 h-集合；族是 `λ m → ⟪ ⟪ a ⟫↪ m ⟫`，即每个索引所呈现的集合。剩下的只需让每个纤维仅仅居有，这正是 `pick` 的作用：对每个索引 `m`，由 `inh` 在 `memb a m` 所证明的成员处得到所呈现集合 `⟪ a ⟫↪ m` 的成员仅仅存在，`∈-asFiber` 再从该成员资格提取指向 `⟪ a ⟫↪ m` 之呈现的实际索引。输入上的截断全程保持，所以 `pick` 从不宣称在 `a` 的成员内部选了点；它只是给单纯的存在重新编号。

```agda
              → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
  choice a inh disj = PT.map mk (ac ⟪ a ⟫ isSet⟪ a ⟫ (λ m → ⟪ ⟪ a ⟫↪ m ⟫) pick)
      where
      pick : (m : ⟪ a ⟫) → ∥ ⟪ ⟪ a ⟫↪ m ⟫ ∥₁
      pick m = PT.map
```

选择函数随后对每个索引 `m` 返回所呈现集合的一个实际元素 `g m`：对索引之 h-集合的选择给出不加截断的数据，即 `⟪ a ⟫↪ m` 之呈现的一个元素。其余部分 `mk` 把它打包成结论：集合 `c`，加上对 `a` 的每个成员 `x`，与 `c ∩ x` 相交的点类型的紧缩数据。由于选择函数在索引层产生的已是不加截断的数据，`mk` 是普通函数；截断只在整体被 `PT.map` 包装时重新出现。这正是选择集本身只是纯粹存在、而每个交都携带显式 `isContr` 数据的原因。

```agda
        (λ { (y , y∈) → ∈-asFiber {a = y} {b = ⟪ a ⟫↪ m} y∈ .fst })
        (inh (⟪ a ⟫↪ m) (memb a m))
      mk : ((m : ⟪ a ⟫) → ⟪ ⟪ a ⟫↪ m ⟫)
         → Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
              → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩))
```

在 `mk` 内部，把选出的数据加以解释。`g m` 返回的是指向 `⟪ a ⟫↪ m` 之呈现的索引，与该呈现复合后得到实际的集合 `chosen m`，即索引 `m` 所指成员的一个成员。选择集就是 `c = sett ⟪ a ⟫ chosen`：为每个索引选出的集合，经层级集合构造器的一次应用收集起来。

```agda
      mk g = c , uniq
        where
        chosen : ⟪ a ⟫ → S
        chosen m = ⟪ ⟪ a ⟫↪ m ⟫↪ (g m)
        c : S
```

在唯一性之前先记录关于 `c` 的一条事实：每个被选集合确实是它来源成员的成员。这由呈现得出：指向集合呈现的索引 `g m` 经 `∈ₛ⟪ ⟫↪` 是小成员资格，`∈∈ₛ` 把它提升为结构性成员资格 `⟨ chosen m ∈ˢ ⟪ a ⟫↪ m ⟩`。有了第二条预备事实的唯一性辅助，`uniq` 成为三段论证：中心、中心居于交中的证明、以及把其他交点紧缩到中心的紧缩。

```agda
        c = sett ⟪ a ⟫ chosen
        chosen∈ : (m : ⟪ a ⟫) → ⟨ chosen m ∈ˢ ⟪ a ⟫↪ m ⟩
        chosen∈ m = ∈∈ₛ {a = chosen m} {b = ⟪ a ⟫↪ m} .snd (∈ₛ⟪ ⟪ a ⟫↪ m ⟫↪ (g m))
        uniq : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)
        uniq x x∈a = isContrΣ-fromCenter {P = λ z → z ∈ˢ (c ∩ x)} z₀ pf₀ uniqz
```

中心这样计算。`a` 的成员 `x` 有不加截断的呈现纤维：`∈-asFiber` 给出索引 `m₀` 及呈现 `x` 的路径 `mf .snd`。交点取该索引处的被选集合 `z₀ = chosen m₀`。这正是不加截断的纤维再次发挥作用之处：从成员资格回收索引是函数而非选择，因此中心的定义无需调用选择实例。

```agda
          where
          mf = ∈-asFiber {a = x} {b = a} x∈a
          m₀ = mf .fst
          z₀ = chosen m₀
          pf₀ : ⟨ z₀ ∈ˢ (c ∩ x) ⟩
```

中心必须居于交 `c ∩ x` 中。由模型的 `∩-spec`，交中的成员资格作为真值等于「属于 `c`」与「属于 `x`」的合取，证明沿对称化后的规格进行搬运。属于 `c` 的部分以自反路径仅仅见证 `z₀` 在索引 `m₀` 处被选，而 `m₀` 呈现 `x`；属于 `x` 的部分由把 `chosen∈ m₀` 沿该呈现路径搬运得到。两部分作为截断的序对合取。剩下的任务是紧缩 `uniqz`：它须把交 `c ∩ x` 中的每个 `z` 送到路径 `z₀ ≡ z`。

```agda
          pf₀ = subst ⟨_⟩ (sym (∩-spec c x z₀))
                  ( ∣ m₀ , refl ∣₁
                  , subst (λ w → ⟨ z₀ ∈ˢ w ⟩) (mf .snd) (chosen∈ m₀) )
          uniqz : (z : S) → ⟨ z ∈ˢ (c ∩ x) ⟩ → z₀ ≡ z
          uniqz z pf = PT.rec (setIsSet z₀ z)
```

紧缩是较精巧的一半。取交 `c ∩ x` 中的任意 `z`；交中的成员资格经 `∩-spec` 搬运为截断的合取 `zcx`。第一分量仅仅说 `z` 居于某个被选集合：即索引 `m` 加上从 `z` 到 `chosen m` 的作为 `c` 成员的路径 `q`。由 `chosen∈`，`chosen m` 是 `⟪ a ⟫↪ m` 的成员，沿 `q` 搬运便知 `z` 也是该成员的成员。于是 `z` 是 `a` 的成员 `x` 与 `⟪ a ⟫↪ m` 的公共元素，不交性随即适用：`disj` 给出路径 `x ≡ ⟪ a ⟫↪ m`。两个成员呈现同一集合，所以它们的呈现索引一致：呈现是嵌入，从而在索引上单射，把复合后的路径交给 `isEmbedding→Inj` 即得 `m ≡ m₀`。因此 `chosen m ≡ chosen m₀ = z₀`，与 `q` 复合即得紧缩路径 `z₀ ≡ z`。目标是 h-集合的元素之间的路径，因而是命题，这正允许在此消去截断。

本章最终定理的记账是精确的。`SetChoice (ℓ-suc ℓ)` 的一个实例被使用两次：`choice→lem` 把它转为 `LEM (ℓ-suc ℓ)`，经 `V⊨ZF` 驱动 ZF 部分；`lowerSetChoice` 把同一实例降到 `SetChoice ℓ`，供给 `ChoiceLemma` 作选择集部分。选择集只是纯粹地存在，而每个交由显式的紧缩数据唯一确定。

```agda
              (λ { (m , q) →
                let z∈m : ⟨ z ∈ˢ ⟪ a ⟫↪ m ⟩
                    z∈m = subst (λ w → ⟨ w ∈ˢ ⟪ a ⟫↪ m ⟩) q (chosen∈ m)
                    x≡m : x ≡ ⟪ a ⟫↪ m
                    x≡m = disj x (⟪ a ⟫↪ m) x∈a (memb a m)
```

把不交性用于 `a` 的两个成员 `x` 与 `⟪ a ⟫↪ m`，以公共元素 `z` 为重叠的见证；前提 `disj` 返回路径 `x ≡ ⟪ a ⟫↪ m`。于是两个索引呈现同一成员，而呈现 `⟪ a ⟫↪` 是嵌入，从而在索引上单射：把复合 `sym x≡m ∙ sym (mf .snd)` 交给 `isEmbedding→Inj`，便得 `m ≡ m₀`。对该路径施加 `chosen` 并与 `q` 复合，即产生紧缩所需的路径 `z₀ ≡ z`。目标 `z₀ ≡ z` 是 h-集合 V 的元素之间的路径，因而是命题，这正允许在此消去分情形的截断。

```agda
                            ∣ z , zcx .snd , z∈m ∣₁
                    m≡m₀ : m ≡ m₀
                    m≡m₀ = isEmbedding→Inj isEmb⟪ a ⟫↪ m m₀
                             (sym x≡m ∙ sym (mf .snd))
                in sym (cong chosen m≡m₀) ∙ q })
```

合取 `zcx` 由把 `pf` 沿路径 `∩-spec c x z` 搬运得到，它把 `c ∩ x` 中的成员资格改写成两个成员命题的普通序对。两个分量随后分开使用：第一个进入上一步的不交性见证，第二个进入 `z` 的成员资格搬运 `z∈m`。中心与紧缩就位后，`uniq` 为 `a` 的每个成员供给 `isContr` 数据，`mk` 返回集合 `c` 连同这些数据。选择集本身只是作为命题截断的一个元素纯粹存在；相比之下，每个交的唯一性是不加截断的显式 `isContr` 数据。

```agda
              (zcx .fst)
            where
            zcx : ⟨ z ∈ˢ c ⟩ × ⟨ z ∈ˢ x ⟩
            zcx = subst ⟨_⟩ (∩-spec c x z) pf
```

## V ⊨ ZFC：单凭选择

上一节的引理与 ZF 定理在此会合。构造 `ChoiceLemma.choice` 是对固定层级结构、在两条明示前提下证明的：该结构上任意一个 `isZFModel`，以及 `SetChoice ℓ` 的一个实例。其索引类型是小呈现 `⟪ a ⟫`，是一个 h-集合，因此选择选出的是族的呈现索引；随后不交性证明每个交可缩。于是选择集仅仅存在，而每个交点作为显式 `isContr` 数据唯一。定理 `V⊨ZFC` 陈述的正是合并后的精确代价：`SetChoice (ℓ-suc ℓ)` 经 `choice→lem` 为 ZF 部分给出 `LEM (ℓ-suc ℓ)`，同一实例经 `lowerSetChoice` 降为 `SetChoice ℓ`，驱动选择集引理。所证的是所述假设下的模型构造，而非无条件的证明。

定理的前提是单个实例：`SetChoice (ℓ-suc ℓ)`，即模型真值层的后继上的集合层选择。结论 `isZFCModel` 把一个 ZF 模型与内部的选择集见证打包在一起，因此证明同时给出两个分量。ZF 部分被命名为 `base`，因为选择集引理要以 ZF 模型为输入。

```agda
V⊨ZFC : SetChoice (ℓ-suc ℓ) → isZFCModel
V⊨ZFC ac = record
  { zf = base ; hasChoice = ChoiceLemma.choice base (lowerSetChoice ac) }
  where
  base : isZFModel
```

单个实例被用于两个结论。`choice→lem` 把它转为层 `ℓ-suc ℓ` 的排中律，恰是 `V⊨ZF` 所期望的前提，由此得到 `base`。选择集部分则由 `lowerSetChoice` 把同一实例降到 `SetChoice ℓ`，这正是 `ChoiceLemma.choice` 所需要的，引理随即应用于 `base`。于是，后继层上的一例选择经排中律给出 ZF 模型，其低一层的形式给出选择集公理。

```agda
  base = V⊨ZF (choice→lem ac)
```

## 小结

本章的记账至此完成。空集、配对与并经由 `∈∈ₛ` 和 `⇔toPath` 从既有构造转换而来；替换沿未加截断的纤维经 `sett` 直接得到；强无穷是 `ω` 的定义再加一次链对齐 (`numeralV≡#`)。剩下两条，全分离与幂集，所需的恰是 `Base.Impredicativity` 打包的 `Impredicativity`：合龙以此精确代价给出 `V⊨ZF-impredicative`，排中律把它提升为主要的 `V⊨ZF`。最后一个条件是一个独立的、再另加的集合层选择实例：`SetChoice (ℓ-suc ℓ)` 为 ZF 部分给出 `LEM (ℓ-suc ℓ)`，同一实例降到 `SetChoice ℓ` 后驱动选择集引理，于是得到 `V⊨ZFC`。可构造宇宙诸章将要向内考察的那个宇宙，至此已经构造完成。