---
title: "把无穷可构造层单射到其指标"
module: L.GCH.StageInjection
lang: zh
site: "Bedrock"
description: "把无穷可构造层单射到其指标"
stage: "证明 GCH"
reading_order: 118
canonical: https://bedrock.institute/zh/L.GCH.StageInjection.html
html: L.GCH.StageInjection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/StageInjection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Absoluteness, V.Hierarchy, V.Collapse, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals, L.Stage, L.Cardinal, L.GCH.Assembly, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.SkolemHull, L.GCH.ConstructibleHull, L.GCH.CardinalSquareLaw, L.GCH.AdequateStages, L.GCH.StageCountingTools, L.GCH.HullCounting]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.StageInjection.md, https://bedrock.institute/ja/L.GCH.StageInjection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 把无穷可构造层单射到其指标

本章证明 GCH 所用的层估计：若 `δ` 是非有限的可构造序数，则 `Lset δ` 有一条到 `δ` 的内部编码单射。结论 `InjL` 是「满足单射条件的可构造图」这一类型的命题截断。因此，它只断言这样的图存在，而不保留某个选定的图；它既不声称给出宿主层函数，也不声称双射，并且不假设 `δ` 本身是内部基数。

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

本章反复区分存在与选择。经典推理提供合适的层和基数代表，而每条对外给出的单射始终处于命题截断之下。因此，局部见证可以在命题性论证内部使用，却不会变成典范的全局数据。

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

论证对宇宙层级一致，只使用明示的排中律实例 `lem : LEM (ℓ-suc ℓ)`。特别地，后文转到内部基数代表时，并未暗中增加「原序数 `δ` 是基数」这一假设。

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

要把逆塌缩变成 `L` 内部的单射，必须用可构造结构的一阶语言表达它的图。这里只需变元、常元、隶属与合取。公式改名会交换两个实参位置而保持满足关系，外围累积层级则提供计算塌缩所用的集合。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

壳具备所需的外延性，因此塌缩在壳上单射。后文中，`self∈sucV` 把 `δ` 放入其集合论后继 `δ+1`；可构造层引理则提供传递性、单调性以及层与其分层之间的联系。这个论证始终区分序数后继与可构造后继层。

```agda
open import V.Collapse {ℓ} using ( isExt )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω; suc-ord )
```

后文会使用两条互补的层事实。一个可构造层可以打包为 `L` 的元素；若序数 `x` 属于层 `Lset α`，则秩比较给出 `x ∈ α`。目标 `InjL` 记录内部编码单射仅仅存在，而 `IsCardinalL` 只会用于稍后引入的基数代表。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
```

所需估计由接口 `StageCountedCoded` 表述。证明先以内部基数代表 `μ` 表示任意无穷序数 `δ` 的基数，再把合适的 Skolem 壳计数到 `μ` 中，最后复合编码单射。为使逆塌缩能够加入这条链，证明会把它表示为可定义映射，其图是 `L` 的元素。

```agda
open import L.GCH.Assembly {ℓ} lem using ( StageCountedCoded )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.SkolemHull {ℓ} lem
```

整体比较由三项材料组成。凝聚把壳变成层 `Lset β`；非有限序数的移位与基数代表 `μ` 使起点可单射到 `μ`；最后，复合把这些局部比较接回所需的两个端点。这些步骤都不会把内部编码单射变成宿主层函数。

```agda
  using ( module Frame; module HullStage; module HullElemDown )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module PiIn; module Condense′ )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( ordL; ω⊆; no-fin; module Shift )
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )
```

壳计数定理是这里的定量输入：只要起始集合单射入一个非有限内部基数，由它生成的壳也单射入该基数。后文还会使用「每个序数包含于其自身可构造层」，以及「可构造性证明是命题，因此底层集合相等就决定可构造载体元素相等」。

```agda
open import L.GCH.HullCounting {ℓ} lem using ( ord⊆Lset; module Count; S≡ )
```

逆塌缩将作为可构造载体 `S` 的元素之间的映射来比较。这样的元素同时包含底层集合与可构造性证明，但证明分量是命题。因此，底层集合相等便决定 `S` 中的相等，编码图不会依赖用哪份可构造性证据呈现其值。

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
```

非有限性在后面的计数论证中有两项具体作用：它给出移位单射 `δ+1 ↪ δ`，并保证每个有限序数，特别是空集，都位于 `δ` 之下。逆塌缩公式所用的二元环境与这项无穷性论证彼此独立。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet; ∅ )
open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Vec using ( _∷_; [] )
import Cubical.Data.Empty as Empty
```

命题截断出现在两个关键位置。证明壳满足某个公式时，它允许从壳仅仅可构造这一事实消去到命题性的满足陈述；同时，每个 `InjL` 结论的最外层也正是命题截断。因此，这里的截断消去总是以命题为目标。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( squash₁ )
```

记作 `_∈ˢ_` 的隶属是外围层级结构 `𝒮ᵥ` 中的隶属。壳、其塌缩像与序数指标尚未打包为可构造结构的元素时，关于它们的陈述都使用这种隶属。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

类型 `S` 是可构造结构的载体：它的一个元素由外围集合及其属于 `L` 的证明组成。下文内部编码映射的定义域、陪域与图参数都属于这个载体。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

对象语言公式在 `𝒮ʟ` 中的满足关系经绝对性读作关于外围集合的相应命题。这座桥梁使证明可以先在外围建立逆塌缩图，再把同一个关系打包为 `L` 内部的可定义图。

```agda
open FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using () renaming ( _⊨ᵐ_ to _⊨_ )
```

这里需要协调一处约定差异。塌缩公式 `piFo` 按 `(v,x)` 的顺序读取像值与原像，而可定义映射的图按 `(x,v)` 的顺序求值。交换两个自由变元，再利用满足关系在改名下的不变性，就能以所需顺序表达同一关系；模型与公式含义都没有改变。

```agda
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
```

## 在超充分层计数 Skolem 壳

先把论证的几何部分与后面的基数估计分开。固定一个对后继封闭的序数 `lam`，以及包含于 `Lset lam` 的起始集合 `X`；还假设该指标包含空集，并且由 `X` 生成的 Skolem 壳具有所需的初等性。此时尚未涉及任何目标基数。

```agda
module Site (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆Lλ ∅∈λ)
```

`lam` 的超充分性提供凝聚所需的闭包与正确性条件。`X` 的可构造性保证生成壳时逐次得到的有限闭包层，以及这些闭包层的并，仍留在 `L` 中。因此，壳及其塌缩像都能在可构造结构内部表示。

```agda
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩) where
```

凝聚由此把塌缩像认同为某个序数 `β` 所索引的 `Lset β`。另一方面，壳构造证明壳 `M` 可构造。这两条事实恰好使逆塌缩能够被视为从一个可构造层到一个可构造壳的映射。

```agda
  condenses′ = Condense′.condenses′ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
  M-isL = Condense′.M-isL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
```

把塌缩记作 `π : M → πX`，并以 `πX` 表示其像。塌缩机制提供 `πX` 中各点的原像、塌缩在外延壳上的单射性，以及它固定壳中传递部分这一事实。公式 `piFo` 表示 `π` 的图；其充分性引理会把该公式的满足关系与实际塌缩值联系起来。

```agda
  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( πX; π; fixes; πX-intro; πX-member )
  module P = PiIn (HS.M , M-isL) using ( piFo; up; good-at; piFo-val )
```

序数 `β` 衡量塌缩像所处的高度。在这个一般场址中，尚无待计数的序数 `δ`，也无目标基数，因此此时不能把 `β` 与二者中的任何一个比较。

```agda
  β : V ℓ
  β = condenses′ .fst
```

随附的序数性证明使 `Lset β` 成为真正由序数索引的层。稍后把某个序数属于 `Lset β` 转换为它与 `β` 的序数比较时，也必须使用这份证明。

```agda
  oβ : IsOrd β
  oβ = condenses′ .snd .fst
```

等式 `ext : πX = Lset β` 是塌缩理论与可构造层级之间的枢纽。它把塌缩像中的隶属转换为 `β` 处层中的隶属；稍后证明塌缩固定 `δ` 后，正是沿这条等式得到 `δ ∈ Lset β`。

```agda
  ext : HSC.πX ≡ Lset β
  ext = condenses′ .snd .snd
```

由于 `β` 是序数，`Lset β` 可构造，因而可以打包为载体 `S` 的元素 `Lβ`。这个打包后的层将成为逆塌缩映射的定义域。

```agda
  Lβ : S
  Lβ = LsetS β oβ
```

序数 `β` 本身也可构造，并被打包为 `βL`。逆塌缩映射使用的是 `Lβ`，而打包后的指标会在后面的有界子集论证中用于通过内部编码单射比较 `β` 与目标基数。

```agda
  βL : S
  βL = ordL β oβ
```

内部编码映射的陪域必须是载体 `S` 的元素，不能只是外围描述的壳成员类。元素 `hullL` 给出壳在内部的这种呈现，并携带其可构造性证据。

```agda
  hullL : S
  hullL = Condense′.hullL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
```

等式 `M≡` 连接壳的两种呈现。塌缩定理谈论外围集合 `M`，内部图则谈论载体元素 `hullL`；沿这条等式搬运后，同一份隶属证据即可用于两边。

```agda
  M≡ : fst hullL ≡ HS.M
  M≡ = Condense′.hullL-spec lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
```

壳框架证明 `M` 上的隶属关系具有外延性。这正是从「壳的两个成员具有相同塌缩值」推出它们相等所需的假设。

```agda
  Mext : isExt HS.M
  Mext = Frame.Mext lam ordλ succλ X X⊆Lλ ∅∈λ
```

把塌缩单射性定理施于这个外延壳，便得到 `π-inj`。它既用于证明每个原像唯一，也用于证明由这些原像构造的逆塌缩映射单射。

```agda
  module CI = HullStage.C.InjExt lam ordλ succλ X X⊆Lλ ∅∈λ Mext using ( π-inj )
```

塌缩值 `v` 的原像，是其塌缩等于 `v` 底层集的壳元素 `x`。该记录是未截断的依赖对：原像、其隶属及其同一视都被显式携带。

```agda
  Pre : S → Type (ℓ-suc ℓ)
  Pre v = Σ[ x ∈ V ℓ ] (⟨ x ∈ˢ HS.M ⟩ × (HSC.π x ≡ fst v))
```

原像唯一，因为塌缩在壳上单射：值相同的两条记录经 `π-inj` 认同其原像，其余分量都是命题。正因如此，无需选择即可恢复原像。

```agda
  isPropPre : (v : S) → isProp (Pre v)
  isPropPre v (x , mx , e) (x' , mx' , e') =
    Σ≡Prop (λ x → isProp× (snd (x ∈ˢ HS.M)) (setIsSet _ _)) (CI.π-inj x x' mx mx' (e ∙ sym e'))
```

逆塌缩只需定义在其像中的点上，而凝聚已把该像认同为 `Lset β`。因此，`Mem v` 是「`v` 的底层集合属于这个层」这一命题；正是这份定义域证据保证原像类型有元素。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem v = ⟨ fst v ∈ˢ fst Lβ ⟩
```

属于 `Lset β` 起初只给出塌缩原像类型的命题截断。由于 `Pre v` 已经证明为命题，截断消去可以恢复其中唯一的元素。因此，`pre` 依靠唯一性取得逆像值，并未在多个竞争原像之间作任意选择。

```agda
  pre : (v : S) → Mem v → Pre v
  pre v m = PT.rec (isPropPre v) (λ w → w)
    (HSC.πX-member (fst v) (subst (λ w → ⟨ fst v ∈ˢ w ⟩) (sym ext) m))
```

原像被打包为可构造集合：其可构造性经「打包壳等于壳」的同一视从壳搬运而来。该函数只定义在 `β` 处层的成员上，以壳为陪域；它是塌缩在其像上的逆，而非全局逆函数。

```agda
  fn : (v : S) → Mem v → S
  fn v m = pre v m .fst
         , isL-trans {x = fst hullL} {y = pre v m .fst}
             (subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)) (snd hullL)
```

改名交换两个变元槽：零槽变为一槽，反之亦然。

```agda
  ρ : Fin 2 → Fin 2
  ρ zero = suc zero
  ρ (suc zero) = zero
```

两个环境以相反顺序列出同样的载体元素。证明 `ag` 对两个变元指标逐一核对：先应用 `ρ` 再查找变元，与在交换后的环境中查找该变元相同。这种逐点一致正是改名保持满足关系所需的假设。

```agda
  private
    ag : (x v : S) → Ren.Agrees ρ (x ∷ v ∷ []) (v ∷ x ∷ [])
    ag x v zero = refl
    ag x v (suc zero) = refl
```

改名公式在有序环境处的满足等于原公式在交换环境处的满足；这正是安排塌缩图槽位所用的搬运。

```agda
    rn : (x v : S) → ⟨ (x ∷ v ∷ []) ⊨ renameFo ρ P.piFo ⟩ ≡ ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
    rn x v = cong ⟨_⟩ (Ren.⊨-rename ρ P.piFo (x ∷ v ∷ []) (v ∷ x ∷ []) (ag x v))
```

逆塌缩图即该合取：原像属于壳，且改名后的配对图对原像与值成立。

```agda
  invFo : Formula S 2
  invFo = (var zero ∈̇ con hullL) ∧̇ renameFo ρ P.piFo
```

若壳成员 `x` 的塌缩为 `v`，则实际的有序对 `(v,x)` 满足 `piFo`。壳的可构造性本身经命题截断给出，因此证明把该截断消去到命题性的满足陈述，并在任意包含该壳的可构造层中完成构造。

```agda
  π-graph : (x : S) (mx : ⟨ fst x ∈ˢ HS.M ⟩) (v : S) → HSC.π (fst x) ≡ fst v
          → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
  π-graph x mx v e = PT.rec (snd ((v ∷ x ∷ []) ⊨ P.piFo)) read M-isL
    where
    read : Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ HS.M ∈ˢ Lset α ⟩) → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
```

读取陈述搬运两个槽：塌缩值与 `v` 的底层集同一视，壳成员与 `x` 的底层集同一视。

```agda
    read (α , oα , M∈Lα) =
      subst2 (λ a b → ⟨ (a ∷ b ∷ []) ⊨ P.piFo ⟩)
        (S≡ {x = HSC.π (fst x) , G .fst} {y = v} e) (S≡ {x = P.up (fst x) mx} {y = x} refl)
        (G .snd mx)
      where
```

给定一个包含该壳的可构造层 `Lset α`，分层的传递性把每个壳成员 `x` 放入同一层。引理 `good-at` 随后给出 `π x` 的可构造性证明，并证明打包后的塌缩值与打包后的成员满足 `piFo`。

```agda
      G = P.good-at α oα (fst x) mx (layer-trans (Lset-layer α) {x = HS.M} {y = fst x} mx M∈Lα)
```

证明 `defines` 把实际逆像值连接到内部公式。其第一分量把该值放入打包后的壳，第二分量则结合塌缩等式与公式改名，证明 `invFo` 把这个值关联到相应的像点。

```agda
  defines : (v : S) (m : Mem v) → ⟨ (fn v m ∷ v ∷ []) ⊨ invFo ⟩
  defines v m =
      subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    , transport (sym (rn (fn v m) v)) (π-graph (fn v m) (pre v m .snd .fst) v (pre v m .snd .snd))
```

只剩下原像需要识别：任何满足逆图的原像与打包后的原像有相同的塌缩值，而塌缩的单射性返回两个原像的相等。

```agda
  only : (v : S) (m : Mem v) (x' : S) → ⟨ (x' ∷ v ∷ []) ⊨ invFo ⟩ → x' ≡ fn v m
  only v m x' (hx , hp) = S≡ (CI.π-inj (fst x') (pre v m .fst) mx' (pre v m .snd .fst)
    (sym (P.piFo-val x' mx' v (transport (rn x' v) hp)) ∙ sym (pre v m .snd .snd)))
    where
    mx' : ⟨ fst x' ∈ˢ HS.M ⟩
```

若另一个输出 `x'` 满足该图，第一合取支说明其底层集属于打包后的壳。沿 `M≡` 搬运后，便得到它属于外围壳 `M`，这正是利用塌缩单射性把 `x'` 与已恢复原像比较所需的前提。

```agda
    mx' = subst (λ w → ⟨ fst x' ∈ˢ w ⟩) M≡ hx
```

这些结果把受限逆内化为单值的可定义映射。每个 `v ∈ Lβ` 都被送入壳并满足 `invFo`，而 `only` 说明任何满足同一图的其他输出都等于这个值。单射性是进一步的性质，将在下一步另行证明。

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = Lβ ; cod = hullL ; fn = fn
    ; into = λ v m → subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    ; graph = invFo ; defines = defines ; only = only }
```

每个由唯一性确定的原像都满足 `π(pre(v)) = v`。因此，若逆塌缩映射的两个值相等，对该等式施加 `π`，再与两端的原像等式复合，便得到 `v = v'`。所以塌缩像上的逆映射是单射；这一步使用的是右逆等式，而不是塌缩本身的单射性。

```agda
  inj : (v : S) (m : Mem v) (v' : S) (m' : Mem v') → fst (fn v m) ≡ fst (fn v' m') → fst v ≡ fst v'
  inj v m v' m' q = sym (pre v m .snd .snd) ∙ cong HSC.π q ∙ pre v' m' .snd .snd
```

受限逆被打包为从 `Lβ` 到壳的编码单射，完成第一节的构造。打包保持截断形式，只暴露编码图的存在性。

```agda
  Lβ↪M : InjL Lβ hullL
  Lβ↪M = Inj.injL Dmap inj
```

## 把 Skolem 壳塌缩回原层

计数模块 `At` 固定非有限可构造序数 `δL`、其序数性与对 `ω` 的排除；具有相同非有限性的内部基数代表 `μ`；以及 `δL` 与 `μ` 之间双向的编码单射。这些恰是以基数代表计数非有限层所需的数据。

```agda
module At (δL : S) (oδ : IsOrd (fst δL)) (δ∉ω : ⟨ fst δL ∈ˢ ω ⟩ → Empty.⊥)
          (μ : S) (oμ : IsOrd (fst μ)) (cμ : IsCardinalL μ)
          (μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥)
          (δ↪μ : InjL δL μ) (μ↪δ : InjL μ δL) where
```

这里需要区分载体元素 `δL` 与其底层外围序数 `δ = fst δL`。集合论后继、层隶属与塌缩作用于 `δ`，内部编码单射的端点则仍使用打包后的 `δL`。

```agda
  δ : V ℓ
  δ = fst δL
```

序数 `δ` 的层是包含它的最早可构造层；此处它提供寻找足够高的超充分层的起始索引。

```agda
  private
    α₀ : V ℓ
    α₀ = stage δ (snd δL)
```

最小层构造总会返回一个序数索引。把它用于可构造集合 `δ`，便得到 `α₀` 的序数性；这一步并非从另一项「`δ` 是序数」的假设推出。

```agda
    oα₀ : IsOrd α₀
    oα₀ = stage-ord δ (snd δL)
```

序数 `δ` 属于自身所在的层，这正是把 `δ` 锚定在可构造层级内的隶属事实。

```agda
    δ∈Lα₀ : ⟨ δ ∈ˢ Lset α₀ ⟩
    δ∈Lα₀ = stage-mem δ (snd δL)
```

在层索引之上取得一个超充分层；它携带着 Skolem 壳构造与凝聚搬运所需的全部闭包条件。

```agda
    sa = superadequate-above α₀ oα₀
```

取上面给出的超充分层，并把它的序数指标记作 `λ`。后续的壳与凝聚论证都在这个足够高的固定层中进行。

```agda
  opaque
    lam : V ℓ
    lam = sa .fst
```

所选高指标 `λ` 是序数。它的传递性先沿比较 `δ ∈ α₀ ∈ λ` 把 `δ` 放入 `λ`，随后又把 `δ+1` 的每个成员放到 `λ` 之下。

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

对后继封闭是下文立即使用的第二项指标性质：由 `δ ∈ λ` 可得 `δ+1 ∈ λ`。这是关于序数指标 `λ` 的陈述，不能与取可构造后继层混淆。

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

超充分性断言：对 `λ` 的每个成员 `d`，仅仅存在一个仍属于 `λ` 且位于 `d` 之上的充分层 `γ`。这些中间充分层提供计数并凝聚该壳时所需的局部反映与闭包。

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

首先，由 `δ ∈ Lset α₀` 以及 `δ`、`α₀` 都是序数，可得 `δ ∈ α₀`。再由 `α₀ ∈ λ` 和序数 `λ` 的传递性，得到 `δ ∈ λ`。

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

取冯·诺伊曼后继 `X = δ+1` 为起点集。它包含 `δ` 以及每个更小的序数；又因 `δ` 是序数，`X` 是传递集。这些性质正用于稍后证明塌缩固定 `δ`。

```agda
  X : V ℓ
  X = sucV δ
```

序数指标的后继封闭性现给出 `X = δ+1 ∈ λ`。这是一项序数比较。壳构造所需的另一项陈述，即 `X` 的每个成员都属于 `Lset λ`，将在下一步另行推出。

```agda
  sucδ∈λ : ⟨ X ∈ˢ lam ⟩
  sucδ∈λ = succλ δ δ∈λ
```

若 `z ∈ X`，则由序数 `λ` 的传递性与 `X ∈ λ` 得到 `z ∈ λ`。再用序数包含于自身可构造层的一般事实，可得 `z ∈ Lset λ`。因此，所需前提正是 `X ⊆ Lset λ`。

```agda
  X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z hz = ord⊆Lset lam ordλ z (ordλ .fst hz sucδ∈λ)
```

由于 `δ` 非有限，每个有限序数都位于 `δ` 之下，特别有 `∅ ∈ δ`。再结合 `δ ∈ λ` 与序数 `λ` 的传递性，便得到壳构造的另一前提 `∅ ∈ λ`。

```agda
  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = ordλ .fst (ω⊆ δ oδ δ∉ω ∅ (#∈ω zero)) δ∈λ
```

起点集可构造，因为可构造集合的编码后继也可构造，沿认同编码后继与集合论后继的等式运输而来。

```agda
  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) (sucʟ-fst δL) (snd (sucʟ δL))
```

可构造性证明把外围集合 `X = δ+1` 变成载体元素 `XS`。这只改变其呈现；计数问题仍是把 `δ` 的后继单射到基数代表 `μ`。

```agda
  XS : S
  XS = X , X-isL
```

起点由链 `δ+1 ↪ δ ↪ μ` 计数。第一条编码单射是每个非有限序数 `δ` 都具有的移位单射，第二条是从 `δ` 到其基数代表 `μ` 的已知内部单射。复合后得到 `InjL XS μ`，全程无须假设 `δ` 本身是基数。

```agda
  base : InjL XS μ
  base = injl-trans XS δL μ
    (move (sucʟ δL) XS δL δL (sucʟ-fst δL) refl (Shift.injL δL oδ δ∉ω))
    δ↪μ
```

由 `X` 生成的 Skolem 壳在外围层 `Lset λ` 中是初等的。这项初等性使计数定理与凝聚论证能够在壳和该层之间转移相关公式及其见证。

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

Skolem 壳由基数代表 `μ` 计数，因为起点已经单射入 `μ`，而壳章证明封闭保持计数。

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

把一般凝聚构造用于这个壳。它给出序数 `β`，使其层 `Lβ` 正是塌缩像；同时把壳呈现为可构造集合，并由逆塌缩给出命题截断下的编码单射 `Lβ ↪ M`。

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

余下的比较使用该壳的三项性质：其底层集合是 `M`，起点的每个成员都属于 `M`，而塌缩 `π` 把 `M` 映到 `Lβ`，并固定 `M` 的任一传递子集中的成员。把这些性质用于传递起点 `δ+1`，稍后便可把 `δ` 放入 `Lβ`。

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

序数 `δ` 属于自身的后继，后者是壳构造的起点集。

```agda
  δ∈X : ⟨ δ ∈ˢ X ⟩
  δ∈X = self∈sucV δ
```

因此序数 `δ` 属于壳，因为壳包含起点集的每个成员。

```agda
  δ∈M : ⟨ δ ∈ˢ HS.M ⟩
  δ∈M = HSH.X⊆M δ δ∈X
```

后继 `X = δ+1` 是传递集，并且包含于壳 `M`。因此塌缩固定 `X` 的每个成员；特别地，由 `δ ∈ X` 可得 `π(δ) = δ`。

```agda
  πδ : HSC.π δ ≡ δ
  πδ = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    (suc-ord oδ .fst) δ δ∈X
```

序数 `δ` 落在塌缩层 `Lset β` 之内，因为其塌缩 (即自身) 属于塌缩像，而塌缩像等于 `Lset β`。

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

现在可应用序数的层界：若序数 `δ` 属于 `Lset β`，则它必属于序数指标 `β`。因此 `δ ∈ β`。这正是层单调性所需的严格比较，其方向给出 `Lset δ ⊆ Lset β`。

```agda
  δ∈β : ⟨ δ ∈ˢ St.β ⟩
  δ∈β = ord∈Lset→∈ St.β St.oβ δ oδ δ∈Lβ
```

典范载体呈现 `Lδ` 的底层集是 `Lset δ`。`At.result` 以它为始域；最终定理随后会把这个始域搬到任意另一个底层集等于同一层的载体元素上。

```agda
  Lδ : S
  Lδ = LsetS δ oδ
```

最终比较沿链 `Lset δ ↪ Lset β ↪ M ↪ μ ↪ δ` 进行。四条箭头依次来自：利用 `δ ∈ β` 的层单调性、逆塌缩、壳计数，以及已知单射 `μ ↪ δ`。复合它们便证明 `InjL Lδ δL`，即从 `δ` 处的层到 `δ` 的内部编码单射在命题截断下存在。

```agda
  result : InjL Lδ δL
  result = injl-trans Lδ St.Lβ δL
    (inclusion-coded Lδ St.Lβ (λ z hz → Lset-mono {α = St.β} {β = δ} δ∈β hz))
    (injl-trans St.Lβ St.hullL δL St.Lβ↪M
      (injl-trans St.hullL μ δL hull↪μ μ↪δ))
```

对一般的非有限可构造序数 `δ`，`cardOf` 只在命题截断下给出基数代表。证明在消去器内部使用局部代表 `μ`，并应用 `At.result`。由于目标 `InjL Lδ δ` 本身是命题截断下的存在，因而是命题，这项消去合法。所得定理随后既作为 GCH 装配的层计数接口，也用于有界子集论证；它本身只证明 `Lset δ ↪ δ`，并不单独证明 GCH。

```agda
stage-counted : StageCountedCoded
stage-counted δ Lδ oδ δ∉ω q = PT.rec squash₁ build (cardOf δ oδ)
  where
  build : Σ[ μ ∈ S ]
            ( IsOrd (fst μ) × IsCardinalL μ
```

`cardOf` 的一个局部见证记录：`μ` 是序数和内部基数，其底层集包含于 `δ`，并且两个方向的编码单射都存在。包含性证明属于基数代表的数据包，但 `At.result` 并不使用它；该构造使用两条单射以及序数性、基数性和非有限性。最后，`move` 沿等式 `q : fst Lδ = Lset (fst δ)`，把始域从典范呈现 `LsetS (fst δ) oδ` 搬到 `StageCountedCoded` 所要求的呈现。

```agda
            × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst δ ⟩)
            × InjL δ μ × InjL μ δ )
        → InjL Lδ δ
  build (μ , oμ , cμ , μ⊆δ , δ↪μ , μ↪δ) =
    move (LsetS (fst δ) oδ) Lδ δ δ (sym q) refl
```

最后还须证明壳计数定理要求的非有限性。若 `μ ∈ ω`，编码单射 `δ ↪ μ` 就会把非有限序数 `δ` 单射入有限序数，与 `δ ∉ ω` 矛盾；故 `μ ∉ ω`。有了这项最后前提，`At.result` 恰好给出从所选 `Lset δ` 呈现到 `δ` 的命题截断下的编码单射。

```agda
      (At.result δ oδ δ∉ω μ oμ cμ μ∉ω δ↪μ μ↪δ)
    where
    μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
    μ∉ω h = no-fin δ μ oδ δ∉ω oμ h δ↪μ
```