---
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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 後続基数を冪集合へ単射する

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

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

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

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

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

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

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

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_; ∃̇∈ )
import FOL.ZFModel
import FOL.Absoluteness
```

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

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

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

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

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

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

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

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

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

```agda
import Cubical.Induction.WellFounded as WF
open WF using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

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

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

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

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

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

```agda
module SL = hPropStructure 𝒮ʟ 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} → fst x ≡ fst y → x ≡ y
S≡ = Σ≡Prop (λ v → snd (isL v))
```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
    valF : (x : SL.S) → ⟨ fst x ∈ 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 → fst x ≡ fst x'
    injF = injAt-out zero γF (code .snd .snd .fst)
```

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

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

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

```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 ξ = PT.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) → ⟨ fst A ∈ fst (𝒫 κ) ⟩ → Holds F A ξ
            → (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) → ⟨ (ξ ∷ []) ⊨ φD ⟩
      φD-in ξ A mA h n =
        ∣ A , (mA , (transport (sym (a1 ξ A)) h , (λ k → lift (n k)))) ∣₁
```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
  ranG : (x y : SL.S) → Holds G x y → ⟨ fst y ∈ 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' → fst y ≡ fst y'
  svG = svAt-out zero γG (code .fst)
```

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

```agda
  valG : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → ∥ Σ[ 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 → fst x ≡ fst x'
  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 → snd (pr (fst x) (fst w) ∈ fst G)) (S≡ (svG x y y' h h'))
```

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

```agda
  val : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → Σ[ y ∈ SL.S ] Holds G x y
  val x m = PT.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 ]
               ( ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩
               × Holds G a x × Holds G b y × ⟨ fst x ∈ fst y ⟩ ) ∥₁
```

この関係を対象言語で表すため、環境は `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 → 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) = PT.rec squash₁
        (λ { (x , hx) → PT.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 = PT.rec (snd ((b ∷ a ∷ p ∷ []) ⊨ φR))
        (λ { (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) → ⟨ fst a ∈ fst P ⟩ → ⟨ fst b ∈ fst P ⟩
       → Holds G a x → Holds G b y → ⟨ fst x ∈ fst y ⟩ → 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
       → ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩
  Rsub a b h = PT.rec
    (isProp× (snd (fst a ∈ fst P)) (snd (fst b ∈ fst P)))
    (λ { (_ , _ , 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 = fst (val (OT.up b) (OT.up-mem b))
```

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

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

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

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

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

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

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

```agda
  ≺-fwd : (a b : OT.Dom) → a OT.≺ b → ⟨ fst (v a) ∈ fst (v b) ⟩
  ≺-fwd a b k = PT.rec (snd (fst (v a) ∈ fst (v b)))
    (λ { (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) → ⟨ fst (v a) ∈ fst (v b) ⟩ → 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) → fst (v b) ≡ 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 (fst (v a)) (subst (λ w → ⟨ fst (v a) ∈ˢ 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 (fst (v b)) 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 (fst (v c)) (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 (fst (v a)) (ord-v a) (fst (v b)) (ord-v b))
    where
    go : Tri (fst (v a)) (fst (v b))
       → (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 ∈ fst G ⟩) (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 (fst C.otL)
  ot-ord = tr , mem
    where
    mem : (x : V ℓ) → ⟨ x ∈ˢ fst C.otL ⟩ → isTransV x
    mem x h = PT.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 (fst C.otL)
    tr {x} {y} y∈x x∈ot =
      PT.rec (snd (y ∈ˢ fst C.otL)) outer (C.otL-out x x∈ot)
      where
      outer : Σ[ b ∈ OT.Dom ] (C.col b ≡ x) → ⟨ y ∈ˢ fst C.otL ⟩
```

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

```agda
      outer (b , e) = PT.rec (snd (y ∈ˢ fst C.otL)) 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 ∈ˢ fst C.otL ⟩
```

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

```agda
        inner (r , _ , e2) =
          subst (λ w → ⟨ w ∈ˢ fst C.otL ⟩) 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 ∈ˢ fst C.otL ⟩ → Fib w
  fib w h = PT.rec (isPropFib w) (λ z → z) (C.otL-out w h)
```

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

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

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

```agda
  result : InjL δ P
  result = go (ord-tri (fst C.otL) ot-ord (fst δ) ordδ)
    where
    from-sub : ((z : SV.S) → ⟨ z ∈ˢ fst δ ⟩ → ⟨ z ∈ˢ fst C.otL ⟩)
             → 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 (fst C.otL) (fst δ) → InjL δ P
    go (inl ot∈δ)       = Empty.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)
```

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

この定理は、後続基数の証人 `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 =
  PT.rec squash₁ (λ { (G , code) → Build.result zf κ δ sc G code })
```