GCH 论证所需的充分层

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

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

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

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

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

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

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

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 的单调性。另一些序数事实保证序数的成员、这些成员的后继以及途中使用的公共界仍是序数。因此，取界论证作用于指标，而其结论则把见证集合放进一层之内。

  ( 𝒮ʟ; 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 相关的四个可构造集合：内部层级表、全体公式码之集、统一满足关系的图，以及环境塔。充分性把这四个集合一同放进同一个更后的可构造层，使一条有界描述能够在那里遍历它们。

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 )

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

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 )

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

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 ℓ 中的隶属，不应与下一步引入的可构造载体内部隶属混同。

open hPropStructure 𝒮ᵥ

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

module CS = hPropStructure 𝒮ʟ using (S)

充分层所容纳的四个见证

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

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

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

  A : CS.S
  A = LsetS c oc

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

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

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

  hier : CS.S
  hier = hierL c cL oc

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

  codes : CS.S
  codes = AllCodes A

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

  table : CS.S
  table = SatGraph.pairs A

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

  tower : CS.S
  tower = Tower.tower A

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

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 ⟩

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

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

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

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 γ。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    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 得出；应用时使用见证的底层集合及其可构造性证据。

    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)。这些都是序数指标之间的界；第五族并不是一族诞生层。

    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 则合并四个见证界。这里不声称所得界最小；这些运算只给出严格公共界及所需的隶属证明。

    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)

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

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

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

  β : V ℓ
  β = b11 .fst

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

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

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

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

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

    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 也属于 β。重复同一传递性论证，便会把其余每个见证界都放入 β。

    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 下处于相同位置，所以下一行将闭合这个对称论证。

    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 ∈ β。至此，四个诞生层之界都已与公共序数指标 β 建立严格隶属关系。

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

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

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

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

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

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

  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 的呈现索引之纤维取值于命题。

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

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

  private

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

    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 β。两步分别依据相应序数指标之间的严格隶属关系。

      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 认同。

    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) 的全部四个分量，而且结果不依赖某一份特定的序数性证明。

            (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 的四个见证；这一步既不消去命题截断，也不作选择。

  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 开始。取并本身不要求该族单调；后面的两次应用会另行证明每一项属于其后继项。

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

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

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

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

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

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

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

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

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

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

  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，再对所得序数指标取并。

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

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

  private
    base = bound2 p ω op ω-ord

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

  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)

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

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

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

  γ : V ℓ
  γ = C.γ

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

  oγ : IsOrd γ
  oγ = C.oγ

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

  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 单调性所需的指标比较。

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

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

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

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

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

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

  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 是命题，可以把所得结果从命题截断中消去。

  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) 到指标 γ 的单调性。分别把它用于层级表、码集合、满足关系图与环境塔，便完成四分量的见证元组。

      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 γ。后文所用的充分性，其全部内容正是这四条。

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

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

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，但命题截断既不保留选定的 γ，也不保留最小的 γ。

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

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

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

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

  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)。该定理显式提供某个这样的下一指标，但不声称其最小。

    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 )

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

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

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

  lam : V ℓ
  lam = U.γ

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

  olam : IsOrd lam
  olam = U.oγ

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

  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 ∈ λ。因此序列中的每个充分指标本身都是最终序数指标 λ 的成员。

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

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

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

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

  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 λ 所要求的成员关系 ω ∈ λ。

  ω∈λ : ⟨ ω ∈ 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 是命题，可以合法地从命题截断中消去。

  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 λ。

        , ( 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 λ 的模型论断言。

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

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

  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 λ 的证明。虽然 λ 本身是可用的数据，但为其各成员保证的局部充分指标仍处于命题截断下；构造没有给出最小局部指标，也没有给出全局选择族。

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 β 属于下一可构造层，这与一个层逐点包含于另一个层是不同的陈述。

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