---
title: "後続基数を冪集合へ単射する"
module: L.GCH.SuccessorIntoPowerSet
lang: ja
site: "Bedrock"
description: "後続基数を冪集合へ単射する"
stage: "GCH の証明"
reading_order: 113
canonical: https://bedrock.institute/ja/L.GCH.SuccessorIntoPowerSet.html
html: L.GCH.SuccessorIntoPowerSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/SuccessorIntoPowerSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.ZFModel, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Axioms.Full, L.Cardinal, L.InjectionComposition, L.Coding.Model, L.Coding.Injection, L.GCH.BelowSuccessorCardinal, L.GCH.Assembly, L.DefinableInjection, L.GCH.OrderType]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.SuccessorIntoPowerSet.md, https://bedrock.institute/zh/L.GCH.SuccessorIntoPowerSet.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 後続基数を冪集合へ単射する

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

排中律の仮定は `ℓ-suc ℓ` のレベルに置かれる。集合と符号化されたグラフに関する必要な命題が、このレベルに属するためである。したがって、以下の古典的な比較はすべて、この一つのパラメータに遡れる。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_; ∃̇∈ )
import FOL.ZFModel
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; IsOrd; isL; isL-trans; isTransV; isPropIsTransV )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; SuccCardL )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; inclusion-coded; injl-trans; module Relation )
open import L.Coding.Model {ℓ} using ( svAt-out; domAt-in )
open import L.Coding.Injection {ℓ} lem using ( injAt-out )
open import L.GCH.BelowSuccessorCardinal {ℓ} lem using ( below-succ-injects )
open import L.GCH.Assembly {ℓ} lem using ( SuccIntoPower )
open import L.DefinableInjection {ℓ} lem using ( module Inj )
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
```

`L` の内部での Cantor の定理は、`𝒫 κ` から `κ` への内部的に符号化された単射を排除する。この章では、`κ` の後続基数 `δ` と、別に与えられた比較 `InjL (𝒫 κ) δ` から、逆向きの比較 `InjL δ (𝒫 κ)` を構成する。ここで `InjL a b` は、`a` から `b` への単射を符号化する `L` のグラフが存在することの命題的切り詰めである。証明では、`δ` 上の順序数の順序を与えられた単射に沿って `𝒫 κ` へ引き戻し、その順序を順序数 `μ` へ崩壊して、Cantor の障害から `μ` が `δ` に属しえないことを示す。

古典的推論は、明示的なパラメータ `lem` を通して導入される。順序数の三分法が証明中の目に見える場合分けを与え、ここで用いる分出定理と符号化された単射に関する結果も、同じ仮定のもとで具体化されている。したがって、この章の古典的な依存は一箇所に明記されている。

対角部分集合と後で用いる引き戻し順序は、ともに `L` の集合でなければならない。そこで、構成可能モデルで解釈される一階の論理式によって両者を記述する。ここで用意される構文は、所属・連言・否定と、これらの関係を表すために必要な有界または非有界の存在証人を表現できる。

引き戻し順序の整礎性は、その下降の各段階を周囲の累積階層における所属の一段階へ移し、そこで正則性を適用して証明する。続いて、構成可能な順序数についての事実により、順序数の下への所属から比較に必要な順序数構造を得る。

内部の大きさの比較には二つの層がある。`InjCode F a b` は特定の構成可能なグラフとその単射の法則を保持するが、`InjL a b` はそのような符号が存在するという命題的切り詰めだけを保持する。後続基数の最小性、符号化された包含、単射の合成により、大域的なグラフを取り出さずにこれらの比較を組み合わせられる。

先の二つの結果が最終的な比較を支える。後続基数 `δ` より真に小さい順序数はすべて、その基数 `κ` へ単射する。また、符号化された整列順序は構成可能な順序数へ崩壊でき、崩壊像への符号化写像と、そこから戻る符号化写像が得られる。第三の材料 `InjL (𝒫 κ) δ` は、この章の条件付き定理の仮定であり、後続基数の記録だけからは従わない。

以下では、第二成分が証明である依存対をいくつか同一視する。その証明成分は命題なので、底の集合の等しさだけで十分である。得られた同一視に沿って、所属やグラフについての事実を輸送できる。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

到達可能性の記録は、引き戻した順序に対する整礎再帰を表す。命題的切り詰めは、この章全体で単なる存在を表し、そこからの消去先は常に、空の型や別の `InjL` の主張のような命題である。

```agda
import Cubical.Induction.WellFounded as WF
open WF using ( Acc; acc; WellFounded )
```

正則性と推移性を適用するとき、底の集合の所属は周囲の階層で読む。この周囲の関係は、構成可能性の証明と組にされた要素どうしの所属とは区別しなければならない。

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

周囲の集合を `SV.S` と書く。順序数の底の集合どうしの逐点包含のように、累積階層そのものの対象を動く主張で、この台を用いる。

```agda
module SV = hPropView 𝒮ᵥ using ( S )
```

集合とその構成可能性の証明との組を `SL.S` と書く。内部の冪集合、後続基数の述語、符号化された単射の関係は、いずれもこの台の要素を引数に取る。

```agda
module SL = hPropView 𝒮ʟ using ( S; _∈ˢ_ )
```

`L` 上の ZF 構造が、その内部の冪集合を定める。その仕様は、`𝒫 κ` への所属を内部の部分集合関係と同一視し、そこでの量化は構成可能モデルの要素を動く。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ using ( isZFModel; module isZFModel; ℩-spec )
```

対象言語の論理式は、構成可能な集合からなる環境で評価される。絶対性が、その充足の主張と証明で用いる台の水準の述語とを結ぶ意味論的な読みを与える。

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

`SL.S` の要素は、底の集合と構成可能性の証明からなる。構成可能性は命題なので、底の集合の等しさを `SL.S` における等しさへ持ち上げられ、証明どうしの等しさを別に選ぶ必要はない。

```agda
S≡ : {x y : SL.S} → x .fst ≡ y .fst → x ≡ y
S≡ = Σ≡Prop (λ v → (isL v) .snd)
```

## 内部部分集合はモデルの冪集合に属する

最初の構成は、点ごとの内部包含をモデルの冪集合への所属へ変える。これは任意の構成可能集合 `κ` と `y` に適用できる。`y` の構成可能な要素がすべて `κ` に属するなら、`y` は `κ` の内部部分集合であり、したがって `𝒫 κ` に属する。

```agda
into-power :
    (zf : ModelL.isZFModel) (κ y : SL.S)
  → ((z : SL.S) → ⟨ z .fst ∈ˢ y .fst ⟩ → ⟨ z .fst ∈ˢ κ .fst ⟩)
  → ⟨ y .fst ∈ˢ (ModelL.isZFModel.𝒫 zf κ) .fst ⟩
into-power zf κ y sub =
```

冪集合の仕様は、`y` が `𝒫 κ` に属することと、点ごとの内部部分集合条件とが同値であると述べる。この同値性に沿って書き換えると、目標はちょうど与えられた包含の証明になる。

```agda
  subst ⟨_⟩ (sym (ModelL.℩-spec (hasPower κ) y)) sub
  where open ModelL.isZFModel zf using ( hasPower )
```

## L の内部での Cantor の対角線論法

ここで任意の構成可能集合 `κ` を固定し、そのモデル内の冪集合について内部の Cantor の障害を証明する。この部分では、`κ` が基数であることも無限であることも仮定しない。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module Cantor (zf : ModelL.isZFModel) (κ : SL.S) where
```

</summary>
<div class="submodule-fold-content">

対角線論法を通して、`𝒫 κ` は固定した `L` 上の ZF モデルが与える冪集合を意味する。したがって、その要素は、まさにこのモデルの内部で認識される部分集合である。

```agda
  open ModelL.isZFModel zf using ( 𝒫 )
```

対角の議論は、明示的に与えられた一つのグラフ `F` とその符号について展開される。後の主張はすべて、この固定されたグラフに関するものである。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
  module Diag (F : SL.S) (code : InjCode F (𝒫 κ) κ) where
```

</summary>
<div class="submodule-fold-content">

グラフの環境は、グラフと、それが全域的である冪集合とを対にする。

```agda
    γF : Vec SL.S 2
    γF = F ∷ 𝒫 κ ∷ []
```

符号の値域の条項は、グラフに記録されたすべての値が `κ` に属することを言う。

```agda
    ranF : (x y : SL.S) → Holds F x y → ⟨ y .fst ∈ κ .fst ⟩
    ranF = code .snd .snd .snd
```

全域性の条項は、`𝒫 κ` の各要素が `F` による何らかの値をもつことを述べる。値の証人は命題的切り詰めの内側に留まるので、ここでは存在だけが得られ、大域的に値を選ぶことはない。

```agda
    valF : (x : SL.S) → ⟨ x .fst ∈ (𝒫 κ) .fst ⟩
         → ∥ Σ[ y ∶ SL.S ] Holds F x y ∥₁
    valF = domAt-in zero (suc zero) γF (code .snd .fst)
```

単射性の条項は、値から入力を復元する。同じ記録された値をもつ二つの要素は、底の集合が等しくなる。

```agda
    injF : (y x x' : SL.S) → Holds F x y → Holds F x' y → x .fst ≡ x' .fst
    injF = injAt-out zero γF (code .snd .snd .fst)
```

対角の述語は、単に、冪集合のある要素 `A` で、記録された値が `ξ` に等しく、しかも `ξ` が `A` に属さないものが存在する、と言う。存在は切り詰められており、そのような集合は選ばれない。

```agda
    Diagonal : SL.S → Type (ℓ-suc ℓ)
    Diagonal ξ = ∥ Σ[ A ∶ SL.S ] ( ⟨ A .fst ∈ (𝒫 κ) .fst ⟩ × Holds F A ξ
                                 × (⟨ ξ .fst ∈ A .fst ⟩ → ⊥₀) ) ∥₁
```

適用のアトムの充足は、適用の符号化の妥当性により、文字どおり、台の水準でのグラフの成立である。

```agda
    private
      a1 : (ξ A : SL.S)
         → ⟨ (A ∷ ξ ∷ []) ⊨ appC F zero (suc zero) ⟩ ≡ Holds F A ξ
      a1 ξ A = cong ⟨_⟩ (appC-adequate F zero (suc zero) (A ∷ ξ ∷ []))
```

対角条件を定める論理式は、`𝒫 κ` の中から、`F` が対 `(A, ξ)` を記録し、かつ `ξ` が `A` に属さないような集合 `A` を探する。有界量化は、その証人が `κ` の内部部分集合であることを正確に記録する。続いて `κ` 上で分出を適用し、この条件を満たす `ξ∈κ` 全体の集合を作る。

```agda
    opaque
      φD : Formula SL.S 1
      φD = ∃̇∈ (con (𝒫 κ))
             (appC F zero (suc zero) ∧̇ ¬̇ (var (suc zero) ∈̇ var zero))
```

適用の符号化の妥当性により、`F` を `A` に適用する論理式のアトムは、意味論的な主張 `Holds F A ξ` と同一視される。この等式によって、以下の二方向で対角論理式と符号化されたグラフを相互に読み替えられる。

```agda
      φD-out : (ξ : SL.S) → ⟨ (ξ ∷ []) ⊨ φD ⟩ → Diagonal ξ
      φD-out ξ = map₁ (λ { (A , (mA , (h , n))) →
        A , mA , transport (a1 ξ A) h , (λ k → lower (n k)) })
```

逆に、`A ∈ 𝒫 κ`、グラフについての事実 `Holds F A ξ`、および `ξ ∉ A` の証明が与えられれば、対角論理式を充足できる。これらのデータは、論理式の有界存在量化に伴う命題的切り詰めの中にまとめられる。

```agda
      φD-in : (ξ A : SL.S) → ⟨ A .fst ∈ (𝒫 κ) .fst ⟩ → Holds F A ξ
            → (⟨ ξ .fst ∈ A .fst ⟩ → ⊥₀) → ⟨ (ξ ∷ []) ⊨ φD ⟩
      φD-in ξ A mA h n =
        ∣ A , (mA , (transport (sym (a1 ξ A)) h , (λ k → lift (n k)))) ∣₁
```

対角の集合は、この有界の論理式によって `κ` から分出される。

```agda
    D₀ : SL.S
    D₀ = ((hasSeparationL κ φD) .fst) .fst
```

その所属の仕様は、分出自身の読みである。対角の集合に属するとは、`κ` に属し、かつ対角の論理式を充足することの連言である。

```agda
    D₀-spec : (ξ : SL.S) → (ξ SL.∈ˢ D₀) ≡ ((ξ SL.∈ˢ κ) ⊓ ((ξ ∷ []) ⊨ φD))
    D₀-spec = ((hasSeparationL κ φD) .fst) .snd
```

対角の集合は内部の冪集合の要素である。逐点の読みが、そのすべてのモデルの要素が `κ` に属することを証明する。

```agda
    D₀∈𝒫κ : ⟨ D₀ .fst ∈ (𝒫 κ) .fst ⟩
    D₀∈𝒫κ = into-power zf κ D₀ (λ z h → (subst ⟨_⟩ (D₀-spec z) h) .fst)
```

矛盾を導くため、グラフが対角集合 `D₀` にある値 `ξ` を割り当てると仮定する。値域の条項から `ξ ∈ κ` が得られ、`D₀` の定義から `ξ ∈ D₀` と `ξ ∉ D₀` の両方が強制される。

```agda
    absurd : Σ[ ξ ∶ SL.S ] Holds F D₀ ξ → ⊥₀
    absurd (ξ , h₀) = out inside
      where
```

`ξ ∈ D₀` と仮定する。対角論理式は、命題的切り詰めのもとで、`F` が `A` を `ξ` へ送り、かつ `ξ ∉ A` となる集合 `A ∈ 𝒫 κ` を与える。`F` は `D₀` も `ξ` へ送るので、単射性により `A` と `D₀` の底の集合が同一視される。仮定した所属を `A` へ輸送すると、`ξ ∉ A` と矛盾する。

```agda
      out : ⟨ ξ .fst ∈ D₀ .fst ⟩ → ⊥₀
      out hm = rec₁ isProp⊥
        (λ { (A , _ , hA , n) →
          n (subst (λ w → ⟨ ξ .fst ∈ w ⟩) (injF ξ D₀ A h₀ hA) hm) })
        (φD-out ξ ((subst ⟨_⟩ (D₀-spec ξ) hm) .snd))
```

逆向きでは、先ほどの反証をデータとして用いる。値域の条項から `ξ ∈ κ` が得られる。`A = D₀` と取り、`F` が `D₀` を `ξ` へ送ることと、前段で証明した `ξ ∉ D₀` を使えば、対角論理式を証せる。したがって分出の仕様から `ξ ∈ D₀` が得られ、これにその反証を適用して矛盾を得る。

```agda
      inside : ⟨ ξ .fst ∈ D₀ .fst ⟩
      inside = subst ⟨_⟩ (sym (D₀-spec ξ))
        (ranF D₀ ξ h₀ , φD-in ξ D₀ D₀∈𝒫κ h₀ out)
```

</div>
</details>

この二つの半分が、冪集合から `κ` への内部の符号化された単射をすべて反証する。単射はグラフへ消去され、グラフの対角の集合における値が矛盾へ消去される。目標が空の型なので、どちらの消去も正当である。

```agda
  no-inj : InjL (𝒫 κ) κ → ⊥₀
  no-inj = rec₁ isProp⊥ step
    where
    step : Σ[ F ∶ SL.S ] InjCode F (𝒫 κ) κ → ⊥₀
    step (F , code) = rec₁ isProp⊥ D.absurd (D.valF D.D₀ D.D₀∈𝒫κ)
```

選んだグラフ `F` に対して、対角構成は内部部分集合 `D₀` と、そこに値を割り当てることが不可能であるという証明を与える。それでも全域性は値を割り当てるので、このグラフについて矛盾が完成する。

```agda
      where module D = Diag F code
```

</div>
</details>

## 冪集合を整列してその順序型を比較する

逆向きの比較を構成するため、`κ` の後続基数 `δ` と、仮定された単射 `𝒫 κ ↪ δ` を符号化する特定のグラフ `G` を固定する。このグラフは命題的切り詰めから得られる局所的な分岐の中でだけ利用でき、最終結果は再び `InjL` の主張になる。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module Build (zf : ModelL.isZFModel) (κ δ : SL.S) (sc : SuccCardL δ κ)
             (G : SL.S)
             (code : InjCode G (ModelL.isZFModel.𝒫 zf κ) δ) where
```

</summary>
<div class="submodule-fold-content">

ここで始域となる `𝒫 κ` も、固定した ZF モデルが定める内部の冪集合である。この構成で、それを底の集合の周囲の冪集合に置き換えることはない。

```agda
  open ModelL.isZFModel zf using ( 𝒫 )
```

後続の順序数性は、その記録の最初の成分である。

```agda
  ordδ : IsOrd (δ .fst)
  ordδ = sc .fst
```

冪集合が、比較の源として名付けられる。

```agda
  P : SL.S
  P = 𝒫 κ
```

グラフの環境は、グラフと冪集合を対にする。

```agda
  γG : Vec SL.S 2
  γG = G ∷ P ∷ []
```

符号の値域の条項は、すべての値が後続の中に着地することを言う。

```agda
  ranG : (x y : SL.S) → Holds G x y → ⟨ y .fst ∈ δ .fst ⟩
  ranG = code .snd .snd .snd
```

一価性は一つの固定した入力についての性質である。`G` が `G(x)=y` と `G(x)=y'` の両方を記録するなら、`y` と `y'` の底の集合は等しくなる。この一意性により、`x` の可能な値からなる型が命題になる。

```agda
  svG : (x y y' : SL.S) → Holds G x y → Holds G x y' → y .fst ≡ y' .fst
  svG = svAt-out zero γG (code .fst)
```

全域性は、各 `x ∈ P` に対して命題的に切り詰められた値の証人を与える。この時点では、値はまだ選ばれていない。すぐ後で一価性から可能な値のファイバーが命題であることを示し、この切り詰めから消去して局所的に値を読み出す。

```agda
  valG : (x : SL.S) → ⟨ x .fst ∈ P .fst ⟩ → ∥ Σ[ y ∶ SL.S ] Holds G x y ∥₁
  valG = domAt-in zero (suc zero) γG (code .snd .fst)
```

符号化された単射 `G` の単射性の条項は、値から始域の要素を復元する。二つの始域の要素が同じ記録値をもつなら、それらの底の集合は等しくなる。

```agda
  injG : (y x x' : SL.S) → Holds G x y → Holds G x' y → x .fst ≡ x' .fst
  injG = injAt-out zero γG (code .snd .snd .fst)
```

入力 `x` を固定すると、`G` のグラフが与える任意の二つの値は、一価性によって等しくなる。構成可能性の証明は命題なので、基礎にある値の等しさは証人全体の等しさへ持ち上がる。したがって、可能な値からなるファイバー自身が命題である。

```agda
  isPropVal : (x : SL.S) → isProp (Σ[ y ∶ SL.S ] Holds G x y)
  isPropVal x (y , h) (y' , h') =
    Σ≡Prop (λ w → (pr (x .fst) (w .fst) ∈ G .fst) .snd) (S≡ (svG x y y' h h'))
```

定義域の条項が最初に与える `G` の値は、命題的切り詰めの内側にある。直前に示した一意性によって行き先のファイバーは命題値になるので、切り詰めを除去し、その一意な値を以後の構成で使える。この段階で用いるのは一意性であり、一般の選択原理ではない。

```agda
  val : (x : SL.S) → ⟨ x .fst ∈ P .fst ⟩ → Σ[ y ∶ SL.S ] Holds G x y
  val x m = rec₁ (isPropVal x) (λ z → z) (valG x m)
```

`a` が `b` に先行するとは、両者が `P` に属し、`G(a)=x`、`G(b)=y`、`x∈y` を満たすグラフの値 `x` と `y` が命題的切り詰めのもとで存在することだと定める。命題的切り詰めは、適切な像が存在することだけを記録し、証人の選択は保持しない。

```agda
  Read : SL.S → SL.S → Type (ℓ-suc ℓ)
  Read a b = ∥ Σ[ x ∶ SL.S ] Σ[ y ∶ SL.S ]
               ( ⟨ a .fst ∈ P .fst ⟩ × ⟨ b .fst ∈ P .fst ⟩
               × Holds G a x × Holds G b y × ⟨ x .fst ∈ y .fst ⟩ ) ∥₁
```

この関係を対象言語で表すため、環境は `A`、`B` と、その像の候補 `x`、`y` を、`G` の二つの適用から読める位置に置く。これにより、一つの論理式で `G(A)=x`、`G(B)=y`、`x∈y` を同時に述べられる。

```agda
  private
    env5 : SL.S → SL.S → SL.S → SL.S → SL.S → Vec SL.S 5
    env5 p A B x y = y ∷ x ∷ B ∷ A ∷ p ∷ []
```

最初の妥当性の等式は、符号化された適用をグラフの主張 `Holds G A x` と同一視する。これは、対象言語の論理式と、符号化されたグラフが `A` を `x` へ送るという主張を結ぶ橋である。

```agda
    b1 : (p A B x y : SL.S)
       → ⟨ env5 p A B x y ⊨ appC G (suc (suc (suc zero))) (suc zero) ⟩
       ≡ Holds G A x
    b1 p A B x y = cong ⟨_⟩
      (appC-adequate G (suc (suc (suc zero))) (suc zero) (env5 p A B x y))
```

二つ目の妥当性の等式は、`B` と `y` について同じ変換を行う。二つの等式を合わせることで、引き戻した関係を、論理式の充足からも、`G` のグラフについての通常の主張からも証明できる。

```agda
    b2 : (p A B x y : SL.S)
       → ⟨ env5 p A B x y ⊨ appC G (suc (suc zero)) zero ⟩ ≡ Holds G B y
    b2 p A B x y = cong ⟨_⟩
      (appC-adequate G (suc (suc zero)) zero (env5 p A B x y))
```

定義する論理式は、まず二つの端点を内部冪集合に制限し、続いてそれらの像となる二つのモデル要素を量化する。二つの適用のアトムと、像の間の所属比較を合わせることで、`P` 上の関係の一階的な記述が得られ、関係の構成はその記述を `L` の集合として表す。

```agda
  private
    opaque
      φR : Formula SL.S 3
      φR = (var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ∃̇ (∃̇
        (appC G (suc (suc (suc zero))) (suc zero)
```

二つの存在束縛の内側で、残りの条項は、二つの証人がそれぞれ端点の `G` による像であり、最初の像が二つ目の像に属することを述べる。これはまさに、`δ` 上の所属順序を `G` に沿って引き戻したものである。

```agda
          ∧̇ (appC G (suc (suc zero)) zero ∧̇ (var (suc zero) ∈̇ var zero)))))
```

論理式を外向きに読むと、まず二つの像の証人が命題的切り詰めのもとに保たれる。次に、二つの妥当性の等式が符号化された適用をグラフの事実へ変え、`Read` の意味論的データ、すなわち端点の所属、二つの値、その間の所属比較をちょうど与える。

```agda
      read : (a b p : SL.S) → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ → Read a b
      read a b p (ma , mb , h) = rec₁ squash₁
        (λ { (x , hx) → map₁ (λ { (y , ha , hb , hxy) → x , y , ma , mb
          , transport (b1 p a b x y) ha , transport (b2 p a b x y) hb , hxy }) hx }) h
```

内向きの読み出しは、逆向きの妥当性の等式に沿って、それぞれのホスト側の事実を運び戻し、存在量化子と適用の枠を満たして、論理式の充足を再構築する。

```agda
      fill : (a b p : SL.S) → Read a b → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩
      fill a b p = rec₁ (((b ∷ a ∷ p ∷ []) ⊨ φR) .snd)
        (λ { (x , y , ma , mb , ha , hb , hxy) → ma , mb , ∣ x , ∣ y
          , transport (sym (b1 p a b x y)) ha
          , transport (sym (b2 p a b x y)) hb , hxy ∣₁ ∣₁ })
```

有界関係の構成は、この定義可能な述語を `L` にある実際の関係集合へ変える。上で示した二方向の読み替えにより、符号化された関係への所属は、`Read` が表す命題的に切り詰められた内容とちょうど一致する。

```agda
    module Pullback = Relation P P φR (λ a b → Read a b , squash₁) read fill
```

逆向きに読むときは、二つの妥当性の等式によって、グラフの事実 `Holds G A x` と `Holds G B y` を適用のアトムへ戻す。続いて `x` と `y` を二つの存在量化の証人としてまとめると、定義論理式の充足が再構成される。

```agda
  R : SL.S
  R = Pullback.rel
```

`R` の一つの関係項から、引き戻しを定義する命題的に切り詰められたデータを読み戻せる。すなわち、二つの端点は冪集合に属し、それぞれ `G` による像をもち、最初の像は二つ目の像に属する。

```agda
  R-out : (a b : SL.S) → Holds R a b → Read a b
  R-out = Pullback.pair-out
```

内向きの読み出しは、二つの端点の所属、`G` の像の二つの事実、そして像の間の所属から、関係の項目を作る。

```agda
  R-in : (a b x y : SL.S) → ⟨ a .fst ∈ P .fst ⟩ → ⟨ b .fst ∈ P .fst ⟩
       → Holds G a x → Holds G b y → ⟨ x .fst ∈ y .fst ⟩ → Holds R a b
  R-in a b x y ma mb ha hb hxy = Pullback.into a b ma mb ∣ x , y , ma , mb , ha , hb , hxy ∣₁
```

符号化された関係の各項目では、二つの端点がとも `P` に属する。証明は命題的切り詰めのもとにある証人を読み、像のデータを捨てて、二つの端点の所属だけを残す。その積は命題なので、この切り詰めの除去が許される。

```agda
  Rsub : (a b : SL.S) → Holds R a b
       → ⟨ a .fst ∈ P .fst ⟩ × ⟨ b .fst ∈ P .fst ⟩
  Rsub a b h = rec₁
    (isProp× ((a .fst ∈ P .fst) .snd) ((b .fst ∈ P .fst) .snd))
    (λ { (_ , _ , ma , mb , _) → ma , mb })
```

外向きの読み出しを適用すると、抽出に必要な証人が得られる。その切り詰めを除去できるのは、結論である二つの端点の所属命題の組もまた命題だからである。

```agda
    (R-out a b h)
```

順序型の構成は、`P` の要素を小さい提示領域 `Dom` で表す。関係 `a ≺ b` は、表された要素どうしが `R` で関係づけられるという符号化された事実をちょうど記録する。そこで以下では、添字上の引き戻し順序を調べ、のちにそれを崩壊できる。

```agda
  module OT = Code P R Rsub
    using ( Dom; Dom≡; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out
          ; module Conjuncts )
```

この領域の添字 `b` に対し、`v b` を、`b` が表す `P` の要素へ `G` が割り当てる一意な値とする。次に、これらの代表が `δ` より下の順序数であることを示す。

```agda
  v : OT.Dom → SL.S
  v b = (val (OT.up b) (OT.up-mem b)) .fst
```

選んだ値の第二成分は、対応するグラフの事実 `Holds G (up b) (v b)` を記録する。これは、代表どうしの比較を引き戻した関係の項目へ結びつける。

```agda
  v-holds : (b : OT.Dom) → Holds G (OT.up b) (v b)
  v-holds b = (val (OT.up b) (OT.up-mem b)) .snd
```

単射の符号の値域の条項により、`G` の各値は後続基数 `δ` に属する。したがって、すべての代表が一つの順序数の中にあり、そこで所属による比較と順序数の三分法を用いられる。

```agda
  v∈δ : (b : OT.Dom) → ⟨ (v b) .fst ∈ δ .fst ⟩
  v∈δ b = ranG (OT.up b) (v b) (v-holds b)
```

それぞれの `G` の値は順序数である。`δ` の順序数性から受け継がれる。

```agda
  ord-v : (b : OT.Dom) → IsOrd ((v b) .fst)
  ord-v b = mem-ord {A = δ .fst} ordδ ((v b) .fst) (v∈δ b)
```

前向きの比較は、引き戻された関係の一つの先行段階を、二つの代表順序数の間の所属へ移す。関係の項目を読むと二つの像の証人が得られ、`G` の一価性によって、それぞれが固定した値 `v a` と `v b` に同一視される。

```agda
  ≺-fwd : (a b : OT.Dom) → a OT.≺ b → ⟨ (v a) .fst ∈ (v b) .fst ⟩
  ≺-fwd a b k = rec₁ (((v a) .fst ∈ (v b) .fst) .snd)
    (λ { (x , y , _ , _ , ha , hb , hxy) →
      subst2 (λ s t → ⟨ s ∈ t ⟩)
        (svG (OT.up a) x (v a) ha (v-holds a))
```

二つの一価性の等式により、`R` から読み出した像の証人を、固定した代表 `v a` と `v b` にそれぞれ置き換える。`x∈y` を両方の等式に沿って輸送すると、必要な比較 `v a ∈ v b` が得られる。

```agda
        (svG (OT.up b) y (v b) hb (v-holds b)) hxy })
    (R-out (OT.up a) (OT.up b) (OT.≺-out a b k))
```

後ろ向きの比較は、二つの代表の順序数の所属から、引き戻された関係を構成する。二つのグラフの事実と、像の間の所属を、改めて導入することによるものである。

```agda
  ≺-bwd : (a b : OT.Dom) → ⟨ (v a) .fst ∈ (v b) .fst ⟩ → a OT.≺ b
  ≺-bwd a b h = OT.≺-in a b
    (R-in (OT.up a) (OT.up b) (v a) (v b)
      (OT.up-mem a) (OT.up-mem b) (v-holds a) (v-holds b) h)
```

整礎性を示すため、階層の要素 `u` を固定し、代表の値が `u` であるすべての領域の添字を考える。述語 `Pacc u` は、その各添字が引き戻し順序でアクセス可能であることを要求し、周囲の所属関係に関する帰納を準備する。

```agda
  private
    Pacc : V ℓ → Type (ℓ-suc ℓ)
    Pacc u = (b : OT.Dom) → (v b) .fst ≡ u → Acc OT._≺_ b
```

帰納のステップは、代表の順序数が `u` より厳密に下にある先行者のアクセス可能性を構成する。前向きの比較が所属を代表へ運び、帰納の仮定がそこでアクセス可能性を供給する。

```agda
    accStep : (u : V ℓ) → (∀ u' → ⟨ u' ∈ˢ u ⟩ → Pacc u') → Pacc u
    accStep u IH b e = acc (λ a k →
      IH ((v a) .fst) (subst (λ w → ⟨ (v a) .fst ∈ˢ w ⟩) e (≺-fwd a b k))
         a refl)
```

すべての階層の要素でのアクセス可能性は、周囲の階層の正則性の帰納で証明される。それは、所属の整礎性である。

```agda
    accAt : (u : V ℓ) → Pacc u
    accAt = WF.WFI.induction regularityV {P = Pacc} accStep
```

引き戻された順序の整礎性は、代表の順序数ごとのアクセス可能性から組み立てられる。

```agda
  wf : WellFounded OT._≺_
  wf b = accAt ((v b) .fst) b refl
```

引き戻された順序の推移性は、二つの前向きの比較を、順序数 `δ` の推移性を二つの代表の所属に適用して合成する。

```agda
  ≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
  ≺-trans {a} {b} {c} k k' = ≺-bwd a c
    (ordδ .snd ((v c) .fst) (v∈δ c) (≺-fwd a b k) (≺-fwd b c k'))
```

引き戻された順序の三分法は、`δ` にある代表値についての順序数の三分法から移される。任意の `a` と `b` に対して、`v a ∈ v b`、二つの値が等しい、`v b ∈ v a` のいずれかが成り立つ。

```agda
  tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
  tri a b = go (ord-tri ((v a) .fst) (ord-v a) ((v b) .fst) (ord-v b))
    where
    go : Tri ((v a) .fst) ((v b) .fst)
       → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
```

厳密に下の場合は、引き戻された比較を直接作る。等しい場合は、等しい代表の値に `G` の単射性を適用して、二つの定義域の要素を同一視する。厳密に上の場合は比較を逆向きにする。

```agda
    go (inl h)       = inl (≺-bwd a b h)
    go (inr (inl e)) = inr (inl (OT.Dom≡
      (injG (v a) (OT.up a) (OT.up b) (v-holds a)
        (subst (λ w → ⟨ pr (OT.↪ b) w ∈ G .fst ⟩) (sym e) (v-holds b)))))
    go (inr (inr h)) = inr (inr (≺-bwd b a h))
```

整礎性と推移性から、崩壊写像 `col` とその像 `otL` が得られる。三分法を加えると崩壊の単射性も従い、異なる領域の添字が同じ崩壊値をもつことはない。これらの事実は、崩壊の表と、あとでそれを逆向きに読むためのデータの両方を与える。

```agda
  module C = OT.Conjuncts wf ≺-trans
    using ( module Inj; col; col-ord; col-out; colTable; colTable-in
          ; colTable-pair; otL; otL-in; otL-out )
  module I = C.Inj tri using ( code; col-inj; module Inverse )
```

崩壊の表は、内部の冪集合 `P` からその崩壊像 `otL` への符号化された単射である。その特定の表と単射性の証明を命題的に切り詰めることで、内部の主張 `InjL P otL` が得られる。

```agda
  power-into-ot : InjL P C.otL
  power-into-ot = ∣ C.colTable , I.code ∣₁
```

崩壊像が順序数であることを示すには、像自身の推移性と、その各要素が推移的集合であることの両方が必要である。後者について、`otL` への所属から、命題的切り詰めのもとで、与えられた要素を崩壊値として提示する添字 `b` が得られる。

```agda
  ot-ord : IsOrd (C.otL .fst)
  ot-ord = tr , mem
    where
    mem : (x : V ℓ) → ⟨ x ∈ˢ C.otL .fst ⟩ → isTransV x
    mem x h = rec₁ (isPropIsTransV x)
```

各崩壊値 `col b` はすでに順序数だと分かっているので、推移的である。この推移性を等式 `col b = x` に沿って輸送すれば、像の任意の要素 `x` が推移的であることが従う。

```agda
      (λ { (b , e) → subst isTransV e (C.col-ord b .fst) })
      (C.otL-out x h)
```

残るのは、像自身が推移的であることである。`y∈x` と `x∈otL` が与えられると、`otL` の外向きの記述は、命題的切り詰めのもとで `x` をある崩壊値 `col b` として提示する。目標の所属 `y∈otL` は命題なので、この証人を局所的に使える。

```agda
    tr : isTransV (C.otL .fst)
    tr {x} {y} y∈x x∈ot =
      rec₁ ((y ∈ˢ C.otL .fst) .snd) outer (C.otL-out x x∈ot)
      where
      outer : Σ[ b ∶ OT.Dom ] (C.col b ≡ x) → ⟨ y ∈ˢ C.otL .fst ⟩
```

`x` を `col b` に置き換えると、`col b` への所属を述べる崩壊の等式から、再び命題的切り詰めのもとで、崩壊値が `y` である先行者 `r≺b` が得られる。この小さい崩壊値が、`y` を像へ戻すために必要な証人である。

```agda
      outer (b , e) = rec₁ ((y ∈ˢ C.otL .fst) .snd) inner
        (C.col-out b y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym e) y∈x))
        where
        inner : Σ[ r ∶ OT.Dom ] ((r OT.≺ b) × (C.col r ≡ y))
              → ⟨ y ∈ˢ C.otL .fst ⟩
```

先行者の崩壊がその等式に沿って `y` へ運ばれ、`y` を像の中に置くことで、推移性の証明が完成する。

```agda
        inner (r , _ , e2) =
          subst (λ w → ⟨ w ∈ˢ C.otL .fst ⟩) e2 (C.otL-in r)
```

階層の要素 `w` に対し、ファイバー `Fib w` は添字 `b` と等式 `col b = w` からなる。したがって、このファイバーの要素は、崩壊写像による `w` の原像そのものである。

```agda
  Fib : V ℓ → Type (ℓ-suc ℓ)
  Fib w = Σ[ b ∶ OT.Dom ] (C.col b ≡ w)
```

`col` の単射性により、各ファイバーは命題になる。`b` と `b'` がともに `w` へ崩壊するなら、それらの等式から `col b` と `col b'` が等しくなり、単射性によって添字も等しくなる。周囲の階層 `V ℓ` は集合なので、各等式型 `col b = w` は命題であり、その証明が新たな違いを生むこともない。

```agda
  isPropFib : (w : V ℓ) → isProp (Fib w)
  isPropFib w (b , e) (b' , e') =
    Σ≡Prop (λ _ → setIsSet _ _) (I.col-inj b b' (e ∙ sym e'))
```

所属 `w∈otL` が最初に与える原像の添字は、命題的切り詰めの内側にある。`Fib w` が命題であることを直前に示したので、この切り詰めを除去し、崩壊値が `w` である一意な添字を取り出せる。

```agda
  fib : (w : V ℓ) → ⟨ w ∈ˢ C.otL .fst ⟩ → Fib w
  fib w h = rec₁ (isPropFib w) (λ z → z) (C.otL-out w h)
```

いま得た一意な原像により、崩壊の表を `otL` 全体で逆向きに読める。その添字が表すもとの要素は `P` に属するので、逆向きの構成は `L` にあるグラフを作り、とくに以下で用いる内部の符号化された単射 `Back.injL : InjL otL P` を与える。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
  module Back where
```

</summary>
<div class="submodule-fold-content">

```agda
    open I.Inverse C.otL P (λ w mw → fib (w .fst) mw)
      (λ w mw → OT.up-mem (fib (w .fst) mw .fst)) public
      using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )
```

</div>
</details>

崩壊順序数 `otL` を `μ` と書く。順序数の三分法によって `μ` と後続基数 `δ` を比較する。補助関数 `from-sub` は、等しい場合と `δ∈μ` の場合に共通する構成を取り出す。`δ` のすべての要素が `μ` にも属するなら、必要な `InjL δ P` を作る。

```agda
  result : InjL δ P
  result = go (ord-tri (C.otL .fst) ot-ord (δ .fst) ordδ)
    where
    from-sub : ((z : SV.S) → ⟨ z ∈ˢ δ .fst ⟩ → ⟨ z ∈ˢ C.otL .fst ⟩)
             → InjL δ P
```

包含の符号が、部分集合の事実を、`δ` から崩壊の像への符号化された単射としてまとめ、逆崩壊の単射がそれを冪集合の中へ合成する。

```agda
    from-sub sub =
      injl-trans δ C.otL P (inclusion-coded δ C.otL sub) Back.injL
```

三分法では、まず `μ∈δ` の場合を考える。この場合、`below-succ-injects` は後続基数の事実を用いて `InjL μ κ` を与える。これを `InjL P μ` と合成すると `InjL P κ` が得られ、内部の Cantor の定理に反する。したがって排除されるのは、崩壊順序数が `δ` より真に小さい場合だけである。

```agda
    go : Tri (C.otL .fst) (δ .fst) → InjL δ P
    go (inl ot∈δ)       = ⊥₀-rec (Cantor.no-inj zf κ
      (injl-trans P C.otL κ power-into-ot
        (below-succ-injects κ δ sc C.otL ot-ord ot∈δ)))
    go (inr (inl e))    =
```

残る二つの場合は、どちらも `from-sub` に必要な包含を与える。`μ=δ` なら、等式に沿う輸送によって、`δ` への各所属が `μ` への所属になる。`δ∈μ` なら、順序数 `μ` の推移性から同じ包含 `δ⊆μ` が得られる。いずれの場合も、この包含を単射として符号化し、逆崩壊の単射と合成することで `InjL δ P` を得る。

```agda
      from-sub (λ z h → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) h)
    go (inr (inr δ∈ot)) =
      from-sub (λ z h → ot-ord .fst h δ∈ot)
```

</div>
</details>

## 後続基数から冪集合へ到達する

この定理は、後続基数の証人 `sc` と、命題的に切り詰められた単射 `InjL (𝒫 κ) δ` を受け取る。目標 `InjL δ (𝒫 κ)` 自身が命題なので、特定のグラフ `G` を調べられるのは局所的な分岐の中だけである。追加の仮定 `κ∉ω` は `SuccIntoPower` の主張に現れるが、この証明では使われない。GCH の組み立てでは、`succCardExists` は命題的切り詰めのもとで `δ` とその証人 `sc` だけを与える。`power-into-succ` が別に `pis : InjL (𝒫 κ) δ` を構成し、それを `succ-into-power` に渡す。得られる結論が記録するのは、二方向の符号化された単射が命題的切り詰めのもとで存在することだけである。どちらのグラフも選ばず、全単射、集合の等しさ、基数の等式も与えない。

```agda
succ-into-power : (zf : ModelL.isZFModel) → SuccIntoPower zf
succ-into-power zf κ δ κ∉ω sc =
  rec₁ squash₁ (λ { (G , code) → Build.result zf κ δ sc G code })
```