GCH 论证所需的充分层

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

module Adequate (γ : V ℓ) (ad : Adequate γ) where

ord = ad .fst
succ = ad .snd .fst
ω∈ = ad .snd .snd .fst
wit = ad .snd .snd .snd

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

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

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

α 的每个被呈现元素都是序数，因为序数的元素是序数。

  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 ((f (ι α m) (oc m)) .fst) ((f (ι α m) (oc m)) .snd)

诞生层索引 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 ((f (ι α m) (oc m)) .fst) ((f (ι α m) (oc m)) .snd)

这里取五个严格公共界。前四个分别约束 α 的每个被呈现元素所对应的层级表、码集、满足图与环境塔的诞生层索引；第五个直接约束各序数后继 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 : ⟪ α ⟫) → ⟨ (f (ι α m) (oc m)) .fst ∈ 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 ((f (ι α m) (oc m)) .fst) ((f (ι α m) (oc m)) .snd)))

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

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

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

          (land At.codes b2 b2∈ m)
      , ( subst (λ u → ⟨ (At.table (ι α m) u) .fst ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
            (land At.table b3 b3∈ m)
        , subst (λ u → ⟨ (At.tower (ι α m) u) .fst ∈ 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∈

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 = map₁ (λ { (n , hn) → lower n , hn })
  (union-family-out (Lift {ℓ-zero} {ℓ} ℕ) F x h)

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  = 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∈ = rec₁ ((sucV x ∈ γ) .snd)
  (λ { (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∈ = 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 ))

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

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

ch : ℕ → Σ[ γ ∶ V ℓ ] (IsOrd γ × Adequate γ)
ch  =
  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∈ = rec₁ ((sucV x ∈ lam) .snd)
  (λ { (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∈ = 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∈ = map₁
  (λ { (n , d∈n) → ch n .fst , ( ch∈λ n , ( d∈n , ch n .snd .snd )) })
  (U.outof d d∈)