在可构造层级中定位序数

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

序数在可构造层级中的位置由隶属关系控制：它会在自身的后继层出现，却不会早于自身的秩出现。本章证明两个方向，并给出在层内部识别序数的有界公式。

关于塔还有一个问题悬而未决，而无穷公理正系于此：给定一层，到那时为止究竟出现了哪些序数？答案十分简洁。Lset α 中的序数恰是 α 的成员，故塔的索引与它的序数内容逐层一致，而序数首次现身于自身之后的那一层。

两个方向都有实质难度。一个方向说序数不会提前现身：若它在 Lset α 中，则它是 α 的成员。这是较难的一半，要经过秩，而这正是这里需要秩构造的原因。Lset α 中的集合是某个更早层的可定义子集，依归纳其成员的秩低于那一层，故它自身的秩有界；而作为序数，它就是自身的秩。

另一个方向说明序数不会延迟出现：α 的每个成员都已经在 Lset α 中。这一半由直接归纳证明，所用陈述正是序数会在自身之后的层出现。这里没有循环：归纳假设为各个成员提供该陈述，而证明所需的也只有这些成员。

两半齐备，一层中的序数便由单一公式「是序数」从中选出，该公式是 Δ₀ 的，因为传递性只用有界量词就能表述。于是 α 是 Lset α 的可定义子集，后继层的可定义幂集子句随即可以应用。

本章在一个固定的宇宙层级 ℓ 内工作，以下关于集合、隶属与 L 的层的全部论述都在这一层级上。我们假设层级 ℓ-suc ℓ 上的排中律。它在数学上的唯一用途是序数三歧：对两个序数，返回两个方向的隶属关系之一或相等这一情形。后文的所有结论都经下一节建立的两次比较引理继承这种经典性。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Ordinal.Stages {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

这里交汇了两类词汇。来自环境层级 V 的是基本动作：集合 S 上的隶属 ∈ˢ、冯·诺伊曼后继 sucV、沿隶属的归纳法与隶属的非自反性。来自可构造一侧的是层 Lset α 本身、可定义子集层 𝒟ₒ，以及把某层中的隶属与它的可定义幂集中的隶属联系起来的两个方向 Lset-in 与 Lset-out。本章的陈述完全落在这个交集里：它问的是序数在各个 Lset α 之间的位置。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧; δ-∀∈ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-irrefl )

序数以谓词 IsOrd 进入：一个集合是序数，当且仅当它是传递的且它的每个成员都是传递的。这是冯·诺伊曼式的读法，其中序数 α 就是所有更小序数的集合，因此问序数是否已在某层出现，字面上就是隶属问题。相应的闭包事实是 mem-ord 与 suc-ord：序数的成员是序数，序数的后继是序数。它们保证论证中的每层指标都是序数。

open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}
  using ( IsOrd; isTransV; Lset; Lset-layer; layer-trans
        ; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv; Lset-mono; Lset-in; Lset-out )

一切背后的判定程序是 ord-tri：给定两个各自被证明为序数的序数，它回答三种情形中的哪一种成立，即 a ∈ b、a = b 或 b ∈ a。它使用上述排中律假设。三歧比较以和类型返回三个情形，不可能的分支落入空类型。另一方面，命题截断 ∣_∣₁ 记录层分解所需的较早层仅仅存在。

open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Rank {ℓ} using ( rank; rank-upper; rank-ord; rank-fix )

open import Cubical.Data.Sum as Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty

秩构造提供如下三条性质。对集合 x，rank x 是一个序数，刻画 x 在累积层级中所处的深度；rank-ord 证明它是序数，rank-fix 把序数的秩等同于该序数本身，rank-upper 由各成员秩的上界给出该集合秩的上界。这三条正是较难方向所需的事实。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; extensionality; _⊆_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions

为了把外围隶属与层上的公式联系起来，集合 A 有一个选定的呈现 ⟪ A ⟫，∈-asFiber 把 A 中的成员转为指名该成员的指标。互相包含则通过 extensionality 给出集合相等。公式的满足解释直接在 hProp 中：每个公式表示一个 hProp。这些对应使论证可以在集合、其指标与有界公式之间转换。

  using ( module InfinitySet )
open InfinitySet using ( sucV )

open hPropStructure 𝒮ᵥ

两次比较

三歧比较只留下三个数学情形。若 a ∈ b，则 a 也属于 b 的后继；若 a = b，则 a 作为新增的顶端元素属于该后继。余下的 b ∈ a 将由包含关系 a ⊆ b 排除。

设集合 a 与 b 满足 a ⊆ b，用三歧性比较二者。若 a 是 b 的成员，第一个辅助件调用 ∈sucV-inl：b 的成员自动是 sucV b 的成员，因为后继是 b 连同它的单点集。若 a 等于 b，第二个辅助件沿路径 a ≡ b 传递事实 self∈sucV b，即 b 属于自身的后继。三种情形中两种已经关闭。

private
  ∈-case : (a b : S) → ⟨ a ∈ˢ b ⟩ → ⟨ a ∈ˢ sucV b ⟩
  ∈-case a b a∈b = ∈sucV-inl a∈b

  ≡-case : (a b : S) → a ≡ b → ⟨ a ∈ˢ sucV b ⟩
  ≡-case a b a≡b = subst (λ w → ⟨ w ∈ˢ sucV b ⟩) (sym a≡b) (self∈sucV b)

余下情形是 b ∈ a，而包含关系将它排除：由 b ∈ a 与 a ⊆ b 可得 b ∈ b，这与 ∈-irrefl 矛盾。由此矛盾可推出目标 a ∈ sucV b。因此，对序数 a 与 b，包含 a ⊆ b 强制 a ∈ sucV b。

  wit-case : (a b : S) → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩)
           → ⟨ b ∈ˢ a ⟩ → ⟨ a ∈ˢ sucV b ⟩
  wit-case a b a⊆b b∈a = Empty.rec (∈-irrefl b (a⊆b b b∈a))

⊆→∈suc : (a b : S) → IsOrd a → IsOrd b
       → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩) → ⟨ a ∈ˢ sucV b ⟩

这是第一次使用经典的序数比较。三歧结果返回之后的推理都是构造性的；下面关于后继的第二个比较会再使用同一原理。

⊆→∈suc a b orda ordb a⊆b = Sum.rec
  (∈-case a b)
  (Sum.rec (≡-case a b) (wit-case a b a⊆b))
  (ord-tri a orda b ordb)

现在设 β ∈ α。用三歧性比较 sucV β 与 α，结果要么后继仍位于 α 内，要么它等于 α，要么 α 位于 sucV β 内。类型 Out β α 记录前两种可能；第三种将与 β ∈ α 矛盾。

不可能的情形在 overshoot 内部排除，它的前提恰是两个不能同时成立的事实：α 属于 sucV β，而 β 属于序数 α。用 ∈sucV-elim 展开 sucV β 中成员的事实，得到两个子情形：α ∈ β，或 α = β。该消去原则要求目标是命题，而空类型 ⊥* 正是命题，于是两个分支都可以终止于矛盾。

private
  Out : S → S → Type (ℓ-suc ℓ)
  Out β α = ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

  overshoot : (β α : S) → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ α ∈ˢ sucV β ⟩ → Out β α
  overshoot β α ordα β∈α α∈sβ = Empty.rec*

第一个子情形给出隶属链 α ∈ β ∈ α。α 的传递性，即其第一分量 ordα .fst，将这条链复合为 α ∈ α。第二个子情形中，α = β 沿反向路径传递 β ∈ α，同样得到 α ∈ α。两者都与 ∈-irrefl 矛盾，因此这个不可能的第三种情形推出所需结论 Out β α。

    (∈sucV-elim {A = β} {x = α} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* α∈sβ
      (λ α∈β → lift (∈-irrefl α (ordα .fst α∈β β∈α)))
      (λ α≡β → lift (∈-irrefl α (subst (λ w → ⟨ w ∈ˢ α ⟩) (sym α≡β) β∈α))))

suc∈or≡ : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
        → ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

引理本身接着在 sucV β 与 α 之间运行三歧性，二者都被证明为序数，sucV β 经 suc-ord。前两种情形已经具有所需形状，隶属或相等，直接返回即可。

suc∈or≡ β α ordβ ordα β∈α = go (ord-tri (sucV β) (suc-ord ordβ) α ordα)
  where
  go : (⟨ sucV β ∈ˢ α ⟩ ⊎ ((sucV β ≡ α) ⊎ ⟨ α ∈ˢ sucV β ⟩)) → Out β α
  go (inl s∈α)        = inl s∈α
  go (inr (inl s≡α))  = inr s≡α

第三种情形 α ∈ sucV β 恰是 overshoot 的前提，代入已有假设 β ∈ α 即完成分析。结论 suc∈or≡ 是「不越头」的锐利形式：在 α 之下，α 各成员的后继层从不停留在严格超出 α 的位置。

  go (inr (inr α∈sβ)) = overshoot β α ordα β∈α α∈sβ

而它所服务的累积引理则是：在自身后继层现身过的序数，在此后每层都已现身，其中「此后」指索引在其之上。

这是「β 在 sucV β 现身」这一逐点陈述与「α 的每个成员都在 Lset α 中」这一层陈述之间的桥。给定 β ∈ α，后继 sucV β 或位于 α 内部、或与之重合，无论哪种情形，较小层中的隶属都会转化为 Lset α 中的隶属。

隶属分支使用层的单调性：Lset-mono 说若 γ ∈ δ 则 Lset γ 包含于 Lset δ，于是较早层的成员是较晚层的成员。此处 γ = sucV β、δ = α，恰是 suc∈or≡ 的第一种情形。

private
  cumul-∈ : (β α : S) → ⟨ sucV β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset (sucV β) ⟩
          → ⟨ β ∈ˢ Lset α ⟩
  cumul-∈ β α s∈α = Lset-mono {α = α} {β = sucV β} s∈α {x = β}

  cumul-≡ : (β α : S) → sucV β ≡ α → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩

相等分支是退化情形：当 sucV β 不严格在下而是等于 α 时，Lset (sucV β) 中的隶属已经是 Lset α 中的隶属，沿该路径的传递把这一点变成字面事实。Lset-cumul 的陈述取两个序数证书与现身假设，并按 suc∈or≡ 分派。

  cumul-≡ β α s≡α = subst (λ w → ⟨ β ∈ˢ Lset w ⟩) s≡α

Lset-cumul : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
           → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩
Lset-cumul β α ordβ ordα β∈α β∈Lsβ =
  Sum.rec (λ s∈α → cumul-∈ β α s∈α β∈Lsβ)

注意结果的形状：它并未直接断言对所有 β ∈ α 都有 β ∈ Lset α，因为在后继层的现身仍是假设。最后的定理将用归纳给出该假设，而这条引理恰是把假设转化为层内容的那一步。

          (λ s≡α → cumul-≡ β α s≡α β∈Lsβ)
          (suc∈or≡ β α ordβ ordα β∈α)

没有东西早于自身的秩现身

若一个集合属于 Lset α，其秩便以 α 为界。对于秩等于自身的序数，这说明它不能在更早层出现。

这是较难的一半。沿层索引归纳：Lset α 中的集合落在某个 β ∈ α 的 Lset β 的可定义子集里，故它是 Lset β 的子集；于是依归纳假设它的每个成员的秩都在 β 中；故它自身的秩，即那些秩的后继之并，包含于 β；三歧比较给出它属于 β 的后继，从而属于 α。

关于归纳的一点记法说明：截断存在式中的成员关系本身也是截断的，归纳按截断形式 β ∈ᵗ α 陈述，而非按显式成员。目标是一个隶属陈述，因而是命题，所以用 PT.rec 消去该截断是合法的。

陈述同时对所有序数 α 量化，∈-induction 施加于作为 α 之函数的整个谓词，序数证书作为参数一路携带。归纳是沿 α 上的隶属进行的，故在 α 处的归纳假设谈论的是 α 的成员 β，而不是按任何次序排列的「更早层」。

rank-Lset : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
rank-Lset = ∈-induction
  {P = λ α → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩} step
  where
  step : (α : S)

关键一步揭示 x ∈ Lset α 的含义：由 Lset-out，x 仅仅 (merely) 属于某个 β ∈ α 之上的可定义子集层。层中的成员关系同样是截断的，但结论 rank x ∈ α 是命题，故 PT.rec 可以消去截断，并把纤维 β、β∈α、x∈𝒟ₒLβ 当作已经给出而加以使用。

       → (∀ β → β ∈ᵗ α → IsOrd β → (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ rank x ∈ˢ β ⟩)
       → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
  step α IH ordα x x∈Lα = PT.rec (snd (rank x ∈ˢ α)) fromStage (Lset-out α x x∈Lα)
    where
    fromStage : Σ[ β ∈ S ] (⟨ β ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩) → ⟨ rank x ∈ˢ α ⟩

在纤维内部，运行归纳假设所需的一切都被恢复。序数 α 的成员 β 经 mem-ord 本身就是序数，正是这一点让归纳假设得以在 β 处启用。

    fromStage (β , β∈α , x∈𝒟ₒLβ) = rankx∈α
      where
      ordβ : IsOrd β
      ordβ = mem-ord {A = α} ordα β β∈α
      x⊆Lβ : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ Lset β ⟩

x 在 Lset β 上的可定义性意味着 x 是它的子集：𝒟ₒ-inv 拆开证书，DefOf.Def∋⊆A 把它变成包含关系 x ⊆ Lset β。与归纳假设结合，x 的每个成员 y 的秩都在 β 中。随后 rank-upper 在恰有这些成员秩上界的前提下，把 rank x 本身包含进 β。

      x⊆Lβ = DefOf.Def∋⊆A (Lset β) x (𝒟ₒ-inv (Lset β) x x∈𝒟ₒLβ)
      ry∈β : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ rank y ∈ˢ β ⟩
      ry∈β y y∈x = IH β β∈α ordβ y (x⊆Lβ y y∈x)

      rankx⊆β : (z : S) → ⟨ z ∈ˢ rank x ⟩ → ⟨ z ∈ˢ β ⟩
      rankx⊆β = rank-upper x β ordβ ry∈β

剩下的是把 rank x ∈ sucV β 提升为 rank x ∈ α。rank x 与 β 都是序数，前者由 rank-ord 保证，于是第一节建立的 ⊆→∈suc 施于二者的包含关系，把 rank x 放进 β 的后继。随后 ∈sucV-elim 与已知的 β ∈ α 比较：若 rank x 是 β 的成员，α 的传递性把隶属再推一步；若 rank x 等于 β，路径直接传递 β ∈ α。无论哪种情形，秩都落入 α，归纳完成。

      rankx∈α : ⟨ rank x ∈ˢ α ⟩
      rankx∈α = ∈sucV-elim {A = β} {x = rank x} (snd (rank x ∈ˢ α))
        (⊆→∈suc (rank x) β (rank-ord x) ordβ rankx⊆β)
        (λ rx∈β → ordα .fst rx∈β β∈α)
        (λ rx≡β → subst (λ w → ⟨ w ∈ˢ α ⟩) (sym rx≡β) β∈α)

对序数，结论更简单，因为秩完全确定它：Lset α 中的序数是 α 的成员。这就是本章刻画中以下界形式呈现的可用版本。

这一步是一次传递：rank-fix x ordx 给出路径 rank x ≡ x，沿它替换即把秩上界 rank x ∈ α 转化为隶属 x ∈ α。注意方向，这正是上述归纳所保证的：在层中的现身强制对索引的隶属，而非相反。

ord∈Lset→∈ : (α : S) → IsOrd α → (x : S) → IsOrd x → ⟨ x ∈ˢ Lset α ⟩
           → ⟨ x ∈ˢ α ⟩
ord∈Lset→∈ α ordα x ordx x∈Lα =
  subst (λ w → ⟨ w ∈ˢ α ⟩) (rank-fix x ordx) (rank-Lset α ordα x x∈Lα)

用有界量词表达序数性质

一个集合是传递的，且其每个成员也都是传递的，这一性质可以用有界量词表达。因此，该公式在传递层与外围宇宙之间绝对地识别序数。

这个谓词由两条子句构成，两条都已有界：集合传递，指其成员的成员也都是其成员；成员皆传递，指同一条性质在低一层成立。没有无界量词出现，故公式是 Δ₀；也没有常元出现，从而免去了一整套常元改名操作。

索引采用 de Bruijn：每个有界量词约束一个新的变元 0，并把先前已有的变元向外推移一位，故两层约束之后，候选序数位于索引 2。

第一条子句说的是传递性。其有界量词 ∀̇∈ 在外一层所约束值的成员上取遍；按 de Bruijn 索引来读，第一层约束后成员位于索引 0、候选序数位于索引 1，而第二层约束内的原子公式要求 y ∈ x，y 在 0，x 被推到 2。公式对常元字母表 K 多态但不使用任何常元，故同一语法可服务于任何解释。

φ-ord : ∀ {ℓk} {K : Type ℓk} → Formula K 1
φ-ord =
  (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
  ∧̇
  (∀̇∈ (var zero)

第二条子句多叠一层量词：候选序数的成员 x、x 的成员 y、y 的成员 z 必须落回候选序数，这正说明候选序数的每个成员都是传递的。三层约束之后，最内层变元在索引 0，候选序数在索引 3。证书 φ-ord-Δ₀ 由同样的三种基本证书拼成，原子隶属的 δ-∈、有界量词的 δ-∀∈ 与合取的 δ-∧，一步对一步地映照公式的构造。

    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))

φ-ord-Δ₀ : ∀ {ℓk} {K : Type ℓk} → Δ₀ (φ-ord {K = K})
φ-ord-Δ₀ = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))

一层中的序数

用有界序数公式作分离，恰好收集属于某一层的全部序数。其成员规格在内部与外围宇宙中都可使用。

固定一层。利用传递层上的有界绝对性，公式在环境层级中的满足恰好展开成序数谓词的两条子句，故二者只需重排参数即可互换。于是它作分离所得的可定义子集就是 α 自身：其成员是该层的序数，故经秩那一半是 α 的成员；而 α 的成员是已经现身过的序数，经累积引理，它们满足该公式。

累积引理需要 α 的每个成员都在自身的后继层现身。这恰是本定理的结论本身，故在此把它作为假设引入，而下面的归纳正是给出这一假设的论证。

固定序数 α 及其证书。层 A = Lset α 是一层，layer-trans 把它升级为集合 A 的传递性，这是 Δ₀ 公式在 A 的内部满足与外围宇宙之间保持绝对的唯一前提。L.Definability 那章的可定义性机制相对于 A 打开，故下文的 defSet φ 总指 φ 从 A 中定出的子集。

module OrdAt (α : S) (ordα : IsOrd α) where
  private
    A = Lset α
    Atrans = layer-trans (Lset-layer α)
    module DefA = DefOf A

A 的成员通过纤维 ⟪ A ⟫ 自我呈现：指标 m 命名 A 中的元素 ⟪ A ⟫↪ m。公式 φ 是 φ-ord 在载体 ⟪ A ⟫ 上的实例，它有一个自由变元槽，由环境 ⟪ A ⟫↪ m ∷ [] 占据。由于 φ 不含常元，mapFo DefA.ι φ 只是经常元解释 ι 改名，就这条公式而言在语法上没有改变任何东西。此处的满足号 ⊨ᵛ 是绝对性细化所给的、外围层面的满足。

    module RefA = DefA.Refine Atrans
    open RefA.Abs using ( _⊨ᵛ_ )

    φ : Formula ⟪ A ⟫ 1
    φ = φ-ord {K = ⟪ A ⟫}

  ⊨ᵛ→ord : (m : ⟪ A ⟫) → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩

第一个方向把满足关系读成序数谓词。合取的满足是一个有序对，其第一个分量恰是第一条有界子句施于 x = B (所呈现的元素) 的结果：凡 y ∈ x 且 x ∈ B 者，都落回 B。这正是 B 的传递性条件，故该对的第一个投影就是 B 传递的证书。

         → IsOrd (⟪ A ⟫↪ m)
  ⊨ᵛ→ord m sat = transB , memTransB
    where
    B = ⟪ A ⟫↪ m
    transB : isTransV B

第二个分量是第二条子句，量词更深一层嵌套：对 x ∈ B、y ∈ x、z ∈ y，元素 z 落回 B。这恰好说明 B 的每个成员 x 自身都是传递的，于是连同第一个投影，满足数据恰是 B 的 IsOrd 证书。

    transB {x} {y} y∈x x∈B = sat .fst x x∈B y y∈x
    memTransB : (x : S) → ⟨ x ∈ˢ B ⟩ → isTransV x
    memTransB x x∈B {y} {z} z∈y y∈x = sat .snd x x∈B y y∈x z z∈y

  ord→⊨ᵛ : (m : ⟪ A ⟫) → IsOrd (⟪ A ⟫↪ m)
         → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩

逆方向由序数证书组装出一个满足。其第一个分量须接受 x ∈ B 与 y ∈ x 并返回 y ∈ B，而 IsOrd 有序对的第一个分量，即 B 的传递性，恰以正确的参数顺序完成此事。

  ord→⊨ᵛ m ord = c1 , c2
    where
    B = ⟪ A ⟫↪ m
    c1 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ B ⟩
    c1 x x∈B y y∈x = ord .fst y∈x x∈B

第二个分量须把三个隶属串回 B，而 IsOrd 有序对的第二条子句正是这个串联条件。于是 φ 的满足与序数谓词在两个方向都可互换；二者表达同一数学条件。有了这一等价，主要陈述成形：φ 所选出的可定义子集等于 α，由 extensionality 经两个包含证明，并陈述于显式假设 α⊆A 之下，即 α 的每个成员已在 A 中现身。

    c2 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩
       → (z : S) → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩
    c2 x x∈B y y∈x z z∈y = ord .snd x x∈B z∈y y∈x

  defSet-φ-ord : ((β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ A ⟩) → DefA.defSet φ ≡ α
  defSet-φ-ord α⊆A = extensionality (DefA.defSet φ) α (sub₁ , sub₂)

从可定义子集到 α 的包含，是本章秩那一半发挥作用的所在。可定义子集中的隶属经 ∈∈ₛ 展开为呈现层面的事实，故 sub₁ 取一个 y 及「y 属于 defSet φ」的证明，须产出 y ∈ α。

    where
    sub₁ : ⟨ DefA.defSet φ ⊆ α ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = α} .fst
      (y∈α (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ))
      where

这里叠加了三次转换。y 属于可定义子集，由 defSet⊆A 得出 y 属于 A，因为子集包含于层。随后，选定的呈现通过 ∈-asFiber 把这个隶属证明变成指标 m 与路径 q；该路径把 y 与 m 所指名的元素等同起来。

      y∈α : ⟨ y ∈ˢ DefA.defSet φ ⟩ → ⟨ y ∈ˢ α ⟩
      y∈α y∈def = ord∈Lset→∈ α ordα y ordy y∈A
        where
        y∈A = DefA.defSet⊆A φ y y∈def
        fib = ∈-asFiber {a = y} {b = A} y∈A

路径 q 把 y 的隶属传递为所呈现元素 ⟪ A ⟫↪ m 的隶属。由于 φ 是 Δ₀ 且 A 传递，abs-defSet 等同了「该元素属于 defSet φ」与「mapFo ι φ 在单元环境处外围满足」这两个 hProp。沿这些路径替换便得到所需的 sat；路径传递本身不要求目标具有命题性。

        m = fib .fst
        q = fib .snd
        sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
        sat = subst ⟨_⟩ (RefA.abs-defSet φ φ-ord-Δ₀ m)
                (subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) (sym q) y∈def)

由 sat，蕴涵 ⊨ᵛ→ord 返回所呈现元素的 IsOrd 证书，沿 q 传递后便得到 y 自身的证书。随后 ord∈Lset→∈，即秩那一半，把 y 放进 α。于是可定义子集的任意成员都是该层的序数，而层索引包含它。

        ordy : IsOrd y
        ordy = subst IsOrd q (⊨ᵛ→ord m sat)

    sub₂ : ⟨ α ⊆ DefA.defSet φ ⟩
    sub₂ y y∈ₛ = ∈∈ₛ {a = y} {b = DefA.defSet φ} .fst
      (y∈def (∈∈ₛ {a = y} {b = α} .snd y∈ₛ))

反向包含把同一回路倒着走。α 的成员 y 到手时已带着序数证书，由 mem-ord 给出。假设 α⊆A 经纤维 m、q 把 y 呈现在层内，ord→⊨ᵛ 便给出 φ 在该环境处的外围满足。

      where
      y∈def : ⟨ y ∈ˢ α ⟩ → ⟨ y ∈ˢ DefA.defSet φ ⟩
      y∈def y∈α = subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) q
        (subst ⟨_⟩ (sym (RefA.abs-defSet φ φ-ord-Δ₀ m)) sat)
        where

绝对性现在朝另一方向换算：Δ₀ 公式的外围满足等于 ⟪ A ⟫↪ m 属于 defSet φ，沿 q 传递便把隶属落在 y 自身，即可定义子集之内。全程未做任何选择：每个纤维 m、q 都只在产生它的那个 y 上局部使用。

        ordy = mem-ord {A = α} ordα y y∈α
        y∈A = α⊆A y y∈α
        fib = ∈-asFiber {a = y} {b = A} y∈A
        m = fib .fst
        q = fib .snd

两个包含合拢，defSet-φ-ord 陈述结论：有界公式从 Lset α 中切出的子集恰是 α。至此一切都以 α⊆A 为条件；下一节将移除这个条件，本章的主定理随之就位。

        sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
        sat = ord→⊨ᵛ m (subst IsOrd (sym q) ordy)

序数现身于其后继

每个序数都是自身的可定义子集，由有界序数公式选出。因此 α 属于 Lset α 的可定义幂集，也就是后继层。

剩下的缺口正是上一节不得不假设的包含关系 α ⊆ Lset α。它由对隶属关系的归纳填补：归纳假设陈述的是定理对 α 的每个成员 β 的情形，于是 β 出现在 Lset (sucV β) 中，再经第一节的累积引理被提升到 Lset α 中。一旦所有成员都累积进来，公式便从 Lset α 中分离出 α，而下一层定义中的并包含这一项。这里没有循环：归纳假设关心的是成员，而非 α 自身。

归纳之前先打包两个小事实。其一是从可定义幂集到层的单向桥：一个说明 α 属于 𝒟ₒ (Lset α) 的证书，即 α 是 Lset α 的可定义子集，与 self∈sucV α (它说 α 属于自身的后继) 合在一起，恰是 Lset-in 所需的全部数据。第二行开始定理本身，直接应用对隶属关系的归纳原理：被归纳证明的陈述就是定理本身，相对化到每个序数上。

private
  𝒟ₒ→Lset-suc : (α : S) → ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩ → ⟨ α ∈ˢ Lset (sucV α) ⟩
  𝒟ₒ→Lset-suc α α∈𝒟ₒ = Lset-in (sucV α) α α (self∈sucV α) α∈𝒟ₒ

ord∈Lset-suc : (α : S) → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
ord∈Lset-suc = ∈-induction

归纳步对 α 的每个成员 β 收到定理在 β 处的结论，并须给出在 α 处的结论。由于上一节已把目标化归为唯一的假设 α ⊆ Lset α，这一步要做的只是组装这个包含关系，并把结果交给桥引理。除了 α 是序数与归纳假设之外，别无所用。

  {P = λ α → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩} step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → IsOrd β → ⟨ β ∈ˢ Lset (sucV β) ⟩)
       → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
  step α IH ordα = 𝒟ₒ→Lset-suc α α∈𝒟ₒ

包含关系逐个成员地组装。对 α 中的每个 β，作为序数 α 的成员使 β 自己也是序数，归纳假设把它放进 Lset (sucV β)；而第一节的累积引理，正是为其后继或落入 α、或与之相等这两种情形而设，随即把它提升到 Lset α。前面那两个比较引理在此兑现：一次分情形就同时覆盖了所有成员。

    where
    α⊆A : (β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset α ⟩
    α⊆A β β∈α = Lset-cumul β α ordβ ordα β∈α (IH β β∈α ordβ)
      where
      ordβ = mem-ord {A = α} ordα β β∈α

有了 α ⊆ Lset α，上一节的结论原样适用：由 φ-ord 从 Lset α 中选出的可定义子集正是 α 自身。证书以截断的方式仅仅给出，因为 𝒟ₒ 的成员只需要某个定义公式及一致性证明，而 φ-ord 与 OrdAt 中的外延性论证组成的对恰是这样的见证。桥引理随后把 α 移入 Lset (sucV α)，归纳与定理同时完成。

    α∈𝒟ₒ : ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩
    α∈𝒟ₒ = 𝒟ₒ-intro (Lset α) α
      ∣ φ-ord {K = ⟪ Lset α ⟫} , OrdAt.defSet-φ-ord α ordα α⊆A ∣₁

小结

序数现在具有准确的层界：α 出现在 Lset (sucV α) 中，而若它出现在 Lset β 中，则必有 α ∈ β。有界序数公式使后续内部论证能够使用这些事实。

ord∈Lset-suc 说序数现身在自身之后的那一层中，ord∈Lset→∈ 说它不会更早现身。二者合起来，Lset α 中的序数恰是 α 的成员。经由第一节那两次比较，本章是经典的，而它用到的其余一切都是构造性的。模块 L.Stage 将这一结果应用于 ω，从而完成无穷公理的证明。