---
title: "無限構成可能段階をその添字へ単射する"
module: L.GCH.StageInjection
lang: ja
site: "Bedrock"
description: "無限構成可能段階をその添字へ単射する"
stage: "GCH の証明"
reading_order: 118
canonical: https://bedrock.institute/ja/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/zh/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` の上に、なお `λ` に属する十分な段階 `γ` が単に存在することを述べます。このような中間の十分な段階が、包の計数と凝縮に必要な局所的な反映と閉性を与えます。

```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` とします。これは `δ` と、それより小さいすべての順序数を含み、`δ` が順序数なので推移的です。これらの性質を用いて、後で崩壊が `δ` を固定することを示します。

```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 δ↪μ
```