有界子集落在受控层

module At (κ : S) (oκ : IsOrd (κ .fst)) (cκ : IsCardinalL κ)
          (κ∉ω : ⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
          (y : S) (y⊆κ : (z : V ℓ) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ κ .fst ⟩) where

由 κ 的序数性与 κ ∉ ω 可得 ω ⊆ κ。每个有限 von Neumann 数码 # k 都属于 ω，所以对每个 k 都有 # k ∈ κ。这些元素将充当并集编码中的有限标签。

num∈κ : (k : ℕ) → ⟨ # k ∈ κ .fst ⟩
num∈κ k = ω⊆ (κ .fst) oκ κ∉ω (# k) (#∈ω k)

序数 κ 与以它为指标的可构造层是两个不同的集合。因此把 Lset κ 打包为内部集合 Lκ；该层将构成起始集的主要部分，而 κ 自身仍是起始集所要编码单射入的基数。

Lκ : S
Lκ = LsetS (κ .fst) oκ

为了把 κ 与 y 放进同一个层，先在 L 内形成二者的无序对。任何包含该对的传递层都会包含它的两个元素，因此只需一次出现层构造便能同时处理这两个对象。

private
  P₀ : S
  P₀ = pairʟ κ y

选取序数层索引 α₀，使该无序对出现在其所索引的层中。这只是由可构造性给出的一个方便的出现索引；这里没有断言 α₀ 是该对最早出现的层。

  α₀ : V ℓ
  α₀ = stage (P₀ .fst) (P₀ .snd)

所选层索引 α₀ 是序数。这一点很关键：下一步要取得严格高于它的超充分序数，稍后还要用序数的传递性把 κ 从 α₀ 以下继续送入 lam。

  oα₀ : IsOrd α₀
  oα₀ = stage-ord (P₀ .fst) (P₀ .snd)

基数 κ 属于 Lset α₀。这是因为 κ 是无序对的元素，该无序对属于 Lset α₀，而这一层是传递集。这里得到的是层成员关系，尚不是后文所用的序数成员关系 κ ∈ α₀。

  κ∈Lα₀ : ⟨ κ .fst ∈ˢ Lset α₀ ⟩
  κ∈Lα₀ = layer-trans (Lset-layer α₀) {x = P₀ .fst} {y = κ .fst}
    (pairʟ-in κ y κ (inl refl)) (stage-mem (P₀ .fst) (P₀ .snd))

同一个传递性论证经无序对的另一元素把 y 放进 Lset α₀。与 κ 不同，并未假设 y 是序数，所以后文会用层的单调性把这一事实搬到 Lset lam，而不会把它转换成 y ∈ α₀。

  y∈Lα₀ : ⟨ y .fst ∈ˢ Lset α₀ ⟩
  y∈Lα₀ = layer-trans (Lset-layer α₀) {x = P₀ .fst} {y = y .fst}
    (pairʟ-in κ y y (inr refl)) (stage-mem (P₀ .fst) (P₀ .snd))

现在显式选取超充分序数 lam，满足 α₀ ∈ lam。这个严格扩张提供后续壳与凝聚论证所需的闭包性质。lam 自身虽是显式数据，但其超充分性所保证的局部充分指标仍处于命题截断下。

  sa = superadequate-above α₀ oα₀

把这个高序数在代码中记作 lam，正文中记作 λ。它的具体构造后文不再起作用；证明只使用其序数性、后继闭包、超充分性以及它高于 α₀ 这一事实。

opaque
  lam : V ℓ
  lam = sa .fst

首先保留的事实是 lam 为序数。因此它是传递集，这使得 lam 以下的序数成员关系可以继续向上传递。

  ordλ : IsOrd lam
  ordλ = sa .snd .fst

其次保留对序数后继的闭包：只要 d ∈ lam，便有 sucV d ∈ lam。这项闭包是保证有限 Skolem 构造留在 lam 所索引层内的结构前提之一。

  succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
  succλ = sa .snd .snd .snd .fst .snd .fst

超充分性表示：对每个 d ∈ lam，都仅仅存在充分序数 γ，满足 d ∈ γ ∈ lam。它在 lam 以下提供局部的充分空间，却不选取最小的 γ，也不选取这样一族 γ。

  sup : Superadequate lam
  sup = sa .snd .snd .snd .snd

基数 κ 属于序数索引 lam。由于 κ 与 α₀ 都是序数，先由 κ ∈ Lset α₀ 得到 κ ∈ α₀；再结合 α₀ ∈ lam 与序数 lam 的传递性，得到 κ ∈ lam。这个结论说的是属于索引 lam，而不是属于层 Lset lam。

  κ∈λ : ⟨ κ .fst ∈ˢ lam ⟩
  κ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ (κ .fst) oκ κ∈Lα₀) (sa .snd .snd .fst)

对 y，所需结论则是它属于层 Lset lam。由 α₀ ∈ lam，层的单调性给出 Lset α₀ ⊆ Lset lam；把它用于先前的 y ∈ Lset α₀，便得到 y ∈ Lset lam。这里不需要假设 y 是序数。

  y∈Lλ : ⟨ y .fst ∈ˢ Lset lam ⟩
  y∈Lλ = Lset-mono {α = lam} {β = α₀} (sa .snd .snd .fst) y∈Lα₀

y 的每个外围元素都属于 Lset κ。子集前提先把 z ∈ y 送到 z ∈ κ；由于 κ 是序数，这样的 z 本身也是序数，属于自己的后继层，再由累积性得到 z ∈ Lset κ。因此，y ⊆ κ 给出了使起始集成为传递集所需的层包含关系。

y⊆Lκ : (z : V ℓ) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ Lset (κ .fst) ⟩
y⊆Lκ z hz = ord⊆Lset (κ .fst) oκ z (y⊆κ z hz)

在 Lset lam 内形成起始集 X = Lset κ ∪ {y}。它包含 y，并且是传递集：来自 Lset κ 的元素仍留在这个传递层中；来自 y 的元素则由假设属于 κ，因而属于 Lset κ。这项传递性正是后文使塌缩固定 y 的原因。

module UK = UnionKit (κ .fst) lam (y .fst) oκ ordλ κ∈λ y⊆Lκ y∈Lλ κ∉ω
  using ( X; X⊆Lλ; ∅∈λ; Lα∈X; x∈X; X-mem; sgl≡; Xtr )

下文用 X 表示这个由 Lset κ 扩张而成的传递集。需要保留的两项性质彼此配合：y ∈ X 保证壳包含待定位的集合，传递性则保证塌缩不会改变它。

X : V ℓ
X = UK.X

为了计数，在内部构造单点集 {y} 及其到 κ 的编码单射，其中使用标签 0 ∈ κ，再把它与 Lκ 作内部并。这样得到同一集合 Lset κ ∪ {y} 的编码呈现，其两个部分已经分别带有带标签并集论证所需的单射。

module Pt = Point κ (num∈κ ) y using ( Y; Y-out; Y-in; injL )
module U = Union2 Lκ Pt.Y using ( D; out; in₁; in₂ )

把这个内部构造的并记作 Xʟ。它与 X 表示同一个数学并集，但其构造附带了证明它编码单射入 κ 所需的内部数据。

Xʟ : S
Xʟ = U.D

为了把 Xʟ 与 X 识别起来，双向比较二者的元素。正向中，属于内部编码并意味着在命题截断下分成两种情形：属于 Lset κ，或属于编码单点集；两种情形都推出属于 X。由于属于 X 是命题，这次消去是合法的。

Xʟ-eq : Xʟ .fst ≡ X
Xʟ-eq = extensionalV {a = Xʟ .fst} {b = X} (λ z → ⇔toPath (fwd z) (bwd z))
  where
  fwd : (z : V ℓ) → ⟨ z ∈ˢ Xʟ .fst ⟩ → ⟨ z ∈ˢ X ⟩
  fwd z h = rec₁ ((z ∈ˢ X) .snd) go (U.out zS h)

在层这一分支中，左侧包含把该元素放入 X。把 z 暂时打包为可构造集合是由 L 的传递性保证的：既然 z 属于可构造集合 Xʟ，它自身也可构造。

    where
    zS : S
    zS = z , isL-trans {x = Xʟ .fst} {y = z} h (Xʟ .snd)
    go : ⟨ z ∈ˢ Lset (κ .fst) ⟩ ⊎ ⟨ z ∈ˢ Pt.Y .fst ⟩ → ⟨ z ∈ˢ X ⟩
    go (inl hz) = UK.Lα∈X z hz

在单点分支中，编码元素等于已知属于 X 的 y。反向中，属于 X 同样只在命题截断下拆分为 Lset κ 一侧与单点一侧；目标「属于 Xʟ」是命题，因此第二次消去同样合法。

    go (inr hz) = subst (λ w → ⟨ w ∈ˢ X ⟩) (sym (Pt.Y-out zS hz)) UK.x∈X
  bwd : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Xʟ .fst ⟩
  bwd z h = rec₁ ((z ∈ˢ Xʟ .fst) .snd) go (UK.X-mem z h)
    where
    go : ⟨ z ∈ˢ Lset (κ .fst) ⟩ ⊎ ⟨ z ∈ˢ ⁅ y .fst ⁆s ⟩ → ⟨ z ∈ˢ Xʟ .fst ⟩

反向的两个分支分别进入 Xʟ 的两个并项。Lset κ 的元素从左侧进入，其可构造性由该层继承；{y} 的元素先与 y 识别，再从编码单点集一侧进入。因此外延性给出 Xʟ .fst ≡ X，而不保留任何一次截断的分支选择。

    go (inl hz) = U.in₁ (z , isL-trans {x = Lset (κ .fst)} {y = z} hz (Lκ .snd)) hz
    go (inr hz) = subst (λ w → ⟨ w ∈ˢ Xʟ .fst ⟩) (sym (UK.sgl≡ z hz)) (U.in₂ y Pt.Y-in)

起始集合可构造，因为内部副本可构造且两副本底层集合相等。

X-isL : ⟨ isL X ⟩
X-isL = subst (λ w → ⟨ isL w ⟩) Xʟ-eq (Xʟ .snd)

把 X 连同这份可构造性证明打包为 XS : S。它的底层外围集合仍恰好是 X；这项打包只提供 InjL 所要求的内部定义域。

XS : S
XS = X , X-isL

无穷基数平方律给出编码单射 κ × κ ↪ κ 的命题截断存在。它所需的前提正是开头固定的事实：κ 是序数、内部基数且不属于 ω。这里既不产生双射，也不产生一张选定的单射图。

pairκ : InjL (prodL κ) κ
pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (κ .fst) (κ .snd) oκ cκ κ∉ω

两条分量单射输入带标签并的构造，得到编码单射 Xʟ ↪ κ × κ：标签 #0 与 #1 区分层部分和单点集部分。再与平方律给出的单射复合，得到 Xʟ ↪ κ；最后沿 Xʟ .fst ≡ X 搬运定义域，把它换成可构造包装 XS。所得正是需要的编码单射 X ↪ κ，并且仍处于命题截断下。

base : InjL XS κ
base = move Xʟ XS κ κ Xʟ-eq refl
  (injl-trans Xʟ (prodL κ) κ
    (tag-union κ (num∈κ ) (num∈κ ) Lκ Pt.Y (stage-counted κ Lκ oκ κ∉ω refl) Pt.injL)
    pairκ)

令 M 为 X 在 Lset lam 内生成的 Skolem 壳。适用于这个壳的 Tarski-Vaught 定理表明，M 具有凝聚所需的初等性。整个传递集 X 就是起始集，因此这正是包含 y、且其塌缩稍后将固定 y 的同一个壳。

elem = HullElemDown.elem lam ordλ X UK.X⊆Lλ UK.∅∈λ

壳计数定理把 X ↪ κ 依次传过 Skolem 闭包的有限阶段及这些阶段的并，得到编码单射 M ↪ κ 在命题截断下的存在性。于是，这个壳既具有应用凝聚所需的初等性，其大小又仍受 κ 控制。

hull↪κ = Count.hull↪κ lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL κ oκ cκ κ∉ω base

凝聚给出显式序数 β，并把 M 的塌缩像识别为 Lset β。它还把 Lset β 与 M 打包为可构造集合，并通过逆塌缩给出编码单射 Lset β ↪ M 的命题截断存在。这里 β 是层索引，Lset β 才是它所索引的层。

module St = Site lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL
  using ( β; oβ; ext; Lβ; βL; hullL; Lβ↪M )

下面使用同一个壳构造的三个方面：壳 M、包含关系 X ⊆ M，以及像为 πX 的塌缩映射 π。相应的不动点定理适用于 M 的传递子集。这些事实将先证明塌缩不改变 y，再把同一个 y 放入凝聚所识别出的层中。

module HS = HullStage lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( M )
module HSH = HullStage.H lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( X⊆M )
module HSC = HullStage.C lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ
  using ( πX; π; fixes; πX-intro )

集合 y 属于 Skolem 壳 M：它已被放入起点集 X，而 X 的每个元素都属于由 X 生成的壳。

y∈M : ⟨ y .fst ∈ˢ HS.M ⟩
y∈M = HSH.X⊆M (y .fst) UK.x∈X

塌缩固定 y：因为起点集 X 传递且包含于壳中，塌缩映射在 X 的每个元素上恒等，而 y 即为其中之一。

πy : HSC.π (y .fst) ≡ y .fst
πy = HSC.fixes X
  (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
  UK.Xtr (y .fst) UK.x∈X

由于 y 属于壳，塌缩像包含 π(y)。凝聚把这个像认同为可构造层 Lset β，再由不动点等式 π(y) = y 得到 y ∈ Lset β。关键在于，塌缩没有用另一个集合替换 y，而是把原来的 y 定位在一个受控的可构造层中。

y∈Lβ : ⟨ y .fst ∈ˢ Lset St.β ⟩
y∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πy
  (subst (λ w → ⟨ HSC.π (y .fst) ∈ˢ w ⟩) St.ext (HSC.πX-intro (y .fst) y∈M))

序数 β 经三条编码单射的链注入 κ：由序数成员关系从 β 到层 Lset β 的包含、由受限逆塌缩从 Lset β 到壳 M 的单射、以及由壳计数从 M 到 κ 的单射。这条链给出的是编码单射，而非裸序数比较。

β↪κ : InjL St.βL κ
β↪κ = injl-trans St.βL St.Lβ κ
  (inclusion-coded St.βL St.Lβ (λ z hz → ord⊆Lset St.β St.oβ z hz))
  (injl-trans St.Lβ St.hullL κ St.Lβ↪M hull↪κ)

局部见证现把可构造序数 β、它的序数性、y 属于层 Lset β 的事实，以及编码单射 β ↪ κ 打包在一起。这里返回的是层指标 β，而 Lset β 是已经容纳 y 的可构造层；二者不可混同。

result : Σ[ b ∶ S ] (IsOrd (b .fst) × ⟨ y .fst ∈ˢ Lset (b .fst) ⟩ × InjL b κ)
result = St.βL , St.oβ , y∈Lβ , β↪κ