---
title: "GCH の議論に必要な十分な段階"
module: L.GCH.AdequateStages
lang: ja
site: "Bedrock"
description: "GCH の議論に必要な十分な段階"
stage: "GCH の証明"
reading_order: 102
canonical: https://bedrock.institute/ja/L.GCH.AdequateStages.html
html: L.GCH.AdequateStages.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/AdequateStages.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Stage, L.Hierarchy, L.Axioms.Basic, L.Coding.CodeSet, L.Definability, L.Coding.EnvironmentTower, L.Coding.SatisfactionGraphSet]
routes: [gch-descriptions]
translations: [https://bedrock.institute/en/L.GCH.AdequateStages.md, https://bedrock.institute/zh/L.GCH.AdequateStages.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# GCH の議論に必要な十分な段階

凝縮で用いる内部記述には、四つの証人集合が同時に存在する必要があります。この章では、順序数添字が十分であるための条件を定め、任意の順序数より上にその条件を満たす添字 `γ` を構成します。さらに、各要素がより小さい十分な添字によって局所的に覆われる添字 `λ` を構成します。対応する構成可能段階は `Lset γ` と `Lset λ` です。十分な段階は、GCH の議論に合わせた四項目の閉包条件を表す本書固有の用語であり、通常の admissible 順序数ではありません。

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

この章のすべての構成は、一つの明示的な排中律の実例に相対しています。この仮定は誕生段階と符号化された証人の構成を通して議論に入りますが、選択関数を与えるものではありません。とくに、後で合併への所属から得る存在は、命題的切り詰めの中にとどまります。

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

宇宙レベル `ℓ` と、レベル `ℓ-suc ℓ` の命題に対する排中律を固定します。以下で構成する十分な添字と、それらに対応する段階は、この一つの古典的仮定に依存します。

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

この構成は周囲の累積階層 `V ℓ` の中で行われます。ここで `c`、`γ`、そして後の `λ` は順序数の添字であり、`Lset c`、`Lset γ`、`Lset λ` がそれぞれにより添字づけられた構成可能段階です。合併は周囲の階層にある順序数添字の間で作られます。恒真論理式を使うのは最後だけで、構成可能段階全体がその後続段階の要素になることを示します。

```agda
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` の単調性を使います。別の順序数に関する事実により、順序数の要素、その後続、そして途中で使う共通上界も順序数であることが保証されます。したがって上界の議論が扱うのは添字であり、その結論によって証人集合が一つの段階に入ります。

```agda
  ( 𝒮ʟ; 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` に結びつく四つの構成可能集合、すなわち内部の階層表、すべての論理式符号の集合、一様な充足関係のグラフ、環境の塔が必要です。妥当性はこの四つを一つの後の構成可能段階にまとめて入れ、一つの有界な記述がそこでそれらを量化できるようにします。

```agda
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 )
```

所属の主張と、それらから組み立てる証人条件はいずれも命題です。このことは、合併の要素から、それを含む族の要素について命題的に切り詰められた情報しか得られない場面で重要です。その情報は命題へ消去できますが、特定の添字を選んで保持することはできません。

```agda
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 )
```

累積階層の各集合には小さな提示があり、小さな添字型からそのすべての要素への写像が与えられます。この提示により、次の上界構成は順序数の全要素にわたって動けます。逆に、族の合併への所属から族の添字が得られるのは命題的切り詰めの中だけです。この違いが、以下の可算鎖の議論で本質的に使われます。

```agda
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 ℓ` における所属であり、次に導入する構成可能な台の内部の所属とは区別しなければなりません。

```agda
open hPropStructure 𝒮ᵥ
```

構成可能な台 `CS.S` の要素は、周囲の集合と、それが構成可能であることの証拠をひとまとめにします。したがって以下の四つの証人は、まず `CS.S` の要素として構成されます。その第一射影が、後の `Lset` への所属を示すべき実際の周囲の集合です。

```agda
module CS = hPropStructure 𝒮ʟ using (S)
```

## 十分な段階が含む四つの証人

証人のモジュールは、順序数 `c` と、それが順序数であることの証明を固定します。

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

構成可能段階 `Lset c` を台 `A` としてまとめます。この台から、階層表、論理式符号の集合、充足関係のグラフ、環境の塔という四つの証人をそれぞれ構成します。

```agda
  A : CS.S
  A = LsetS c oc
```

順序数添字 `c` 自身も構成可能です。`ord∈Lset-suc` が `c` を `Lset (sucV c)` に入れ、順序数で添字づけられた構成可能段階への所属から、必要な構成可能性の証拠 `cL` が得られます。

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

最初の証人は `c` における内部の階層表です。これは `L` の内部で、順序数添字が `c` より下にある構成可能段階を記録します。

```agda
  hier : CS.S
  hier = hierL c cL oc
```

第二の証人は、段階の台の上のすべての論理式符号からなる集合です。これらの符号は、後の階層記述で使われます。

```agda
  codes : CS.S
  codes = AllCodes A
```

一様な充足の表の順序対のグラフが第三の証人です。それぞれのキーに割り当てられた値を記録します。

```agda
  table : CS.S
  table = SatGraph.pairs A
```

環境の塔が第四の証人です。すべての有限の長さの環境を集めます。

```agda
  tower : CS.S
  tower = Tower.tower A
```

順序数である段階の添字 `c` に対し、証人述語は、いま構成した四つの基礎となる集合が一つの共通の容器 `K` に属することを要求します。証明 `oc : IsOrd c` を量化するため、特定の順序数性の証明を選んで保持しません。後では、より大きな順序数添字 `γ` に対する `Lset γ` を `K` とします。

```agda
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 ⟩
```

四つ目の所属が証人の述語を完成させます。環境の塔も同じ容器の中にあります。

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

証人述語は命題です。`c` が順序数であることの各証明に対し、その結論は四つの所属命題の積です。また、値がすべて命題である依存関数も命題です。この命題性により、後では命題的に切り詰められた鎖の添字から `Witnesses` へ直接消去でき、その添字をデータとして選ぶ必要がありません。

```agda
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 γ` です。

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

最後の条項で、この構成の二つの層面が結びつきます。前提 `c ∈ γ` は順序数添字どうしの所属であり、結論は `c` に結びつく四つの集合を構成可能段階 `Lset γ` に入れます。

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

四つの欄が、これからの議論のために名付けられます。順序数性・後続の閉性・無限順序数の所属・そして証人の節です。

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

## 任意の順序数より上に十分な段階を構成する

集合 `α` のすべての要素にわたって上界を取るため、その小さな提示 `⟪ α ⟫` を使います。写像 `ι α` は、各提示添字を、それが名指す周囲の集合へ送ります。この記法自体は、この時点で `α` を順序数とは仮定しません。順序数性は、名指された各要素が順序数であることを構成が示す段階で用いられます。

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

提示された索引はどれも、小さな所属と周囲の所属の橋を通して、順序数の一つの要素を名指します。

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

順序数の推移性は一度だけまとめられます。順序数の内側でつらなった二つの所属は、その順序数への一つの所属になります。

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

順序数添字 `α` から出発し、一回の上界構成で、より大きな順序数添字 `β` を作ります。この一回で、`α` の要素から生じるすべての要請、すなわちそれらの後続と、四つの証人集合の誕生段階の添字を満たします。しかし、`β` に新たに加わった要素について同じ要請をまだ満たしていないので、この時点で `β` が十分であるとは主張しません。

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

まとめられた各構成可能集合 `s : CS.S` には、誕生段階の添字 `stage (fst s) (snd s)` があります。この補助式は、`α` の提示された一要素という文脈の中で、この操作を記録します。得られる添字は証人集合 `s` に依存し、周囲の引数は、その証人がどの要素について作られたかを記録します。

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

`α` の提示されたすべての要素は順序数です。順序数の要素は順序数だからです。

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

`st` を四つの証人構成にそれぞれ適用すると、誕生段階の添字からなる四つの族が得られます。次の共通上界は、これら四つの族を厳密に上から抑える必要があります。

```agda
    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` を、証人の基礎となる集合とその構成可能性の証拠に適用して得られます。

```agda
    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)` 自身を上から抑えます。これらは順序数添字の間の上界であり、五つ目の族は誕生段階の族ではありません。

```agda
    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` は四つの証人上界をそれぞれまとめます。最小の上界であるとは主張しません。これらの操作が与えるのは、必要な所属証明を伴う厳密な共通上界です。

```agda
    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)
```

最後の二項上界は、後者、`α`、`ω` を担う枝と、四種類の誕生段階の上界を担う枝とを合わせます。したがって、その第一成分は六種類の要請すべてを同時に厳密に上から抑えます。

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

最終上界の第一成分を、新しい順序数添字 `β` とします。これは `V ℓ` の中の添字であり、証人を収める構成可能段階は `Lset β` です。

```agda
  β : V ℓ
  β = b11 .fst
```

最終の上界は順序数です。二項の上界の操作によって順序数から作られたからです。

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

最後の合成に供給された二つの部分的な上界は、最終の上界の下にあります。

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

`β` は推移的なので、厳密な所属を上界の木に沿って下へ伝えられます。`b9 ∈ β` から、後続の上界 `b5 ∈ β` と、`α` および `ω` の共通上界 `b6 ∈ β` が得られます。また `b10 ∈ β` から、まず `b7 ∈ β` が得られます。

```agda
    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` も `β` に属します。同じ推移性の議論を繰り返せば、残る各証人上界も `β` に入ります。

```agda
    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` の下で同じ位置にあるので、次の行でこの対称な議論が完結します。

```agda
    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 ∈ β` が得られます。これで、四つの誕生段階の上界すべてが、共通の順序数添字 `β` に厳密に属することが分かりました。

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

`b6` を通る枝は、出発点の順序数添字も保ちます。`α ∈ b6` と `b6 ∈ β` から、推移性により `α ∈ β` が得られます。

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

同じ枝は `ω` も保ちます。`ω ∈ b6` に `b6 ∈ β` をつなぐと、後で必要となる `ω ∈ β` が得られます。

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

`x ∈ α` ならば、提示のファイバーから、`ι α m ≡ x` を満たす添字 `m` が得られます。五つ目の共通上界は `sucV (ι α m)` を含み、`b5 ∈ β` を経て、それが `β` に属することが分かります。最後にファイバーの等式に沿って置換し、`sucV x ∈ β` を得ます。したがって、この一回の構成が示す後続閉包は `α` の要素に対するものだけであり、一回の上界構成に必要な結論と正確に一致します。

```agda
  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` の提示添字を同定するファイバーは命題値だからです。

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

共通の順序数上界 `β` は、四種類の証人の出生段階の添字をすべて厳密に上から押さえるように構成されています。ここから、その証人自身を構成可能段階 `Lset β` に入れます。

```agda
  private
```

四つの証人構成の一つ `f` と、`α` の要素を呈示する添字 `m` を固定します。対応する証人は `Lset (st f m)` に現れ、その出生添字は記録された上界 `b.fst` に属し、さらに `b.fst` は最終上界 `β` に属します。着地の補題は、ここから得られる `Lset β` への所属をまとめます。

```agda
    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 β` へ運びます。どちらの移動も、対応する順序数添字どうしの厳密な所属に基づきます。

```agda
      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` と同一視できます。

```agda
    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)` の四成分がすべて得られ、その結果は特定の順序数性証明に依存しません。

```agda
            (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` の四つの証人が得られます。ここでは命題的切り詰めの除去も選択も行いません。

```agda
  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` から始まります。合併そのものには単調性を仮定せず、後の二つの適用で各項が次の項に属することを別に証明します。

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

累積階層の合併は、周囲の宇宙レベルにある小さな添字型を要求します。`ℕ` を `Lift ℕ` に替えても変わるのは宇宙での位置だけで、`F (lift n)` は依然として順序数 `ch n` です。

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

この順序数族の集合論的な合併を、順序数添字 `γ` と書きます。この時点で `γ` は周囲の累積階層の集合であり、対応する構成可能段階は `Lset γ` です。

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

任意の順序数族の集合論的合併は、再び順序数です。この事実を `F` に適用して `IsOrd γ` を得ます。ここでは自然数添字の順序や共終性に関する性質を使いません。

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

内向きの読み出しが、列のそれぞれの項目のすべての要素を、合併の中に受け入れます。

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

外向きの読み出しは、切り詰めのもとで、合併の任意の要素を含む列の項目を復元します。切り詰められた添字は、命題の中だけで消費されます。

```agda
  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` を繰り返し、得られた順序数添字の合併を取ります。

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

最初の上界は、出発順序数 `p` と順序数 `ω` の両方を厳密に含む順序数です。これにより、最終的な合併まで保つべき二つの所属が直ちに得られます。

```agda
  private
    base = bound2 p ω op ω-ord
```

第零の順序数は最初の共通上界です。その後は各順序数を直前の項に `Bound1` を適用して作るので、`ch n` の要素から生じる義務は `ch (suc n)` で満たされます。一回の構成だけで、その結果自身の全要素について十分になるとは主張していません。

```agda
  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)
```

ここで、先の合併構成をこれらの順序数添字に適用します。内向きの写像は既知の所属を合併へ送り、外向きの写像は任意の要素を含む項を命題的切り詰めのもとでのみ位置づけます。

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

これらの順序数添字の合併を `γ` とします。一段階の遅れは合併によって吸収されます。ある項に現れた要素について、その後者と四つの証人集合は後の項で処理されます。最終的に証人が属すべき先は添字 `γ` 自身ではなく、`Lset γ` です。

```agda
  γ : V ℓ
  γ = C.γ
```

各 `ch n` が順序数なので、その集合論的合併 `γ` も順序数です。ここで得られるのは `IsOrd γ` だけであり、`Adequate γ` の閉性と証人の成分は以下で別に証明します。

```agda
  oγ : IsOrd γ
  oγ = C.oγ
```

列のそれぞれの項目は、その後続の項目より厳密に下にあります。一段階の上界の所属の条項によるものです。

```agda
  private
    up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
    up n = Bound1.α∈β (ch n .fst) (ch n .snd)
```

順序数添字 `ch n` 自身を合併 `γ` に入れるには、まず `ch n ∈ ch (suc n)` を使い、ついで `ch (suc n)` の各要素を合併へ入れます。この事実が、後で `Lset` の単調性に必要な添字の比較を与えます。

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

基底の上界はすでに `p` を含みます。これは列の第零項なので、合併の内向きの写像がこの所属を保ち、`p ∈ γ` を与えます。

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

同じ内向きの写像が `ω ∈ ch 0` を `ω ∈ γ` へ送ります。これが `Adequate γ` に必要な所属の成分です。

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

`x ∈ γ` が与えられると、外向きの写像は `x ∈ ch n` を満たす添字 `n` の命題的に切り詰められた存在だけを与えます。切り詰めの各分岐では、次の `Bound1` が `sucV x` を `ch (suc n)` に入れ、そこから `γ` に入れます。目標の所属 `sucV x ∈ γ` は命題なので、各分岐を再びまとめられます。特定の `n` が命題的切り詰めの外へ取り出されることはありません。

```agda
  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 ∈ γ` に対しても、外向きの写像が与えるのは `c ∈ ch n` を満たす `n` の命題的に切り詰められた存在だけです。各分岐では、一段階の上界構成が四つの証人を `Lset (ch (suc n))` に用意し、`ch (suc n) ∈ γ` に沿う `Lset-mono` がそれらを `Lset γ` へ運びます。`Witnesses (Lset γ) c` は命題なので、得られた結果を命題的切り詰めから除去できます。

```agda
  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)` から添字 `γ` への構成可能階層の単調性を表します。これを階層表、コード集合、充足関係のグラフ、環境の塔にそれぞれ適用して、四成分の証人を完成します。

```agda
      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 γ` に入れることです。後で使う妥当性の内容は、この四項目に尽きます。

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

この定理は順序数添字 `γ` を明示的に返し、`p ∈ γ` と `Adequate γ` を添えます。外側の依存対は切り詰められていないので、後の議論はこの `γ` を名指せます。ただし、それが最小であることも、`p + ω` のような標準的順序数演算で得られることも証明していません。

```agda
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` を含みますが、命題的切り詰めは特定の `γ` も最小の `γ` も保持しません。

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

順序数 `α` より上にこの強化された十分な段階を作るため、`adequate-above` をもう一度反復します。今度は自然数列の各項がすでに十分な順序数添字なので、その項自身を後で局所的な十分な証人として使えます。

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

第零項は `adequate-above α oα` が明示的に返す順序数添字です。この添字は十分であり、出発順序数 `α` を厳密に含みます。これらの事実は後で使えるよう項とともに保持されます。

```agda
  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)` が得られます。この定理はそのような次の添字を明示的に与えますが、最小性は主張しません。

```agda
    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 )
```

この十分な順序数添字の列に合併構成を適用します。先ほどと同様、合併の要素をある項に位置づけられるのは命題的切り詰めのもとだけです。

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

これらの順序数添字の合併を、コードでは `lam`、本文では `λ` と書きます。以下で示すのは、順序数添字 `λ` が `Adequate λ` と `Superadequate λ` の両方を満たすことです。対応する構成可能段階 `Lset λ` は、証人の条項でのみ使われます。

```agda
  lam : V ℓ
  lam = U.γ
```

各 `ch n` が順序数なので、その集合論的合併 `λ` も順序数です。この議論から、より強い極限性、正則性、基数としての性質は導かれません。

```agda
  olam : IsOrd lam
  olam = U.oγ
```

列のそれぞれの項目は、その後続の項目より厳密に下にあります。`adequate-above` が産出する厳密な所属によるものです。

```agda
  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 ∈ λ` が得られます。したがって、列にある各十分な添字自身が最終的な順序数添字 `λ` の要素として利用できます。

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

第零の十分な添字は `α` を厳密に含み、しかも合併を構成する集合の一つです。したがって `α ∈ λ` が従います。

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

`x ∈ λ` が与えられると、外向きの写像が与えるのは `x ∈ ch n` を満たす `n` の命題的に切り詰められた存在だけです。各分岐では、その項の妥当性から `sucV x ∈ ch n` が得られ、内向きの写像が `sucV x ∈ λ` を与えます。目標は所属命題なので、`n` を保持せずに結果を命題的切り詰めから除去できます。

```agda
  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 λ` に必要な所属 `ω ∈ λ` へ送ります。

```agda
  ω∈λ : ⟨ ω ∈ lam ⟩
  ω∈λ = U.into zero ω (Adequate.ω∈ (ch zero .fst) (ch zero .snd .snd))
```

`c ∈ λ` に対し、外向きの写像が与えるのは `c ∈ ch n` を満たす `n` の命題的に切り詰められた存在だけです。各分岐では、`ch n` の妥当性が四つの証人を `Lset (ch n)` に与え、`ch n ∈ λ` に沿う単調性がそれらを `Lset λ` へ運びます。`Witnesses (Lset λ) c` は命題なので、命題的切り詰めから正当に除去できます。

```agda
  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 λ` へ移ります。

```agda
        , ( 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 λ` に関するモデル理論的な主張ではありません。

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

`d ∈ λ` に対し、外向きの写像が与えるのは `d ∈ ch n` を満たす `n` の命題的に切り詰められた存在だけです。その切り詰めの内部で `γ = ch n` と置けば、この添字は `λ` に属し、`d` を含み、十分です。結果は切り詰められたままなので、選択関数 `d ↦ γ` は定義されません。

```agda
  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 λ` の証明を添えます。`λ` 自身はデータとして使えますが、その各要素に保証される局所的な十分な添字は命題的切り詰めのもとにあります。最小の局所添字も大域的な選択族も得られません。

```agda
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 β` が次の構成可能段階に属することであり、一つの段階が別の段階に要素ごとに含まれることとは異なる主張です。

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