---
title: "GCH 论证所需的充分层"
module: L.GCH.AdequateStages
lang: zh
site: "Bedrock"
description: "GCH 论证所需的充分层"
stage: "证明 GCH"
reading_order: 102
canonical: https://bedrock.institute/zh/L.GCH.AdequateStages.html
html: L.GCH.AdequateStages.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/AdequateStages.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Stage, L.Hierarchy, L.Axioms.Basic, L.Coding.CodeSet, L.Definability, L.Coding.EnvironmentTower, L.Coding.SatisfactionGraphSet]
routes: [gch-descriptions]
translations: [https://bedrock.institute/en/L.GCH.AdequateStages.md, https://bedrock.institute/ja/L.GCH.AdequateStages.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# GCH 论证所需的充分层

凝聚所用的内部描述要求四个见证集合同时出现。本章定义序数指标何时充分，在任意给定序数之上构造这样的指标 `γ`，再构造指标 `λ`，使它的每个成员都在某个更小的充分指标中得到局部覆盖。相应的可构造层分别是 `Lset γ` 与 `Lset λ`。充分层是本书为 GCH 论证所需四项闭合条件所定的术语，并非通常所谓容许序数。

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

本章的全部构造都相对于一个显式的排中律实例。它通过诞生层和编码见证的构造进入论证，却不提供选择函数。特别地，后文从属于并集所得的存在性仍带有命题截断。

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

固定宇宙层级 `ℓ`，并假设层级 `ℓ-suc ℓ` 上命题的排中律。下文构造的充分指标及其对应的层都依赖这一个经典假设。

```agda
module L.GCH.AdequateStages {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

这一构造在外围累积层级 `V ℓ` 中进行。其中的对象 `c`、`γ` 以及后文的 `λ` 是序数指标，而 `Lset c`、`Lset γ` 与 `Lset λ` 才是由它们索引的可构造层。并集是在外围层级的序数指标之间形成的；恒真公式只在最后用于证明整个可构造层属于其后继层。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( ⊤̇ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( union-family-in; union-family-out )
open import L.Constructible {ℓ} using
```

要把一个可构造见证放入更后的层，先取它的诞生层索引，再约束这个序数指标，最后使用 `Lset` 的单调性。另一些序数事实保证序数的成员、这些成员的后继以及途中使用的公共界仍是序数。因此，取界论证作用于指标，而其结论则把见证集合放进一层之内。

```agda
  ( 𝒮ʟ; isL; IsOrd; isPropIsOrd; Lset; Lset-mono; Lset→isL; 𝒟ₒ-intro )
open import L.Ordinal {ℓ} using ( boundingOrd; bound2; setUnion-ord; mem-ord; suc-ord; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Hierarchy {ℓ} lem using ( hierL )
```

对固定的序数指标 `c`，后续的层级描述需要与 `Lset c` 相关的四个可构造集合：内部层级表、全体公式码之集、统一满足关系的图，以及环境塔。充分性把这四个集合一同放进同一个更后的可构造层，使一条有界描述能够在那里遍历它们。

```agda
open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
```

隶属断言以及由它们组成的见证条件都是命题。这一点在处理并集元素时至关重要：从并集隶属只能命题截断地知道该元素落在哪个族成员中；这些信息可以消去到一个命题中，却不能借此选定并保留某个特定指标。

```agda
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; sett )
```

累积层级中的每个集合都有一个小呈现：一个小索引类型映到它的全部元素。借助这个呈现，下一步取界可以遍历一个序数的所有成员。反过来，从属于集合族之并只能在命题截断下得到族的索引；这一差别是下文可数链论证的关键。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⋃_; module InfinitySet )
open InfinitySet {ℓ} using ( sucV; ω )
```

我们通过见证命题 `⟨ x ∈ y ⟩` 读取外围隶属 `x ∈ y`。这是 `V ℓ` 中的隶属，不应与下一步引入的可构造载体内部隶属混同。

```agda
open hPropStructure 𝒮ᵥ
```

可构造载体 `CS.S` 的一个元素把外围集合与其可构造性证据打包在一起。因此，下文的四个见证先构造成 `CS.S` 的元素；它们的第一投影才是需要证明属于某个更后 `Lset` 的实际外围集合。

```agda
module CS = hPropStructure 𝒮ʟ using (S)
```

## 充分层所容纳的四个见证

见证模块固定一个序数 `c` 连同它是序数的证明。

```agda
module At (c : V ℓ) (oc : IsOrd c) where
```

可构造层 `Lset c` 被打包为载体 `A`。随后以这个载体为基础，分别构造层级表、公式码集合、满足关系图与环境塔这四个见证。

```agda
  A : CS.S
  A = LsetS c oc
```

序数指标 `c` 自身也是可构造的：`ord∈Lset-suc` 把它放入 `Lset (sucV c)`，而属于一个由序数索引的可构造层便给出所需的可构造性证据 `cL`。

```agda
  cL : ⟨ isL c ⟩
  cL = Lset→isL (sucV c) (suc-ord oc) c (ord∈Lset-suc c oc)
```

第一个见证是 `c` 处的内部层级表。它在 `L` 内部记录序数指标位于 `c` 以下的各个可构造层。

```agda
  hier : CS.S
  hier = hierL c cL oc
```

第二个见证是层载体上全体公式码之集。这些码将在后续的层级描述中使用。

```agda
  codes : CS.S
  codes = AllCodes A
```

统一满足表的有序对图是第三个见证：它记录每个键被赋予的值。

```agda
  table : CS.S
  table = SatGraph.pairs A
```

环境塔是第四个见证：它收集每个有限长度的环境。

```agda
  tower : CS.S
  tower = Tower.tower A
```

对一个序数层索引 `c`，见证谓词要求刚构造的四个底层集合都属于同一个公共容器 `K`。它量化证明 `oc : IsOrd c`，因而不会保留某一份偏好的序数性证明。后文将令 `K` 为 `Lset γ`，其中 `γ` 是更大的序数指标。

```agda
Witnesses : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Witnesses K c = (oc : IsOrd c)
  → ⟨ fst (At.hier c oc) ∈ K ⟩
  × ⟨ fst (At.codes c oc) ∈ K ⟩
  × ⟨ fst (At.table c oc) ∈ K ⟩
```

第四个隶属补全见证谓词：环境塔也属于同一容器。

```agda
  × ⟨ fst (At.tower c oc) ∈ K ⟩
```

见证谓词是命题。对 `c` 为序数的每份可能证明，其结论都是四个隶属命题的积；取值均为命题的依赖函数仍是命题。这一命题性使后文能够把命题截断的链索引直接消去到 `Witnesses`，而不把该索引选作数据。

```agda
isPropWitnesses : (K c : V ℓ) → isProp (Witnesses K c)
isPropWitnesses K c = isPropΠ λ oc →
  isProp× (snd (fst (At.hier c oc) ∈ K))
    (isProp× (snd (fst (At.codes c oc) ∈ K))
      (isProp× (snd (fst (At.table c oc) ∈ K)) (snd (fst (At.tower c oc) ∈ K))))
```

充分指标 `γ` 是一个序数，并满足另外三条性质：每个 `x ∈ γ` 都有 `sucV x ∈ γ`，序数 `ω` 属于 `γ`，且每个序数 `c ∈ γ` 的四个见证集合都位于同一个可构造层 `Lset γ` 内。闭合条件谈的是序数指标 `γ`，见证条件谈的则是与之不同的集合 `Lset γ`。

```agda
Adequate : V ℓ → Type (ℓ-suc ℓ)
Adequate γ =
    IsOrd γ
  × ((x : V ℓ) → ⟨ x ∈ γ ⟩ → ⟨ sucV x ∈ γ ⟩)
  × ⟨ ω ∈ γ ⟩
```

最后一条正是两种层次相接之处。前提 `c ∈ γ` 是序数指标之间的隶属事实，结论则把与 `c` 相关的四个集合放进可构造层 `Lset γ`。

```agda
  × ((c : V ℓ) → ⟨ c ∈ γ ⟩ → Witnesses (Lset γ) c)
```

四个字段为后文论证命名：序数性、后继封闭、无穷序数的隶属，以及见证子句。

```agda
module Adequate (γ : V ℓ) (ad : Adequate γ) where
  ord = ad .fst
  succ = ad .snd .fst
  ω∈ = ad .snd .snd .fst
  wit = ad .snd .snd .snd
```

## 在任意序数之上构造充分层

为了对集合 `α` 的全体成员取界，使用它的小呈现 `⟪ α ⟫`。映射 `ι α` 把每个呈现索引送到它所指名的外围集合。此处这套记号本身并不要求 `α` 是序数；序数性将在构造证明每个被指名成员都是序数时进入。

```agda
private
  ι : (α : V ℓ) → ⟪ α ⟫ → V ℓ
  ι α = ⟪ α ⟫↪
```

每个被呈现索引经由小隶属与外围隶属之间的桥，指名该序数的一个成员。

```agda
  ι∈ : (α : V ℓ) (m : ⟪ α ⟫) → ⟨ ι α m ∈ α ⟩
  ι∈ α m = ∈∈ₛ {a = ι α m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)
```

序数的传递性被打包一次：序数内两条链式隶属坍缩为对该序数的一次隶属。

```agda
  tr : (β : V ℓ) → IsOrd β → (x y : V ℓ) → ⟨ x ∈ β ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ β ⟩
  tr β oβ x y x∈ y∈ = oβ .fst {x = x} {y = y} y∈ x∈
```

从序数指标 `α` 出发，一步取界将构造一个更大的序数指标 `β`。这一步履行由 `α` 的成员产生的全部义务：它们的后继，以及它们四个见证集合的诞生层索引。此时尚不能断言 `β` 已经充分，因为对 `β` 中新增成员的相应义务还没有履行。

```agda
module Bound1 (α : V ℓ) (oα : IsOrd α) where
```

每个打包后的可构造集合 `s : CS.S` 都有诞生层索引 `stage (fst s) (snd s)`。这个辅助表达式在 `α` 的一个被呈现成员的语境中记录该运算；所得指标取决于见证集合 `s`，而外围参数则记录这个见证是为哪个成员构造的。

```agda
  private
    W : ⟪ α ⟫ → (c : V ℓ) → IsOrd c → CS.S → V ℓ
    W m c oc s = stage (fst s) (snd s)
```

`α` 的每个被呈现成员都是序数，因为序数的成员是序数。

```agda
    oc : (m : ⟪ α ⟫) → IsOrd (ι α m)
    oc m = mem-ord {A = α} oα (ι α m) (ι∈ α m)
```

把 `st` 分别用于四类见证构造，便得到四族由序数索引的诞生层指标。下一步的公共界必须严格界住的正是这四族指标。

```agda
    st : (f : (c : V ℓ) (o : IsOrd c) → CS.S) → ⟪ α ⟫ → V ℓ
    st f m = stage (fst (f (ι α m) (oc m))) (snd (f (ι α m) (oc m)))
```

诞生层索引 `st f m` 是序数。这由诞生层构造的一般定理 `stage-ord` 得出；应用时使用见证的底层集合及其可构造性证据。

```agda
    st-ord : (f : (c : V ℓ) (o : IsOrd c) → CS.S) (m : ⟪ α ⟫) → IsOrd (st f m)
    st-ord f m = stage-ord (fst (f (ι α m) (oc m))) (snd (f (ι α m) (oc m)))
```

这里取五个严格公共界。前四个分别约束 `α` 的每个被呈现成员所对应的层级表、码集、满足图与环境塔的诞生层索引；第五个直接约束各序数后继 `sucV (ι α m)`。这些都是序数指标之间的界；第五族并不是一族诞生层。

```agda
    b1 = boundingOrd ⟪ α ⟫ (st At.hier) (st-ord At.hier)
    b2 = boundingOrd ⟪ α ⟫ (st At.codes) (st-ord At.codes)
    b3 = boundingOrd ⟪ α ⟫ (st At.table) (st-ord At.table)
    b4 = boundingOrd ⟪ α ⟫ (st At.tower) (st-ord At.tower)
    b5 = boundingOrd ⟪ α ⟫ (λ m → sucV (ι α m)) (λ m → suc-ord (oc m))
```

第六个严格界同时包含起始指标 `α` 与 `ω`。随后用二元界合并六项义务：`b7` 合并前两个见证界，`b8` 合并另外两个见证界，`b9` 合并后继界与 `α`、`ω` 的公共界，`b10` 则合并四个见证界。这里不声称所得界最小；这些运算只给出严格公共界及所需的隶属证明。

```agda
    b6 = bound2 α ω oα ω-ord
    b7 = bound2 (b1 .fst) (b2 .fst) (b1 .snd .fst) (b2 .snd .fst)
    b8 = bound2 (b3 .fst) (b4 .fst) (b3 .snd .fst) (b4 .snd .fst)
    b9 = bound2 (b5 .fst) (b6 .fst) (b5 .snd .fst) (b6 .snd .fst)
    b10 = bound2 (b7 .fst) (b8 .fst) (b7 .snd .fst) (b8 .snd .fst)
```

最后一次二元取界把两条分支合并：一条携带后继、`α` 与 `ω`，另一条携带四类诞生层之界。因此，它的第一分量同时严格界住全部六类义务。

```agda
    b11 = bound2 (b9 .fst) (b10 .fst) (b9 .snd .fst) (b10 .snd .fst)
```

最终界的第一分量是新的序数指标 `β`。它是 `V ℓ` 中的指标；容纳见证的可构造层将是 `Lset β`。

```agda
  β : V ℓ
  β = b11 .fst
```

最终界是序数，因为它由二元取界从序数构造而来。

```agda
  oβ : IsOrd β
  oβ = b11 .snd .fst
```

喂给最后一次合并的两个部分界位于最终界之下。

```agda
  private
    b9∈ : ⟨ b9 .fst ∈ β ⟩
    b9∈ = b11 .snd .snd .fst
    b10∈ : ⟨ b10 .fst ∈ β ⟩
    b10∈ = b11 .snd .snd .snd
```

因为 `β` 具有传递性，严格隶属可以沿取界树向下传播。从 `b9 ∈ β` 可分别得到后继界 `b5 ∈ β`，以及 `α` 与 `ω` 的公共界 `b6 ∈ β`；从 `b10 ∈ β` 则先得到 `b7 ∈ β`。

```agda
    b5∈ : ⟨ b5 .fst ∈ β ⟩
    b5∈ = tr β oβ (b9 .fst) (b5 .fst) b9∈ (b9 .snd .snd .fst)
    b6∈ : ⟨ b6 .fst ∈ β ⟩
    b6∈ = tr β oβ (b9 .fst) (b6 .fst) b9∈ (b9 .snd .snd .snd)
    b7∈ : ⟨ b7 .fst ∈ β ⟩
```

另一条分支给出 `b8 ∈ β`。再沿 `b7` 向下一步，第一个见证界 `b1` 也属于 `β`。重复同一传递性论证，便会把其余每个见证界都放入 `β`。

```agda
    b7∈ = tr β oβ (b10 .fst) (b7 .fst) b10∈ (b10 .snd .snd .fst)
    b8∈ : ⟨ b8 .fst ∈ β ⟩
    b8∈ = tr β oβ (b10 .fst) (b8 .fst) b10∈ (b10 .snd .snd .snd)
    b1∈ : ⟨ b1 .fst ∈ β ⟩
    b1∈ = tr β oβ (b7 .fst) (b1 .fst) b7∈ (b7 .snd .snd .fst)
```

第二、第三个见证界 `b2` 与 `b3` 分别从分支 `b7` 与 `b8` 得出。第四个见证界 `b4` 在 `b8` 下处于相同位置，所以下一行将闭合这个对称论证。

```agda
    b2∈ : ⟨ b2 .fst ∈ β ⟩
    b2∈ = tr β oβ (b7 .fst) (b2 .fst) b7∈ (b7 .snd .snd .snd)
    b3∈ : ⟨ b3 .fst ∈ β ⟩
    b3∈ = tr β oβ (b8 .fst) (b3 .fst) b8∈ (b8 .snd .snd .fst)
    b4∈ : ⟨ b4 .fst ∈ β ⟩
```

沿见证分支的最后一次下降给出 `b4 ∈ β`。至此，四个诞生层之界都已与公共序数指标 `β` 建立严格隶属关系。

```agda
    b4∈ = tr β oβ (b8 .fst) (b4 .fst) b8∈ (b8 .snd .snd .snd)
```

经过 `b6` 的分支还保留起始序数指标：由 `α ∈ b6` 与 `b6 ∈ β`，传递性给出 `α ∈ β`。

```agda
  α∈β : ⟨ α ∈ β ⟩
  α∈β = tr β oβ (b6 .fst) α b6∈ (b6 .snd .snd .fst)
```

同一分支也保留 `ω`：先有 `ω ∈ b6`，再接上 `b6 ∈ β`，便得到后文所需的 `ω ∈ β`。

```agda
  ω∈β : ⟨ ω ∈ β ⟩
  ω∈β = tr β oβ (b6 .fst) ω b6∈ (b6 .snd .snd .snd)
```

若 `x ∈ α`，呈现纤维便给出索引 `m` 及等式 `ι α m ≡ x`。第五个公共界包含 `sucV (ι α m)`，再经 `b5 ∈ β` 得到它属于 `β`；最后沿纤维等式作替换，便有 `sucV x ∈ β`。因此，这一步只对 `α` 的成员证明后继闭合，恰好符合一步取界的任务。

```agda
  suc∈β : (x : V ℓ) → ⟨ x ∈ α ⟩ → ⟨ sucV x ∈ β ⟩
  suc∈β x x∈ = subst (λ u → ⟨ sucV u ∈ β ⟩) (fib .snd)
    (tr β oβ (b5 .fst) (sucV (ι α (fib .fst))) b5∈ (b5 .snd .snd (fib .fst)))
    where
    fib : Σ[ m ∈ ⟪ α ⟫ ] (ι α m ≡ x)
```

`∈-asFiber` 从外围隶属证明恢复这个纤维。这里的结论是一个实际的依值对，而不只是命题截断的存在：小呈现使用嵌入，所以识别 `x` 的呈现索引之纤维取值于命题。

```agda
    fib = ∈-asFiber {a = x} {b = α} x∈
```

公共序数界 `β` 已经严格界住四类见证的出生层指标。现在要利用这些界，把见证本身放入可构造层 `Lset β`。

```agda
  private
```

固定四类见证构造之一 `f`，并取一个呈现 `α` 的成员的索引 `m`。相应见证出生于 `Lset (st f m)`；记录的界 `b.fst` 严格包含这个出生指标，而最终界 `β` 又严格包含 `b.fst`。安放引理把由此得到的 `Lset β` 中的隶属关系封装起来。

```agda
    land : (f : (c : V ℓ) (o : IsOrd c) → CS.S)
           (b : Σ[ σ ∈ V ℓ ] (IsOrd σ × ((m : ⟪ α ⟫) → ⟨ st f m ∈ σ ⟩)))
         → ⟨ b .fst ∈ β ⟩
         → (m : ⟪ α ⟫) → ⟨ fst (f (ι α m) (oc m)) ∈ Lset β ⟩
    land f b b∈ m =
```

内层的 `Lset-mono` 把见证从 `Lset (st f m)` 搬到 `Lset (b.fst)`，外层的应用再把它搬到 `Lset β`。两步分别依据相应序数指标之间的严格隶属关系。

```agda
      Lset-mono {α = β} {β = b .fst} b∈
        (Lset-mono {α = b .fst} {β = st f m} (b .snd .snd m)
          (stage-mem (fst (f (ι α m) (oc m))) (snd (f (ι α m) (oc m)))))
```

对由 `m` 呈现的成员，证明先把层级表与公式码集合放入 `Lset β`。调用者可以给出任意证明 `o : IsOrd (ι α m)`；由于序数性是命题，它可与构造见证时使用的证明 `oc m` 认同。

```agda
    witAt : (m : ⟪ α ⟫) → Witnesses (Lset β) (ι α m)
    witAt m o =
        subst (λ u → ⟨ fst (At.hier (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
          (land At.hier b1 b1∈ m)
      , ( subst (λ u → ⟨ fst (At.codes (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
```

同一论证完成码集合的隶属证明，并把满足关系图与环境塔放入 `Lset β`。于是得到 `Witnesses (Lset β) (ι α m)` 的全部四个分量，而且结果不依赖某一份特定的序数性证明。

```agda
            (land At.codes b2 b2∈ m)
        , ( subst (λ u → ⟨ fst (At.table (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
              (land At.table b3 b3∈ m)
          , subst (λ u → ⟨ fst (At.tower (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
              (land At.tower b4 b4∈ m) ))
```

一份成员证明 `c ∈ α` 带有实际的呈现纤维：它给出索引 `m` 以及等式 `ι α m ≡ c`。沿该等式搬运 `witAt m`，便得到抽象指定的成员 `c` 的四个见证；这一步既不消去命题截断，也不作选择。

```agda
  wit : (c : V ℓ) → ⟨ c ∈ α ⟩ → Witnesses (Lset β) c
  wit c c∈ = subst (Witnesses (Lset β)) (fib .snd) (witAt (fib .fst))
    where
    fib : Σ[ m ∈ ⟪ α ⟫ ] (ι α m ≡ c)
    fib = ∈-asFiber {a = c} {b = α} c∈
```

并构造从任意自然数索引的序数族 `ch` 开始。取并本身不要求该族单调；后面的两次应用会另行证明每一项属于其后继项。

```agda
module Union (ch : ℕ → V ℓ) (och : (n : ℕ) → IsOrd (ch n)) where
```

累积层级中的并要求索引小类型位于外围宇宙层级。用 `Lift ℕ` 代替 `ℕ` 只改变其宇宙位置：`F (lift n)` 仍是序数 `ch n`。

```agda
  private
    F : Lift {ℓ-zero} {ℓ} ℕ → V ℓ
    F n = ch (lower n)
```

这个序数族的集合论并记为序数指标 `γ`。此时 `γ` 是外围累积层级中的集合；与它对应的可构造层是 `Lset γ`。

```agda
  γ : V ℓ
  γ = ⋃ (sett (Lift {ℓ-zero} {ℓ} ℕ) F)
```

任意序数族的集合论并仍是序数。把这一事实用于 `F` 便得到 `IsOrd γ`；这里没有使用自然数索引的次序性质或共尾性质。

```agda
  oγ : IsOrd γ
  oγ = setUnion-ord (Lift {ℓ-zero} {ℓ} ℕ) F (λ n → och (lower n))
```

向内读式把链中每一项的每个成员都纳入并。

```agda
  into : (n : ℕ) (x : V ℓ) → ⟨ x ∈ ch n ⟩ → ⟨ x ∈ γ ⟩
  into n x = union-family-in (Lift {ℓ-zero} {ℓ} ℕ) F (lift n) x
```

向外读法在截断下恢复包含并中任一给定成员的链项。截断索引仅被消耗到命题。

```agda
  outof : (x : V ℓ) → ⟨ x ∈ γ ⟩ → ∥ Σ[ n ∈ ℕ ] ⟨ x ∈ ch n ⟩ ∥₁
  outof x h = PT.map (λ { (n , hn) → lower n , hn })
    (union-family-out (Lift {ℓ-zero} {ℓ} ℕ) F x h)
```

一步取界只履行前一个序数所产生的义务。为了履行构造途中出现的每一项义务，先取一个严格包含 `p` 与 `ω` 的起点，沿自然数序列反复应用 `Bound1`，再对所得序数指标取并。

```agda
module Above (p : V ℓ) (op : IsOrd p) where
```

初始界是一个同时严格包含起始序数 `p` 与序数 `ω` 的序数。这直接给出随后要保留到最终并中的两条隶属关系。

```agda
  private
    base = bound2 p ω op ω-ord
```

第零个序数是初始公共界。此后每个序数都对前一项应用 `Bound1`，因此由 `ch n` 的成员产生的义务会在 `ch (suc n)` 中得到满足；这里并未声称单独一步已对其自身所有成员充分。

```agda
  ch : ℕ → Σ[ β ∈ V ℓ ] IsOrd β
  ch zero = base .fst , base .snd .fst
  ch (suc n) = Bound1.β (ch n .fst) (ch n .snd) , Bound1.oβ (ch n .fst) (ch n .snd)
```

现在把前面的并构造应用于这些序数指标。其向内映射把已知成员关系送入并，其向外映射则只能在命题截断下定位包含任意给定成员的某一项。

```agda
  module C = Union (λ n → ch n .fst) (λ n → ch n .snd) using (into; outof; oγ; γ)
```

令 `γ` 为这些序数指标之并。取并吸收了一步延迟：任何在某一项中出现的成员，其后继与四个见证都会由后续项处理。最终，见证必须属于 `Lset γ`，而不是属于指标 `γ` 本身。

```agda
  γ : V ℓ
  γ = C.γ
```

由于每个 `ch n` 都是序数，它们的集合论并 `γ` 也是序数。这里仅得到 `IsOrd γ`；`Adequate γ` 的闭包字段与见证字段将在下文分别证明。

```agda
  oγ : IsOrd γ
  oγ = C.oγ
```

链的每项严格低于其后继项，由一步取界的隶属子句而来。

```agda
  private
    up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
    up n = Bound1.α∈β (ch n .fst) (ch n .snd)
```

要把序数指标 `ch n` 本身放入并 `γ`，先用它严格属于 `ch (suc n)`，再把 `ch (suc n)` 的每个成员纳入并。这个事实稍后提供应用 `Lset` 单调性所需的指标比较。

```agda
    ch∈γ : (n : ℕ) → ⟨ ch n .fst ∈ γ ⟩
    ch∈γ n = C.into (suc n) (ch n .fst) (up n)
```

基础界已经包含 `p`。它是该序列的第零项，所以并的向内映射保留这条隶属关系，得到 `p ∈ γ`。

```agda
  p∈γ : ⟨ p ∈ γ ⟩
  p∈γ = C.into zero p (base .snd .snd .fst)
```

同一个向内映射把 `ω ∈ ch 0` 送为 `ω ∈ γ`。这给出 `Adequate γ` 所要求的那项具体隶属事实。

```agda
  ω∈γ : ⟨ ω ∈ γ ⟩
  ω∈γ = C.into zero ω (base .snd .snd .snd)
```

给定 `x ∈ γ`，向外映射只给出命题截断的存在性：某个指标 `n` 满足 `x ∈ ch n`。在截断内的每个分支中，下一次 `Bound1` 把 `sucV x` 放入 `ch (suc n)`，继而放入 `γ`。目标成员关系 `sucV x ∈ γ` 是命题，所以这些分支可以重新合并；没有任何特定的 `n` 逸出命题截断。

```agda
  succ : (x : V ℓ) → ⟨ x ∈ γ ⟩ → ⟨ sucV x ∈ γ ⟩
  succ x x∈ = PT.rec (snd (sucV x ∈ γ))
    (λ { (n , x∈n) → C.into (suc n) (sucV x) (Bound1.suc∈β (ch n .fst) (ch n .snd) x x∈n) })
    (C.outof x x∈)
```

对 `c ∈ γ`，向外映射同样只给出命题截断的存在性：某个 `n` 满足 `c ∈ ch n`。在每个分支中，一步取界在 `Lset (ch (suc n))` 中提供四个见证，而 `ch (suc n) ∈ γ` 使 `Lset-mono` 能把它们搬入 `Lset γ`。由于 `Witnesses (Lset γ) c` 是命题，可以把所得结果从命题截断中消去。

```agda
  wit : (c : V ℓ) → ⟨ c ∈ γ ⟩ → Witnesses (Lset γ) c
  wit c c∈ = PT.rec (isPropWitnesses (Lset γ) c)
    (λ { (n , c∈n) → λ oc →
      let w = Bound1.wit (ch n .fst) (ch n .snd) c c∈n oc
          mono = Lset-mono {α = γ} {β = ch (suc n) .fst} (ch∈γ (suc n))
```

映射 `mono` 表示可构造层级从指标 `ch (suc n)` 到指标 `γ` 的单调性。分别把它用于层级表、码集合、满足关系图与环境塔，便完成四分量的见证元组。

```agda
      in mono (w .fst) , ( mono (w .snd .fst) , ( mono (w .snd .snd .fst) , mono (w .snd .snd .snd) )) })
    (C.outof c c∈)
```

序数指标 `γ` 现在满足 `Adequate` 的全部四条：它是序数，对后继封闭，包含 `ω`，并把每个 `c ∈ γ` 的四个见证放入与指标有别的可构造层 `Lset γ`。后文所用的充分性，其全部内容正是这四条。

```agda
  adequate : Adequate γ
  adequate = oγ , ( succ , ( ω∈γ , wit ))
```

该定理显式返回序数指标 `γ`，并附带 `p ∈ γ` 与 `Adequate γ`。外层依值对没有截断，所以后续论证可以指称这个 `γ`；构造既不证明它最小，也不证明它由 `p + ω` 之类的标准序数运算得到。

```agda
adequate-above : (p : V ℓ) → IsOrd p
               → Σ[ γ ∈ V ℓ ] (IsOrd γ × ⟨ p ∈ γ ⟩ × Adequate γ)
adequate-above p op = Above.γ p op , ( Above.oγ p op , ( Above.p∈γ p op , Above.adequate p op ))
```

## 在整个层中强化充分性

`Superadequate λ` 表示：对每个 `d ∈ λ`，仅仅存在充分序数指标 `γ`，满足 `γ ∈ λ` 且 `d ∈ γ`。因此 `γ` 严格位于序数 `λ` 之下并覆盖 `d`，但命题截断既不保留选定的 `γ`，也不保留最小的 `γ`。

```agda
Superadequate : V ℓ → Type (ℓ-suc ℓ)
Superadequate lam = (d : V ℓ) → ⟨ d ∈ lam ⟩
  → ∥ Σ[ γ ∈ V ℓ ] (⟨ γ ∈ lam ⟩ × ⟨ d ∈ γ ⟩ × Adequate γ) ∥₁
```

为在序数 `α` 之上构造这样的超充分层，再次迭代 `adequate-above`。这一次，自然数序列的每一项已经是充分序数指标，因而这些项本身稍后可充当局部充分见证。

```agda
module Super (α : V ℓ) (oα : IsOrd α) where
```

第零项是 `adequate-above α oα` 显式返回的序数指标。它是充分的，并严格包含起始序数 `α`；这两项事实随该项保存，供后文使用。

```agda
  ch : ℕ → Σ[ γ ∈ V ℓ ] (IsOrd γ × Adequate γ)
  ch zero =
    adequate-above α oα .fst
    , ( adequate-above α oα .snd .fst , adequate-above α oα .snd .snd .snd )
  ch (suc n) =
```

从充分序数指标 `ch n` 出发，再次应用 `adequate-above` 得到下一充分指标 `ch (suc n)`，并有 `ch n ∈ ch (suc n)`。该定理显式提供某个这样的下一指标，但不声称其最小。

```agda
    adequate-above (ch n .fst) (ch n .snd .fst) .fst
    , ( adequate-above (ch n .fst) (ch n .snd .fst) .snd .fst
      , adequate-above (ch n .fst) (ch n .snd .fst) .snd .snd .snd )
```

把并构造应用于这个充分序数指标序列。与前面一样，并中的成员只能在命题截断下局部化到某一项。

```agda
  module U = Union (λ n → ch n .fst) (λ n → ch n .snd .fst) using (into; outof; oγ; γ)
```

把这些序数指标的并在代码中记作 `lam`，在正文中记作 `λ`。下文证明的是序数指标 `λ` 同时满足 `Adequate λ` 与 `Superadequate λ`；只在见证子句中使用的相应可构造层是 `Lset λ`。

```agda
  lam : V ℓ
  lam = U.γ
```

由于每个 `ch n` 都是序数，集合论并 `λ` 也是序数。这个论证不推出更强的极限性、正则性或基数性质。

```agda
  olam : IsOrd lam
  olam = U.oγ
```

链的每项严格低于其后继，由 `adequate-above` 产出的严格隶属而来。

```agda
  private
    up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
    up n = adequate-above (ch n .fst) (ch n .snd .fst) .snd .snd .fst
```

由 `ch n ∈ ch (suc n)`，并的向内映射给出 `ch n ∈ λ`。因此序列中的每个充分指标本身都是最终序数指标 `λ` 的成员。

```agda
    ch∈λ : (n : ℕ) → ⟨ ch n .fst ∈ lam ⟩
    ch∈λ n = U.into (suc n) (ch n .fst) (up n)
```

第零个充分指标严格包含 `α`，而它又是构成该并的集合之一。因此 `α ∈ λ`。

```agda
  α∈λ : ⟨ α ∈ lam ⟩
  α∈λ = U.into zero α (adequate-above α oα .snd .snd .fst)
```

给定 `x ∈ λ`，向外映射只给出命题截断的存在性：某个 `n` 满足 `x ∈ ch n`。在每个分支中，该项的充分性给出 `sucV x ∈ ch n`，向内映射继而给出 `sucV x ∈ λ`。目标是一个隶属命题，所以可以从命题截断中消去结果，而不保留 `n`。

```agda
  succ : (x : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ sucV x ∈ lam ⟩
  succ x x∈ = PT.rec (snd (sucV x ∈ lam))
    (λ { (n , x∈n) → U.into n (sucV x) (Adequate.succ (ch n .fst) (ch n .snd .snd) x x∈n) })
    (U.outof x x∈)
```

第零项是充分的，因而包含 `ω`。并的向内映射把这一事实送为 `Adequate λ` 所要求的成员关系 `ω ∈ λ`。

```agda
  ω∈λ : ⟨ ω ∈ lam ⟩
  ω∈λ = U.into zero ω (Adequate.ω∈ (ch zero .fst) (ch zero .snd .snd))
```

对 `c ∈ λ`，向外映射只给出命题截断的存在性：某个 `n` 满足 `c ∈ ch n`。在每个分支中，`ch n` 的充分性在 `Lset (ch n)` 中提供四个见证，而 `ch n ∈ λ` 允许通过单调性把它们搬入 `Lset λ`。由于 `Witnesses (Lset λ) c` 是命题，可以合法地从命题截断中消去。

```agda
  wit : (c : V ℓ) → ⟨ c ∈ lam ⟩ → Witnesses (Lset lam) c
  wit c c∈ = PT.rec (isPropWitnesses (Lset lam) c)
    (λ { (n , c∈n) → λ oc →
      let w = Adequate.wit (ch n .fst) (ch n .snd .snd) c c∈n oc
      in  Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .fst)
```

四个分量都沿 `ch n ∈ λ`，由可构造层的单调性分别搬运：层级表、码集合、满足关系图与环境塔全都从 `Lset (ch n)` 进入 `Lset λ`。

```agda
        , ( Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .fst)
          , ( Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .snd .fst)
            , Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .snd .snd) )) })
    (U.outof c c∈)
```

并的序数性、后继封闭、`ω ∈ λ` 与搬运后的见证合在一起，便得到 `Adequate λ`。前三项谈的是序数指标 `λ`，第四项则把集合放入可构造层 `Lset λ`。这些是后续层级描述所需的闭合事实，并非关于 `Lset λ` 的模型论断言。

```agda
  adequate : Adequate lam
  adequate = olam , ( succ , ( ω∈λ , wit ))
```

对 `d ∈ λ`，向外映射只给出命题截断的存在性：某个 `n` 满足 `d ∈ ch n`。在该截断内作映射并令 `γ = ch n`；这个指标属于 `λ`，包含 `d`，而且充分。结果仍在截断下，因此并未定义选择函数 `d ↦ γ`。

```agda
  super : Superadequate lam
  super d d∈ = PT.map
    (λ { (n , d∈n) → ch n .fst , ( ch∈λ n , ( d∈n , ch n .snd .snd )) })
    (U.outof d d∈)
```

导出的定理显式返回严格位于 `α` 之上的序数指标 `λ`，并附带 `Adequate λ` 与 `Superadequate λ` 的证明。虽然 `λ` 本身是可用的数据，但为其各成员保证的局部充分指标仍处于命题截断下；构造没有给出最小局部指标，也没有给出全局选择族。

```agda
superadequate-above : (α : V ℓ) → IsOrd α
                    → Σ[ lam ∈ V ℓ ] (IsOrd lam × ⟨ α ∈ lam ⟩ × Adequate lam × Superadequate lam)
superadequate-above α oα =
  Super.lam α oα , ( Super.olam α oα , ( Super.α∈λ α oα , ( Super.adequate α oα , Super.super α oα )))
```

## 一层属于其后继层

对每个外围集合 `β`，整个集合 `Lset β` 都是 `Lset (sucV β)` 的元素；这里不需要假设 `β` 是序数。等式 `Lset (sucV β) = 𝒟ₒ (Lset β)` 把目标化为 `Lset β` 上的可定义性，而恒真公式恰把整个载体定义为其自身的一个子集。结论是集合 `Lset β` 属于下一可构造层，这与一个层逐点包含于另一个层是不同的陈述。

```agda
Lset∈suc : (β : V ℓ) → ⟨ Lset β ∈ Lset (sucV β) ⟩
Lset∈suc β = subst (λ w → ⟨ Lset β ∈ w ⟩) (sym (Lset-suc β))
  (𝒟ₒ-intro (Lset β) (Lset β) ∣ ⊤̇ , DefOf.defSet⊤≡A (Lset β) ∣₁)
```