---
title: "L の無限基数における平方律"
module: L.GCH.CardinalSquareLaw
lang: ja
site: "Bedrock"
description: "L の無限基数における平方律"
stage: "GCH の証明"
reading_order: 111
canonical: https://bedrock.institute/ja/L.GCH.CardinalSquareLaw.html
html: L.GCH.CardinalSquareLaw.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CardinalSquareLaw.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, L.Choice.FirstIntersectionStage, V.Model, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Cardinal, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.OrderType]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.CardinalSquareLaw.md, https://bedrock.institute/zh/L.GCH.CardinalSquareLaw.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# L の無限基数における平方律

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

宇宙レベル `ℓ` を固定し、`lem : LEM (ℓ-suc ℓ)` を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj )
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord; #∈ω; ω-mem-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
import L.Ordinal.SquareLaw {ℓ} lem as SQ
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( lt; eq; gt ) renaming ( Tri to TriW )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt )
open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate )
open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract; module Small )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL; _↪_ )
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.OrderType {ℓ} lem using ( Holds; module Code )
open import L.InjectionComposition {ℓ} lem
  using ( appC; appC-adequate; ω-limit; finite-excl-ω )
open import L.InjectionComposition {ℓ} lem public using ( module Relation )
```

`L` の無限基数 `κ` に対し、その要素の順序対からなる集合は、`L` の内部での符号化された単射によって `κ` 自身へ注入される。本章はこの単射を構成する。道筋は対の上の Gödel 順序を経由する。順序を一階の対象言語の論理式として書き下し、順序数 `κ` のところで外部の Gödel 順序として読み、崩壊によって順序型へ落とし、計数の補題によって `κ` と比較する。本章は固定された宇宙レベル `ℓ` の上で、一つ上のレベルの排中律、すなわち以下の順序数の比較が依存する唯一の古典的仮定のもとで進む。

この構成がすべて構成的なわけではなく、その理由は形式化ではなく数学にある。順序数の対を順序づけるには、二つの順序数 `a` と `b` について `a` が `b` に属するかを判定しなければならない。本章の古典的な判定はどれもこの一つの問いの実例である。そこでモジュールは、レベル `ℓ-suc ℓ` の排中律を明示的なデータとして受け取る。判定される所属の命題の住むレベルである。

モジュールパラメータはその実例を一度だけ固定し、本章の古典的な段階はどれも正確にこれを消費する。

内在化される順序は、一階の対象言語で書かれる。所属と等しさ (等号) の原子式から、結合子、否定、非有界の存在量化子によって作られる論理式であり、周囲の階層の上で解釈される。階層の二つの事実がその傍らにあり、どちらも議論を閉じるために使われる。所属は整礎であり、順序数は `∈` に沿った帰納を許し、またどの集合も自分自身に属さないため、あり得ない比較はそのまま反証できる。

符号化された対の座標を読み、それで計数するには、三つの事実が要る。順序数の後続演算は単射であり、等しい後続は等しい先行者をもつ。順序数の各要素は小さな提示の添字によって名指され、その名指しは単射で、構成可能な集合の要素はそれ自身構成可能である。そして順序対 `pr` は両座標で単射であり、符号化された対はその二つの成分を確定する。

構成可能な側では、内側の構造 `𝒮ʟ` が階層を構成可能な集合という推移的クラスに制限する。全体を通して使う順序数の事実は閉性の事実である。順序数の要素は順序数であり、順序数の後続は順序数であり、`ω` の要素は順序数であり、任意の二つの順序数は三分法によって比較できる。その傍らには、対の上の外部の Gödel 順序、すなわち本章が内在化する順序がある。

二つの順序数の比較は、真理値ではなく三つの場合のデータとしてまとめられる。下の証明は、どの場合が起こったかを検査しなければならないからである。狭義に下、等しい、狭義に上。空集合と `ω` は `L` の要素として使え、内部の後続数詞はその基底集合の同一視を伴い、数項のスロットを周囲の自然数として読めるようにする。

`L` の内部では、順序対とグラフの条件を、内側と外側の二つの読みをもつ一階論理式で表す。対の妥当性は符号化された対を二つの成分からなる周囲の順序対と同一視し、グラフの読みは単値性、定義域、単射性、値が終域に属することを表す。これらの条件が内部の符号化された単射を記述する。

構成は三つの数学的な移行によって進む。まず順序数を、その中に含まれ、内部でそれと同じ濃度をもつ内部基数の代表に替える。次に、定義可能な単射関数から符号化された単射を得る。最後に、整礎で推移的な関係を順序数としての順序型へ崩壊し、三分法によって崩壊写像の単射性を示す。

二つの符号化された対の比較は、四つの座標と二つの最大値という六つの依存する証人を伴う。積は同時に成り立つ等式と順序条件を保ち、非交和は比較の場合分けを保つ。証明の成分は命題なので、得られる順序データに余分な選択を生じさせない。

符号化された対の座標は、`κ` の基底集合の要素であり、その集合の小さな提示を通して読まれる。提示の傍らには、周囲の所属、空虚性の証明を伴う空集合、そして `ω` と後続の演算があり、座標の比較と計数はこれらの概念の中で行われる。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )
```

三つの論理形式が繰り返し現れる。整礎性はすべての要素への到達可能性のデータとして現れ、これが崩壊を順序に沿って下降させる。反証は空の型に住み、証人の存在だけを主張する条件は切り詰めの下で述べられる。そのような条件を消費する目標がそれ自身命題や切り詰めであるため、それで十分なのである。

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

二つの台が名指され、区別して保たれる。周囲の台は階層本来の所属を運び、内側の台 `S` は構成可能な集合からなり、各要素は周囲の集合とその構成可能性の証明の対であり、その所属は基底の集合の上で読んだ周囲の所属である。

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

絶対性の実例は、構成可能な集合という推移的クラスの上で固定される。有界な論理式は `L` の内側でも外側でも同じ意味を持ち、環境は射影を通して読まれ、内側の充足関係は平易な `_⊨_` に改名される。

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

基礎となる集合とその構成可能性の証明に `isSetClass` を適用し、内側の台が h-集合であることを得る。続く対のパスの補題は、各成分の等しさから二つの対の等しさを構成する。

```agda
isSetS : isSet S
isSetS = isSetClass setIsSet (λ v → (isL v) .snd)
opaque
  pair≡ : {A : Type ℓ} {B : Type ℓ} {a a' : A} {b b' : B}
        → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
```

対のパスはまさにこの構成である。`a ≡ a'` と `b ≡ b'` から、各点で `(a , b) ≡ (a' , b')` というパスを作る。順序数は構成可能である。その理由は直接である。順序数 `x` はみずからの後続に属し、その段階は `L` の集合であり、段階への所属が構成可能性だからである。この主張は命題なので、証明は事実の外には何も運ばない。

```agda
  pair≡ e1 e2 = λ i → e1 i , e2 i
opaque
  isL-ord : (x : V ℓ) → IsOrd x → ⟨ isL x ⟩
  isL-ord x ox = Lset→isL (sucV x) (suc-ord ox) x (ord∈Lset-suc x ox)
```

したがって順序数 `x` は、その構成可能性の証明とともに、構成可能な台の要素 `ordL x ox` とみなせる。二つの座標がともに `K` に属するという関係に定義可能分出を適用すると、それらの順序対からなる構成可能集合 `prodL K` が得られる。

```agda
ordL : (x : V ℓ) → IsOrd x → S
ordL x ox = x , isL-ord x ox
private module Product (K : S) = Relation K K
```

積の記述の条件は、二つの座標がともに `K` の要素であることを述べる。ホスト側の読みは、二つの射影の `K` の基底集合への周囲の所属であり、その読みの両方向が与えられる。

```agda
          ((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K))
          (λ x y → (x .fst ∈ˢ K .fst) ⊓ (y .fst ∈ˢ K .fst))
          (λ x y e h → h) (λ x y e h → h)
```

したがって `prodL K` は、`K` の二つの要素からなる順序対の集合であり、`L` の内部でそれらを抑える段階から分出されたものである。

```agda
prodL : S → S
prodL = Product.rel
```

積への所属は、切り詰められた存在によって特徴づけられる。`K` の二つの要素 `a` と `b` があって、その要素がそれらの順序対に等しい、と。切り詰めは、条件が証人の存在を主張する以上のことを記録しない。この段階では、ある証人の対を別の対と区別する何ものもなく、切り詰めを取り除くことは、証人の一意性が証明された後にはじめて可能になる。

```agda
InProd : S → V ℓ → Type (ℓ-suc ℓ)
InProd K e = ∥ Σ[ a ∶ S ] Σ[ b ∶ S ]
               (⟨ a .fst ∈ˢ K .fst ⟩ × ⟨ b .fst ∈ˢ K .fst ⟩
                × (e ≡ pr (a .fst) (b .fst))) ∥₁
```

内向きには、`K` の任意の二つの要素の順序対が `prodL K` に属する。これは分出された関係そのものの導入規則である。

```agda
prodL-in : (K a b : S) → ⟨ a .fst ∈ˢ K .fst ⟩ → ⟨ b .fst ∈ˢ K .fst ⟩
         → ⟨ pr (a .fst) (b .fst) ∈ˢ (prodL K) .fst ⟩
prodL-in K a b ma mb = Product.into K a b ma mb (ma , mb)
```

外向きには、`prodL K` の要素は、切り詰められた形で `K` の二つの要素と対の等式から来る。`K` の小さな提示に対しては、切り詰めのないより強い主張も使える。積のすべての要素は、`K` の二つの添字が名指す要素の順序対なのである。

```agda
prodL-out : (K e : S) → ⟨ e .fst ∈ˢ (prodL K) .fst ⟩ → InProd K (e .fst)
prodL-out K e h = map₁ (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h)
prodL-fst : (K e : S) → ⟨ e .fst ∈ˢ (prodL K) .fst ⟩
          → Σ[ a ∶ ⟪ K .fst ⟫ ] Σ[ b ∶ ⟪ K .fst ⟫ ]
              (e .fst ≡ pr (⟪ K .fst ⟫↪ a) (⟪ K .fst ⟫↪ b))
```

証明は、切り詰められた証人を `K` の索引のファイバーへ変換し、対の等式をファイバー自身の同定に沿って修復する。その同定は、`K` の各要素がまさにその索引の名指す集合であることを述べる。

```agda
prodL-fst K e h = rec₁ isPropFib
  (λ { (a , b , ma , mb , q) →
     fiber (K .fst) ma .fst , fiber (K .fst) mb .fst
     , q ∙ cong₂ pr (sym (fiber (K .fst) ma .snd)) (sym (fiber (K .fst) mb .snd)) })
  (prodL-out K e h)
```

第二成分は一意である。順序対の単射性が名指された集合の等式を取り出し、`K` の索引の単射性がそれを添字の等式へ変える。

```agda
  where
  inner : (a : ⟪ K .fst ⟫)
        → isProp (Σ[ b ∶ ⟪ K .fst ⟫ ] (e .fst ≡ pr (⟪ K .fst ⟫↪ a) (⟪ K .fst ⟫↪ b)))
  inner a (b , q) (b' , q') = Σ≡Prop (λ _ → setIsSet _ _)
    (↪-inj {a = K .fst} (pr-inj (sym q ∙ q') .snd))
```

第一成分も同じ理由で一意であり、したがってファイバーの主張全体が命題になる。

```agda
  isPropFib : isProp (Σ[ a ∶ ⟪ K .fst ⟫ ] Σ[ b ∶ ⟪ K .fst ⟫ ]
                        (e .fst ≡ pr (⟪ K .fst ⟫↪ a) (⟪ K .fst ⟫↪ b)))
  isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner
    (↪-inj {a = K .fst} (pr-inj (sym q ∙ q') .fst))
```

## 論理式としての Gödel 順序

切り詰めのない読みはどの選択にも依存しない。積を手にしたところで、順序が登場する。`MaxIs` は、`a` と `b` が順序数であるとき、`m` がそれらの最大値であることを述べる。

```agda
MaxIs : S → S → S → Type (ℓ-suc ℓ)
```

定義は二つの選択肢を提示する。`a` が `b` に属し `m` が `b` であるか、`a` の `b` への所属が反証され `m` が `a` であるか。切り詰められるのはこの選言だけである。定義は、どちらかの選択肢が成り立つと主張するだけで、どちらかを判定しないからである。順序数の上では排中律が分枝を選び、選ばれた `m` が `a` と `b` の最大値になる。

```agda
MaxIs m a b =
  ∥ (⟨ a .fst ∈ˢ b .fst ⟩ × (m .fst ≡ b .fst))
  ⊎ ((⟨ a .fst ∈ˢ b .fst ⟩ → ⊥₀) × (m .fst ≡ a .fst)) ∥₁
```

二つの対の Gödel 比較も同じく切り詰めの下のデータである。第一の対の最大値 `m` が第二の対の最大値 `n` に属するか、二つの最大値が等しいときは辞書式に比較する。第一座標どうし、ついで第二座標どうしである。

```agda
OrdIs : S → S → S → S → S → S → Type (ℓ-suc ℓ)
OrdIs m n a b c d =
  ∥ ⟨ m .fst ∈ˢ n .fst ⟩
  ⊎ ((m .fst ≡ n .fst)
     × ∥ ⟨ a .fst ∈ˢ c .fst ⟩ ⊎ ((a .fst ≡ c .fst) × ⟨ b .fst ∈ˢ d .fst ⟩) ∥₁) ∥₁
```

最大値は有界な論理式として書ける。`a` が `b` に属するとき `m` は `b` に等しく、`a` の `b` への所属が反証されるとき `a` に等しい。否定が第二の選択肢を守られた分枝として立てる。`a` と `b` が順序数であるとき、この論理式が述べるのはまさに、`m` がそれらの最大値であることである。

```agda
maxAt : ∀ {k} → Fin k → Fin k → Fin k → Formula S k
maxAt m a b = ((var a ∈̇ var b) ∧̇ (var m ≐ var b))
            ∨̇ ((¬̇ (var a ∈̇ var b)) ∧̇ (var m ≐ var a))
```

Gödel の比較も同じやり方で書ける。その優先順位は明示的である。まず最大値を比較し、最大値が等しいときは第一座標を比較し、第一座標も等しいときには第二座標を比較する。

```agda
ordAt : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S k
ordAt m n a b c d =
    (var m ∈̇ var n)
  ∨̇ ((var m ≐ var n)
     ∧̇ ((var a ∈̇ var c) ∨̇ ((var a ≐ var c) ∧̇ (var b ∈̇ var d))))
```

部品を合わせると、`Lt p q` は次のように述べる。`p` と `q` は符号化された対であり、それぞれ要素 `a`、`b` と要素 `c`、`d` からなり、その最大値 `m` と `n` は最大値の条件を満たし、その比較は Gödel の条件を満たす、と。六つの証人は切り詰めの下に記録される。条件が主張するのは証人の存在だけであり、古典的な場合分けが選択肢の中から選ぶのはその後である。

```agda
Lt : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Lt p q = ∥ Σ[ a ∶ S ] Σ[ b ∶ S ] Σ[ c ∶ S ] Σ[ d ∶ S ] Σ[ m ∶ S ] Σ[ n ∶ S ]
           ( (p ≡ pr (a .fst) (b .fst)) × (q ≡ pr (c .fst) (d .fst))
           × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d ) ∥₁
```

六つの束縛子には、呼び出し側の環境を超える六つのスロットが要り、`↑6` は添字をちょうどその数だけずらす。

```agda
private
  ↑6 : ∀ {k} → Fin k → Fin (suc (suc (suc (suc (suc (suc k))))))
  ↑6 i = suc (suc (suc (suc (suc (suc i)))))
```

六つのスロットには `i0` から `i5` までの名前が付き、量化された証人ごとに一つである。最初の三つの別名は位置 0、1、2 を束縛し、そこには第二の対の最大値、第一の対の最大値、第二の対の第二座標が入る。

```agda
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc zero
  i2 : ∀ {k} → Fin (suc (suc (suc k)))
```

別名は続く。位置 2 には第二の対の第二座標が、位置 3 にはその第一座標が、位置 4 には第一の対の第二座標が入る。

```agda
  i2 = suc (suc zero)
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc (suc (suc zero))
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
  i4 = suc (suc (suc (suc zero)))
```

位置 5 は第一の対の第一座標であり、六つがそろう。ついで順序の論理式が始まる。六つの証人を順に束縛し、`p` と `q` について Gödel の比較の要求する内容を述べるのである。

```agda
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc (suc (suc (suc (suc zero))))
opaque
  ltAt : ∀ {k} → Fin k → Fin k → Formula S k
  ltAt p q = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (
```

本体は六つの証人を順に束縛し、五つの原子を連言する。`p` は第五と第四のスロットの順序対、`q` は第三と第二のスロットの順序対であり、第一の最大値の原子は `p` の座標を、第二の最大値の原子は `q` の座標を結び、順序の原子が二つの最大値を、ついで座標を比較する。六スロットの文脈で読めば、これはまさに、Gödel 順序において `p` が `q` より下であることを述べている。

```agda
        prAtL (↑6 p) i5 i4
     ∧̇ (prAtL (↑6 q) i3 i2
     ∧̇ (maxAt i1 i5 i4
     ∧̇ (maxAt i0 i3 i2
     ∧̇ ordAt i1 i0 i5 i4 i3 i2)))))))))
```

妥当性は、具体的な六項目の文脈に対して確かめられる。この文脈は、呼び出し側の環境に六つの証人を新しいものから順に加えたもの、すなわち `n`、`m`、`d`、`c`、`b`、`a` であり、スロット 0 が `n`、スロット 5 が `a` となって別名と一致する。

```agda
  private
    env : ∀ {k} → Vec S k → S → S → S → S → S → S
        → Vec S (suc (suc (suc (suc (suc (suc k))))))
    env γ a b c d m n = n ∷ m ∷ d ∷ c ∷ b ∷ a ∷ γ
```

最初の妥当性の補題は、その文脈で対の原子を読む。対の原子の充足は、呼び出し側の `p` と `a`、`b` の順序対との間の等式である。

```agda
    atP : ∀ {k} (p : Fin k) (γ : Vec S k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩
        ≡ ((lookup p γ) .fst ≡ pr (a .fst) (b .fst))
    atP p γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 p) i5 i4 (env γ a b c d m n))
```

第二は `q` と `c`、`d` の順序対について同じことをする。この二つの同定により、論理式の充足と `Lt` の六証人のデータは互いに取り替えられる。

```agda
    atQ : ∀ {k} (q : Fin k) (γ : Vec S k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩
        ≡ ((lookup q γ) .fst ≡ pr (c .fst) (d .fst))
    atQ q γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 q) i3 i2 (env γ a b c d m n))
```

外向きの方向は、六重に入れ子になった切り詰めを順に消費する。`γ` での `ltAt p q` の充足から、証人 `a` から `n` までと、対の等式、二つの最大値のデータ、そして順序のデータが得られる。

```agda
  lt-out : ∀ {k} (p q : Fin k) (γ : Vec S k) → ⟨ γ ⊨ ltAt p q ⟩
         → Lt ((lookup p γ) .fst) ((lookup q γ) .fst)
  lt-out p q γ = rec₁ squash₁ (λ { (a , ha) → rec₁ squash₁ (λ { (b , hb) →
    rec₁ squash₁ (λ { (c , hc) → rec₁ squash₁ (λ { (d , hd) →
    rec₁ squash₁ (λ { (m , hm) → rec₁ squash₁ (λ { (n , (hp , (hq , (hM , (hN , hO))))) →
```

二つの対の等式は妥当性のパスに沿って輸送され、第一の最大値のデータは周囲のレベルへ運ばれる。六つの存在の証人は持ち上げられた意味の水準に住むので、肯定の場合はそのまま残り、反証の場合は持ち上げの外へ降ろされる。

```agda
      ∣ a , b , c , d , m , n
      , ( transport (atP p γ a b c d m n) hp
        , transport (atQ q γ a b c d m n) hq
        , map₁ (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM
```

第二の最大値のデータも同じやり方で写され、呼び出し側の `p` と `q` における `Lt` の証人がそろう。

```agda
        , map₁ (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hN
        , hO ) ∣₁ }) hm }) hd }) hc }) hb }) ha })
```

内向きの方向は、`Lt` を充足の主張へ変える。主張は命題である。

```agda
  lt-in : ∀ {k} (p q : Fin k) (γ : Vec S k)
        → Lt ((lookup p γ) .fst) ((lookup q γ) .fst) → ⟨ γ ⊨ ltAt p q ⟩
  lt-in p q γ = rec₁ ((γ ⊨ ltAt p q) .snd)
    (λ { (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) →
      ∣ a , ∣ b , ∣ c , ∣ d , ∣ m , ∣ n
```

六つの証人は入れ子の存在証人として再び入れられ、対の等式は妥当性のパスに沿って逆向きに輸送される。

```agda
      , ( transport (sym (atP p γ a b c d m n)) ep
        , ( transport (sym (atQ q γ a b c d m n)) eq'
        , ( map₁ (λ { (inl h) → inl h
                      ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM
          , ( map₁ (λ { (inl h) → inl h
```

二つの最大値のデータは今度は対象レベルの守られた原子へ持ち上げて写され、順序のデータが論理式を閉じる。Gödel のモジュールはついで、集合 `P` のためのこの順序をまとめる。その記述の条件は、二つの座標がともに `P` の要素であることを要求し、順序の論理式で両者を結ぶ。

```agda
                        ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hN
            , hO )))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
private module Godel (P : S) = Relation P P
          ((var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ltAt (suc zero) zero))
```

ホスト側の読みは、両側に `P` への所属を加え、順序の関係と連言する。二つの方向は、二つの束縛子の占めるスロットで、外向きと内向きの補題を引用する。第一座標が外側のスロット、第二座標が内側のスロットである。

```agda
          (λ p q → (p .fst ∈ˢ P .fst) ⊓ ((q .fst ∈ˢ P .fst) ⊓ (Lt (p .fst) (q .fst) , squash₁)))
          (λ p q e h → h .fst , h .snd .fst , lt-out (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
          (λ p q e h → h .fst , h .snd .fst , lt-in (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
```

`godel P` がその分出された関係である。`L` の内部における、`P` の要素からなる順序対のうち、Gödel 順序で互いに下にあるものの集合である。

```agda
godel : S → S
godel = Godel.rel
```

内向きには、`P` の二つの要素 `p` と `q` について、`p` が `q` より下なら、その順序対は `godel P` に属する。

```agda
godel-in : (P p q : S) → ⟨ p .fst ∈ˢ P .fst ⟩ → ⟨ q .fst ∈ˢ P .fst ⟩
         → Lt (p .fst) (q .fst) → ⟨ pr (p .fst) (q .fst) ∈ˢ (godel P) .fst ⟩
godel-in P p q mp mq l = Godel.into P p q mp mq (mp , mq , l)
```

外向きには、`godel P` の要素には二つの要素とその間の順序のデータが伴う。

```agda
godel-out : (P p q : S) → ⟨ pr (p .fst) (q .fst) ∈ˢ (godel P) .fst ⟩
          → ⟨ p .fst ∈ˢ P .fst ⟩ × ⟨ q .fst ∈ˢ P .fst ⟩ × Lt (p .fst) (q .fst)
godel-out = Godel.pair-out
```

## ホスト側の順序への移送

順序のモジュールはついで、平方律が述べられる場合である順序数 `κ` を固定する。

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

```agda
module Order (κ : S) (oκ : IsOrd (κ .fst)) where
```

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

`K` は順序数 `κ` の基底集合である。平方律が展開される台は、まさに `κ` 以下の順序数からなるこの集合である。

```agda
  K : V ℓ
  K = κ .fst
```

`↑` は、小さな提示の埋め込みを通して、`K` の要素を周囲で名指す。各添字はそれが提示する順序数を指すのである。

```agda
  ↑ : ⟪ K ⟫ → V ℓ
  ↑ = ⟪ K ⟫↪
```

添字 `m : ⟪ K ⟫` は周囲の集合 `↑ m` を名指し、それが `κ` に属する証明を伴う。構成可能性は要素へ受け継がれるので、`upK m` はこの名指された順序数を `L` の要素としてまとめる。

```agda
  upK : ⟪ K ⟫ → S
  upK m = ↑ m , isL-trans {x = K} {y = ↑ m} (member K m) (κ .snd)
```

比較される順序の台は `Pair`、すなわち `κ` の二つの添字の型である。ホスト側の順序対であり、各座標は `κ` より下の順序数を名指す。

```agda
  Pair : Type ℓ
  Pair = ⟪ K ⟫ × ⟪ K ⟫
```

座標そのものの上には座標の順序 `≺₁` が立っている。外部の平方律の構成から引用されたもので、`κ` より下の順序数を、それらが名指す周囲の集合どうしの所属によって狭義に比較する。

```agda
  _≺₁_ : ⟪ K ⟫ → ⟪ K ⟫ → Type (ℓ-suc ℓ)
  _≺₁_ = O._≺₁_
    where module O = SQ.OnOrdinal K oκ
```

順序対の上には Gödel 順序 `≺ₚ` が立つ。まず最大値を比べ、ついで第一座標、最後に第二座標を比べるものである。内部の論理式が再現すべき外部の順序はこれである。

```agda
  _≺ₚ_ : Pair → Pair → Type (ℓ-suc ℓ)
  _≺ₚ_ = O._≺_
    where module O = SQ.OnOrdinal K oκ
```

最大値の演算 `maxOrd` は、`κ` より下の二つの順序数に対して大きい方を返す。これも外部の構成からの引用であり、やはり要素が順序数であるからこそ最大値として読めるのである。

```agda
  maxOrd : ⟪ K ⟫ → ⟪ K ⟫ → ⟪ K ⟫
  maxOrd = SQ.maxOrd K oκ
```

二つの小さな事実が、両側の比較の準備をする。第一に、順序数 `κ` の各要素はそれ自身順序数であり、名指された順序数は順序数性の証明を帯ぶ。第二に、`max-out` は、基底の集合が `a'` と `b'` を名指す要素の上で読んだ内部の最大値の条件が、内部の最大値をちょうど `a'` と `b'` のホストの最大値に強いることを述べる。証明はホストの順序の三分法のデータに沿って進む。

```agda
  ord↑ : (m : ⟪ K ⟫) → IsOrd (↑ m)
  ord↑ m = mem-ord {A = K} oκ (↑ m) (member K m)
  max-out : (a b m : S) (a' b' : ⟪ K ⟫) → a .fst ≡ ↑ a' → b .fst ≡ ↑ b'
          → MaxIs m a b → m .fst ≡ ↑ (maxOrd a' b')
  max-out a b m a' b' ea eb = rec₁ (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))
```

場合分けの関数が、この議論の形を固定する。ホストの三分法は下・等しい・上に分かれ、内部のデータは肯定の場合 (`m` が `b`) と反証の場合 (`m` が `a`) に分かれる。二つの場合分けを項ごとに合わせることが内容のすべてである。

```agda
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → (⟨ a .fst ∈ˢ b .fst ⟩ × (m .fst ≡ b .fst))
         ⊎ ((⟨ a .fst ∈ˢ b .fst ⟩ → ⊥₀) × (m .fst ≡ a .fst))
       → m .fst ≡ ↑ (SQ.maxGo K oκ a' b' t)
```

下の場合、肯定の分枝は `m` と `b` の等式に `b` の名指しを合成してホストの最大値を与える。その反証の分枝は不可能である。反証されている所属は、まさに三分法の証人であり、二つの名指しを通して輸送されるだけだからである。

```agda
    go (lt h) (inl (_ , e))   = e ∙ eb
    go (lt h) (inr (na , _))  =
      ⊥₀-rec (na (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (sym ea) (sym eb) h))
    go (eq p) (inl (a∈b , _)) =
      ⊥₀-rec (∈-irrefl (↑ b')
```

等しい場合、肯定の分枝は `a` が `b` の内側にあると置くが、ホストは両者を等しいと宣言しており、名指された順序数 `b` における所属の非反射性と矛盾する。反証の分枝は、最大値を `a` と名指し、`a` の名指しに沿って輸送する。

```agda
        (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (ea ∙ cong ↑ p) eb a∈b))
    go (eq p) (inr (_ , e))   = e ∙ ea
    go (gt h) (inl (a∈b , _)) =
      ⊥₀-rec (∈-irrefl (↑ a')
        (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'}
```

上の場合、ホストの証人は `b ∈ a` を与える。内部でも肯定の枝を取ると `a ∈ b` も得られ、推移性によって `a` での非反射性に反する。

```agda
          (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea eb a∈b) h))
    go (gt h) (inr (_ , e))   = e ∙ ea
```

逆の `max-in` は、ホストの最大値を内部の述語の中に書き込む。添字の各対に対して、`maxOrd` が名指す持ち上げられた要素が、持ち上げられた二つの座標で `MaxIs` を満たす。

```agda
  max-in : (a' b' : ⟪ K ⟫) → MaxIs (upK (maxOrd a' b')) (upK a') (upK b')
  max-in a' b' = go (SQ.tri₁ K oκ a' b')
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → MaxIs (upK (SQ.maxGo K oκ a' b' t)) (upK a') (upK b')
```

その三つの場合はホストの比較から直ちに従う。下では肯定の分枝に等式が定義的に付随し、等しい場合は非反射性によって所属が退けられ、上ではその座標自身の順序数性を通して退けられる。同じブロックでは `code`、すなわちホストの対の二つの名指された順序数の周囲の順序対が定義される。

```agda
    go (lt h) = ∣ inl (h , refl) ∣₁
    go (eq p) = ∣ inr ((λ h → ∈-irrefl (↑ b') (subst (λ w → ⟨ ↑ w ∈ˢ ↑ b' ⟩) p h)) , refl) ∣₁
    go (gt h) = ∣ inr ((λ h' → ∈-irrefl (↑ a') (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'} h' h)) , refl) ∣₁
  code : Pair → V ℓ
  code p = pr (↑ (p .fst)) (↑ (p .snd))
```

移送の核心は反証の補題である。ここでは矛盾の形をしたデータの対を仮定する。`p` と `q` の符号化された対の上で `Lt` が成り立ちながら、ホストの順序はその比較を拒むのである。こうして仮定された `Lt` の六つの証人が、一つの矛盾の主張にまとめられる。

```agda
  private
    refute : (p q : Pair) → (p ≺ₚ q → ⊥₀)
           → Σ[ a ∶ S ] Σ[ b ∶ S ] Σ[ c ∶ S ] Σ[ d ∶ S ] Σ[ m ∶ S ] Σ[ n ∶ S ]
               ( (code p ≡ pr (a .fst) (b .fst)) × (code q ≡ pr (c .fst) (d .fst))
               × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d )
```

結論は空の型である。仮定された順序のデータと拒まれた比較は共存できない。証明は六つの証人を分解し、それらの名指す基底の集合の上で作業する。

```agda
           → ⊥₀
    refute (a' , b') (c' , d') nk (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) =
      rec₁ isProp⊥ outer hO
      where
      ea : a .fst ≡ ↑ a'
```

順序対の単射性が、各符号化の等式から、証人の基底集合と対応する名指された順序数の同定を取り出す。この四つの等式が、後のすべての比較の錨となる。

```agda
      ea = sym (pr-inj ep .fst)
      eb : b .fst ≡ ↑ b'
      eb = sym (pr-inj ep .snd)
      ec : c .fst ≡ ↑ c'
      ec = sym (pr-inj eq' .fst)
```

二つの最大値は、二つの最大値のデータに `max-out` を適用して、ホストの最大値と同一視される。ここで構成全体の内部の読みと外部の読みは、六つの座標のすべてで一致する。

```agda
      ed : d .fst ≡ ↑ d'
      ed = sym (pr-inj eq' .snd)
      em : m .fst ≡ ↑ (maxOrd a' b')
      em = max-out a b m a' b' ea eb hM
      en : n .fst ≡ ↑ (maxOrd c' d')
```

等式 `en` は第二の対にも同じ同定を与えるので、`OrdIs` をホストの最大値と座標へすべて輸送できるようになる。

```agda
      en = max-out c d n c' d' ec ed hN
```

内側の補題は座標の比較を移送する。名指された第一座標の間の周囲の所属は、二つの名指しの同定に沿って輸送されると、ホストの順序での下関係になる。

```agda
      inner : ⟨ a .fst ∈ˢ c .fst ⟩ ⊎ ((a .fst ≡ c .fst) × ⟨ b .fst ∈ˢ d .fst ⟩)
            → (a' ≺₁ c') ⊎ ((a' ≡ c') × (b' ≺₁ d'))
      inner (inl h)       = inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea ec h)
      inner (inr (e , h)) =
        inr ( ↪-inj {a = K} (sym ea ∙ e ∙ ec)
```

相等の場合も同じく伝わる。名指された集合の等式を二つの名指しの間で巡らせると、`K` の名指しの単射性によって添字の等式になり、第二座標は従来どおり比較される。

```agda
            , subst2 (λ x y → ⟨ x ∈ˢ y ⟩) eb ed h )
```

第一の最大値が第二の最大値に属するなら、この所属を `em` と `en` に沿って輸送すると `p ≺ₚ q` の最大値が真に小さい枝が得られ、`nk` と矛盾する。

```agda
      outer : ⟨ m .fst ∈ˢ n .fst ⟩
            ⊎ ((m .fst ≡ n .fst)
               × ∥ ⟨ a .fst ∈ˢ c .fst ⟩ ⊎ ((a .fst ≡ c .fst) × ⟨ b .fst ∈ˢ d .fst ⟩) ∥₁)
            → ⊥₀
      outer (inl h)       = nk (inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) em en h))
```

二つの最大値が等しいなら、基底集合の等式が名指しの単射性によって添字の等式になり、内側の補題がホストの順序の中で二つの対を比較して、再び拒否を退ける。

```agda
      outer (inr (e , h)) = rec₁ isProp⊥
        (λ w → nk (inr (↪-inj {a = K} (sym em ∙ e ∙ en) , inner w))) h
```

`lt→≺` の証明では、ホストの対の三分法から三つの場合が生じる。求める狭義の枝はそのまま返せる。相等または逆向きの狭義の枝では、`p ≺ₚ q` を否定すると `refute` により仮定した `Lt` と矛盾するので、やはり求める比較が得られる。

```agda
  lt→≺ : (p q : Pair) → Lt (code p) (code q) → p ≺ₚ q
  lt→≺ p q l = go (SQ.tri≺ K oκ p q)
    where
    refuted : ((p ≺ₚ q) → ⊥₀) → p ≺ₚ q
    refuted nk = ⊥₀-rec (rec₁ isProp⊥ (refute p q nk) l)
```

相等の場合、仮定した `p ≺ₚ q` は `q ≺ₚ q` へ輸送され、非反射性に反する。逆向きの狭義の場合、その仮定した比較を `q ≺ₚ p` と合成すると `p ≺ₚ p` が得られ、やはり不可能である。

```agda
    go : TriW (p ≺ₚ q) (p ≡ q) (q ≺ₚ p) → p ≺ₚ q
    go (lt k) = k
    go (eq e) = refuted (λ k → SQ.irr≺ K oκ q (subst (λ w → w ≺ₚ q) e k))
    go (gt h) = refuted (λ k → SQ.irr≺ K oκ p (SQ.trans≺ K oκ p q p k h))
```

逆の `≺→lt` は、ホストの比較を対象言語の中に書き込む。六つの証人は持ち上げられた座標と二つの持ち上げられた最大値であり、対の等式は定義的に成り立ち、最大値のデータは `max-in` が、順序のデータはホストの比較そのものが供給する。

```agda
  ≺→lt : (p q : Pair) → p ≺ₚ q → Lt (code p) (code q)
  ≺→lt (a' , b') (c' , d') k =
    ∣ upK a' , upK b' , upK c' , upK d' , upK (maxOrd a' b') , upK (maxOrd c' d')
    , ( refl , refl , max-in a' b' , max-in c' d' , ord k ) ∣₁
    where
```

順序のデータは場合ごとに読まれる。狭義の所属はそのまま通り、相等の二つの場合は、最大値の名指しおよび座標の名指しに沿ってそれぞれ輸送される。

```agda
    ord : (a' , b') ≺ₚ (c' , d')
        → OrdIs (upK (maxOrd a' b')) (upK (maxOrd c' d')) (upK a') (upK b') (upK c') (upK d')
    ord (inl h)                 = ∣ inl h ∣₁
    ord (inr (e , inl h))       = ∣ inr (cong ↑ e , ∣ inl h ∣₁) ∣₁
    ord (inr (e , inr (f , h))) = ∣ inr (cong ↑ e , ∣ inr (cong ↑ f , h) ∣₁) ∣₁
```

`x < y` なら `y < z` との推移性から `x < z` を得る。`x = y` なら、与えられた `y < z` をその等式に沿って輸送する。

```agda
  private
    ≤→≺ : (x y z : ⟪ K ⟫) → let module O = SQ.OnOrdinal K oκ in x O.≤₁ y → y ≺₁ z → x ≺₁ z
    ≤→≺ x y z (inl h) h' = SQ.trans₁ K oκ x y z h h'
    ≤→≺ x y z (inr e) h' = subst (λ w → w ≺₁ z) (sym e) h'
```

対になる補題は、`x ≤ y` と `y = y'` から、`x` が `y'` の後続に属することを導く。狭義の場合は `x ∈ y'` から後続への所属が直接従う。等しい場合は `x` を `y'` と同一視すると、主張は `y'` が自身の後続に属することへ帰着する。

```agda
    ≤→∈suc : (x y y' : ⟪ K ⟫) → let module O = SQ.OnOrdinal K oκ in x O.≤₁ y → y ≡ y'
           → ⟨ ↑ x ∈ˢ sucV (↑ y') ⟩
    ≤→∈suc x y y' (inl h) e = ∈sucV-inl (subst (λ w → x ≺₁ w) e h)
    ≤→∈suc x y y' (inr q) e =
      subst (λ w → ⟨ ↑ w ∈ˢ sucV (↑ y') ⟩) (sym (q ∙ e)) (self∈sucV (↑ y'))
```

節の補題がここで順序から読み取られる。対 `r` が対 `p` より下なら、`r` の第一座標は `p` の最大値の後続の要素である。最大値が真に比較される場合は、たかだかの関係に続いて狭義の比較が行われる。

```agda
  fst∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (r .fst) ∈ˢ sucV (↑ (maxOrd (p .fst) (p .snd))) ⟩
  fst∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) h)
  fst∈suc (a , b) (c , d) (inr (e , _)) =
```

最大値が等しい場合は、第一座標は共有された最大値を超えず、二つの最大値は同一視されるので、所属は最大値がみずからの後続に属することから従う。

```agda
    ≤→∈suc a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) e
```

同じ議論を第二座標に適用すると `snd∈suc` が得られる。`r` の第二座標もまた、二つの最大値が狭義に比較される場合にも、等しい場合にも、`p` の最大値の後続に収まる。

```agda
  snd∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (r .snd) ∈ˢ sucV (↑ (maxOrd (p .fst) (p .snd))) ⟩
  snd∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) h)
  snd∈suc (a , b) (c , d) (inr (e , _)) =
```

この二つの評価から、`(c, d)` の任意の先行者の両座標が `suc(max(c, d))` に属することが分かる。

```agda
    ≤→∈suc b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) e
```

</div>
</details>

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

```agda
module Coll (κ : S) (oκ : IsOrd (κ .fst)) where
```

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

これらの評価は Gödel 順序の各先行者切片を制御する。整礎性と推移性を合わせると、`prodL κ` 上の関係を順序数としての順序型へ崩壊できる状況が得られる。

```agda
  open Order κ oκ
```

順序型へ崩壊される集合は `P`、すなわち積である。順序数 `κ` の要素の順序対の集合であり、すでに `L` の内部で分出されている。

```agda
  P : S
  P = prodL κ
```

崩壊に用いられる関係は `R`、つまりその積の上の Gödel 順序である。`P` の二つの要素は、一方が他方より下で比較されるときに限り関係づけられる。

```agda
  R : S
  R = godel P
```

Gödel 関係では直接従う。`y R x` なら、`y` と `x` はともにその積の要素である。

```agda
  Rsub : (y x : S) → Holds R y x → ⟨ y .fst ∈ P .fst ⟩ × ⟨ x .fst ∈ P .fst ⟩
  Rsub y x h = godel-out P y x h .fst , godel-out P y x h .snd .fst
```

順序型の仕組みはこの積のために一度実例化される。その定義域は崩壊の添字集合であり、`φ` は各添字に対して、積の対応する要素が提示するホストの対を読み取る。二つの座標は積の提示の読みによって切り詰めなしで回収される。

```agda
  module OT = Code P R Rsub using (Dom; Dom≡; isProp≺; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out; module Conjuncts)
  φ : OT.Dom → Pair
  φ m = prodL-fst κ (OT.up m) (OT.up-mem m) .fst
      , prodL-fst κ (OT.up m) (OT.up-mem m) .snd .fst
```

この読みには等式が伴う。添字の内部の符号化は、二つの座標の周囲の順序対に等しいのである。この等式が、内部の順序と外部の順序の間のすべての比較の継ぎ目である。

```agda
  φ-eq : (m : OT.Dom) → OT.↪ m ≡ code (φ m)
  φ-eq m = prodL-fst κ (OT.up m) (OT.up-mem m) .snd .snd
```

`φ` は単射である。二つの添字が同じホストの対を名指すなら、それらの符号化は一致し、定義域みずからの基準、すなわち符号化の相等が添字の相等を返す。したがって、異なる二つの積の添字が同じホストの対へ送られることはない。

```agda
  φ-inj : (m n : OT.Dom) → φ m ≡ φ n → m ≡ n
  φ-inj m n e = OT.Dom≡ (φ-eq m ∙ cong code e ∙ sym (φ-eq n))
```

順方向の移送は、内部の順序を外向きに読む。二つの添字が `L` の内部で比較されれば、それらのホストの対は Gödel 順序で比較される。証明は定義の等式と論理式の外向きの読みを引用し、二つのホストの対の上で移送 `lt→≺` を適用する。

```agda
  ≺-fwd : (m n : OT.Dom) → m OT.≺ n → φ m ≺ₚ φ n
  ≺-fwd m n k = lt→≺ (φ m) (φ n)
    (subst2 Lt (φ-eq m) (φ-eq n) (godel-out P (OT.up m) (OT.up n) (OT.≺-out m n k) .snd .snd))
```

逆方向の移送は、ホストの順序を内向きに読み、論理式の内向きの読みと、同じ二つの対の上の移送 `≺→lt` を引用する。二つの方向を合わせると、崩壊の添字の上の内部の関係は、`φ` を通して読んだホストの Gödel 順序にほかならないと言える。

```agda
  ≺-bwd : (m n : OT.Dom) → φ m ≺ₚ φ n → m OT.≺ n
  ≺-bwd m n k = OT.≺-in m n
    (godel-in P (OT.up m) (OT.up n) (OT.up-mem m) (OT.up-mem n)
      (subst2 Lt (sym (φ-eq m)) (sym (φ-eq n)) (≺→lt (φ m) (φ n) k)))
```

整礎性は添字とともに伝わる。ホストの対の到達可能性は、対応する添字の到達可能性を供給し、その先行者は前方へ、真に小さい対のホストの対へ写される。こうして外部の順序に沿う帰納が、内部の順序に沿う帰納になる。

```agda
  wf : WellFounded OT._≺_
  wf m = go (SQ.wf≺ K oκ (φ m))
    where
    go : {n : OT.Dom} → Acc _≺ₚ_ (φ n) → Acc OT._≺_ n
    go {n} (acc r) = acc (λ n' k → go (r (φ n') (≺-fwd n' n k)))
```

推移性も同じように伝わる。内部の二段階を外向きに読み、ホストの順序の推移性で合成し、`a` から `c` への一段階として内向きに読み戻す。

```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 (SQ.trans≺ K oκ (φ a) (φ b) (φ c) (≺-fwd a b k) (≺-fwd b c k'))
```

三分法が移送された一式を完成させる。任意の二つの添字に対して、ホストの三分法がそれらの対を比較する。主張は内部の比較の三方向の和として述べられる。

```agda
  tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
  tri a b = go (SQ.tri≺ K oκ (φ a) (φ b))
    where
    go : TriW (φ a ≺ₚ φ b) (φ a ≡ φ b) (φ b ≺ₚ φ a)
       → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
```

三つの場合はそれぞれ読み戻される。二つの狭義の場合は逆方向の移送を通り、相等の場合は `φ` の単射性を通って、同じホストの対を名指す添字は等しくなる。

```agda
    go (lt h) = inl (≺-bwd a b h)
    go (eq e) = inr (inl (φ-inj a b e))
    go (gt h) = inr (inr (≺-bwd b a h))
```

整礎性と推移性から崩壊とその順序型を構成する。

```agda
  module C = OT.Conjuncts wf ≺-trans using (module Inj; col; col-ord; col-out; colTable; colTable-in; colTable-pair; colʟ; otL; otL-out)
  module I = C.Inj tri using (code; col-inj; module Inverse)
  injL-ot : InjL P C.otL
  injL-ot = ∣ C.colTable , I.code ∣₁
```

</div>
</details>

## 三つの計数事実

続いて三分法が崩壊写像の単射性を与えるので、そのグラフが内部単射 `P ↪ C.otL` を証する。

```agda
incl : (a b : V ℓ) → ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ b ⟩) → ⟪ a ⟫ ↪ ⟪ b ⟫
```

計数の補題は周囲の側から始まる。二つの周囲の集合の間の包含は小さな提示の上で働く。部分集合の各添字は大きい集合の要素を名指し、その要素の大きい提示におけるファイバーが対応する添字を名指す。

```agda
incl a b sub = ι , ι-inj
  where
  ι : ⟪ a ⟫ → ⟪ b ⟫
  ι m = fiber b (sub (⟪ a ⟫↪ m) (member a m)) .fst
  ι-inj : (m n : ⟪ a ⟫) → ι m ≡ ι n → m ≡ n
```

誘導された添字の写しは単射である。部分集合の二つの添字が名指す要素が大きい提示で同じ添字によって名指されるなら、名指しの等式が名指された要素の等式を強制し、部分集合みずからの単射性が添字の等式を返す。

```agda
  ι-inj m n e = ↪-inj {a = a}
    (sym (fiber b (sub (⟪ a ⟫↪ m) (member a m)) .snd)
     ∙ cong ⟪ b ⟫↪ e
     ∙ fiber b (sub (⟪ a ⟫↪ n) (member a n)) .snd)
opaque
```

`L` 内の符号化された単射は外側で読み取れる。そのグラフ条件から、定義域と終域の小さな提示の間の単射が定まる。さらに任意の無限順序数 `a` に対する `ω ⊆ a` と合わせることで、内部単射を通常の基数比較へ結びつける。

```agda
  coded→ambient : (a b : S) → Σ[ F ∶ S ] InjCode F a b → ⟪ a .fst ⟫ ↪ ⟪ b .fst ⟫
  coded→ambient a b (F , sv , dm , ij , ran) = Sm.small , Sm.small-inj
    where module Sm = Small F a b sv dm ij ran
ω⊆ : (a : V ℓ) → IsOrd a → (⟨ a ∈ˢ ω ⟩ → ⊥₀)
   → (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
```

`ω` の包含は、順序数 `a` での三分法から従う。無限性の仮定により `a` は `ω` に属せず、`a` が `ω` に等しいときは所属が輸送され、`ω` が `a` の内側にあるときは推移性がすべての所属を中継する。

```agda
ω⊆ a oa a∉ω z z∈ω = go (ord-tri a oa ω ω-ord)
  where
  go : ⟨ a ∈ˢ ω ⟩ ⊎ ((a ≡ ω) ⊎ ⟨ ω ∈ˢ a ⟩) → ⟨ z ∈ˢ a ⟩
  go (inl h)         = ⊥₀-rec (a∉ω h)
  go (inr (inl e))   = subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω
```

その最後の場合は、`z ∈ ω` と `ω ∈ a` に推移性を適用するものである。包含を手にすると、第二の計数の事実は排除となる。無限の順序数は、`ω` の要素、すなわち有限の順序数への内部の単射を許さない。

```agda
  go (inr (inr ω∈a)) = oa .fst z∈ω ω∈a
no-fin : (a b : S) → IsOrd (a .fst) → (⟨ a .fst ∈ˢ ω ⟩ → ⊥₀)
       → IsOrd (b .fst) → ⟨ b .fst ∈ˢ ω ⟩ → InjL a b → ⊥₀
no-fin a b oa a∉ω ob b∈ω = rec₁ isProp⊥ (λ c →
  finite-excl-ω (b .fst) ob b∈ω (λ x → h c x , h c x)
```

反証の最後の部分は、`ω` が `a` に含まれるという事実を引用する。`ω ⊆ a` なので二つの補題が合成され、`ω` から `b` への単射は `a` を経由すると `ω` から有限集合 `b` への単射になる。包含写像 `ι` は where 節で一度定められる。

```agda
    (λ x y e → ι .snd x y
       (coded→ambient a b c .snd (ι .fst x) (ι .fst y) (cong (λ p → p .fst) e))))
  where
  ι : ⟪ ω ⟫ ↪ ⟪ a .fst ⟫
  ι = incl ω (a .fst) (ω⊆ (a .fst) oa a∉ω)
```

写像 `h` は包含 `ω ↪ a` の後で符号化された単射を評価する。

```agda
  h : Σ[ F ∶ S ] InjCode F a b → ⟪ ω ⟫ → ⟪ b .fst ⟫
  h c x = coded→ambient a b c .fst (ι .fst x)
```

## 符号化された単射を直積へ持ち上げる

積上の写像を構成するため、`a` 上で単値であり、定義域が `a`、単射的で、値が `b` に入るグラフ `F` を固定する。これらが符号化された単射 `a ↪ b` の四条件である。

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

```agda
module ProdMap (a b F : S)
               (sv : ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩)
               (ij : ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩)
               (ran : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩
                    → ⟨ y .fst ∈ b .fst ⟩) where
```

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

写像 `h` は包含 `ω ↪ a` の後で符号化された単射を評価する。積上の写像を構成するため、`a` 上で単値であり、定義域が `a`、単射的で、値が `b` に入るグラフ `F` を固定する。これらが符号化された単射 `a ↪ b` の四条件である。

抽出のモジュールは、グラフから実際の関数を読み取る。`toFun` が定義域の各要素での値を計算し、`toFun-graph` がその対がグラフに属することを証明し、`toFun-inj` がグラフの単射性を関数へ移す。

```agda
  module E = Extract F a sv dm using (toFun; toFun-graph; toFun-inj)
```

二つの述語が対象を記述する。`Mem p` は `p` が積 `prodL a` の要素であることを、`Comp p` は `p` が `a` の二つの要素 `x` と `y` に分解され、その順序対が `p` の基底集合に等しいことを述べる。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem p = ⟨ p .fst ∈ˢ (prodL a) .fst ⟩
  Comp : S → Type (ℓ-suc ℓ)
  Comp p = Σ[ x ∶ S ] Σ[ y ∶ S ]
             (⟨ x .fst ∈ˢ a .fst ⟩ × ⟨ y .fst ∈ˢ a .fst ⟩ × (p .fst ≡ pr (x .fst) (y .fst)))
```

積の要素の成分は一意であり、`isPropComp` がそれを証明する。第一射影は順序対の単射性によって同一視され、第二射影は内側の補題で比較される。

```agda
  isPropComp : (p : S) → isProp (Comp p)
  isPropComp p (x , y , _ , _ , e) (x' , y' , _ , _ , e') =
    Σ≡Prop inner (Σ≡Prop (λ v → (isL v) .snd) (pr-inj (sym e ∙ e') .fst))
    where
    inner : (x : S)
```

内側の補題は第二成分を比較する。同じ第一座標と対にされた候補 `y` と `y'` は等しくなる。対の等式がそれらの基底集合を同じ集合と同一視し、構成可能性と所属の成分は命題だからである。

```agda
          → isProp (Σ[ y ∶ S ] (⟨ x .fst ∈ˢ a .fst ⟩ × ⟨ y .fst ∈ˢ a .fst ⟩
                                × (p .fst ≡ pr (x .fst) (y .fst))))
    inner x (y , _ , _ , e) (y' , _ , _ , e') =
      Σ≡Prop (λ w → isProp× ((x .fst ∈ˢ a .fst) .snd)
                      (isProp× ((w .fst ∈ˢ a .fst) .snd) (setIsSet _ _)))
```

最後の成分は基底集合の相等によって処理され、一意性が完成する。`Comp p` は命題なので、切り詰められた存在は実際の分解へ消去できる。

```agda
        (Σ≡Prop (λ v → (isL v) .snd) (pr-inj (sym e ∙ e') .snd))
```

読み `comp` は、積の切り詰められた所属を実際の分解へ変える。その消去を許すのは、証明されたばかりの一意性である。そして値の写像 `val` が、`a` の各要素 `x` に対して、符号化された単射 `F` が割り当てる要素を計算する。

```agda
  comp : (p : S) → Mem p → Comp p
  comp p mp = rec₁ (isPropComp p) (λ z → z) (prodL-out a p mp)
  opaque
    val : (x : S) → ⟨ x .fst ∈ˢ a .fst ⟩ → S
    val x mx = E.toFun (x , mx)
```

グラフの補題は、計算された値が入力とともにグラフの内部で対にされることを証明する。すなわち `x` と `val x` の順序対が `F` に属するのである。この割り当ての記録は `a` のすべての要素について保たれる。

```agda
    val-graph : (x : S) (mx : ⟨ x .fst ∈ˢ a .fst ⟩)
              → ⟨ pr (x .fst) ((val x mx) .fst) ∈ F .fst ⟩
    val-graph x mx = E.toFun-graph (x , mx)
```

単射性の補題は、グラフの単射性を計算された値へ移す。`a` の二つの要素に割り当てられた値の基底集合が等しければ、要素そのものも等しいのである。これが、対の上の持ち上げられた写像を単射にする鍵である。

```agda
    val-inj : (x : S) (mx : ⟨ x .fst ∈ˢ a .fst ⟩) (x' : S) (mx' : ⟨ x' .fst ∈ˢ a .fst ⟩)
            → (val x mx) .fst ≡ (val x' mx') .fst → x .fst ≡ x' .fst
    val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')
```

持ち上げられた写像 `fn` は、積の要素に座標ごとに `F` を適用する。第一座標の像と第二座標の像の内部の順序対である。

```agda
  fn : (p : S) → Mem p → S
  fn p mp = prʟ (val (comp p mp .fst) (comp p mp .snd .snd .fst))
                (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
```

像は `b` の上の積の中に収まる。値域の節により二つの成分の値はともに `b` の要素であり、したがってその内部の対は `prodL b` に属する。内部の対と周囲の対の同一視は、みずからの第一射影の補題に沿って輸送される。

```agda
  into : (p : S) (mp : Mem p) → ⟨ (fn p mp) .fst ∈ˢ (prodL b) .fst ⟩
  into p mp =
    subst (λ w → ⟨ w ∈ˢ (prodL b) .fst ⟩) (sym (prʟ-fst (val x mx) (val y my)))
      (prodL-in b (val x mx) (val y my)
        (ran x (val x mx) (val-graph x mx)) (ran y (val y my) (val-graph y my)))
```

`p` の分解は座標 `x,y` と、`x ∈ a` および `y ∈ a` の証明を同時に与える。`val` は `a` の要素についてのみ定義されるため、これらの所属証明もデータの一部である。

```agda
    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
```

連鎖の型は、グラフの論理式が証明すべき内容をまとめる。`p` は `x` と `y` の対、`q` は `x'` と `y'` の対であり、`F` のグラフには二つの第一座標の対と二つの第二座標の対が含まれるのである。

```agda
  Chain : S → S → S → S → S → S → Type (ℓ-suc ℓ)
  Chain q p x y x' y' =
      (p .fst ≡ pr (x .fst) (y .fst)) × (q .fst ≡ pr (x' .fst) (y' .fst))
    × ⟨ pr (x .fst) (x' .fst) ∈ F .fst ⟩ × ⟨ pr (y .fst) (y' .fst) ∈ F .fst ⟩
```

グラフの論理式 `mapFo` は `x,y,x',y'` を存在量化し、`p=(x,y)`、`q=(x',y')`、および `F` の二つの適用という四つの主張を連言する。

```agda
  opaque
    mapFo : Formula S 2
    mapFo = ∃̇ (∃̇ (∃̇ (∃̇ (
          prAtL i5 i3 i2
       ∧̇ (prAtL i4 i1 i0
```

最後の二つの原子は適用の節である。`F` のグラフには第一座標どうしの対と第二座標どうしの対が含まれ、これはまさに、`F` が `x` を `x'` へ、`y` を `y'` へ写すということである。

```agda
       ∧̇ (appC F i3 i1
       ∧̇ appC F i2 i0))))))
```

妥当性は、具体的な六項目の文脈に対して確かめられる。四つの証人を新しいものから順に加え、対 `q` と対 `p` を続けた文脈であり、スロット 0 が `y'`、スロット 5 が `p` となって四つの原子の添字と一致する。

```agda
    private
      env₄ : S → S → S → S → S → S → Vec S 6
      env₄ q p x y x' y' = y' ∷ x' ∷ y ∷ x ∷ q ∷ p ∷ []
```

最初の妥当性の補題は `p` の対の原子を読む。文脈における対の原子の充足は、`p` の基底集合と `x`、`y` の順序対との間の等式である。

```agda
      at1 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i5 i3 i2 ⟩ ≡ (p .fst ≡ pr (x .fst) (y .fst))
      at1 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i5 i3 i2 (env₄ q p x y x' y'))
```

第二の妥当性の補題は、証人 `x'` と `y'` に対して `q` について同じことをする。この二つの等式が、連鎖の対の部分の錨である。

```agda
      at2 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i4 i1 i0 ⟩ ≡ (q .fst ≡ pr (x' .fst) (y' .fst))
      at2 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i4 i1 i0 (env₄ q p x y x' y'))
```

三つ目の妥当性の補題は第一の適用の原子を読む。`L` での充足は、二つの第一座標の対の `F` のグラフへの周囲の所属と同一視される。

```agda
      at3 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i3 i1 ⟩ ≡ ⟨ pr (x .fst) (x' .fst) ∈ F .fst ⟩
      at3 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i3 i1 (env₄ q p x y x' y'))
```

四つ目は第二座標に対して同じことをし、四つの原子のすべてが、集合の要素についての通常の主張へ翻訳される。

```agda
      at4 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i2 i0 ⟩ ≡ ⟨ pr (y .fst) (y' .fst) ∈ F .fst ⟩
      at4 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i2 i0 (env₄ q p x y x' y'))
```

外向きの方向は、四重に入れ子になった存在量化を順に消費し、切り詰められた連鎖を組み立てる。四つの証人と、周囲の読みへ輸送された四つの原子である。

```agda
    mapFo-out : (q p : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
              → ∥ Σ[ x ∶ S ] Σ[ y ∶ S ] Σ[ x' ∶ S ] Σ[ y' ∶ S ] Chain q p x y x' y' ∥₁
    mapFo-out q p = rec₁ squash₁ (λ { (x , hx) → rec₁ squash₁ (λ { (y , hy) →
      rec₁ squash₁ (λ { (x' , hx') → map₁ (λ { (y' , (h1 , (h2 , (h3 , h4)))) →
        x , y , x' , y'
```

各原子はみずからの妥当性のパスに沿って輸送されるため、連鎖が記録するのは充足の判断ではなく、通常の等式と通常の所属である。

```agda
        , ( transport (at1 q p x y x' y') h1 , transport (at2 q p x y x' y') h2
          , transport (at3 q p x y x' y') h3 , transport (at4 q p x y x' y') h4 ) })
        hx' }) hy }) hx })
```

内向きの方向は、連鎖から論理式を組み立て直す。四つの証人を入れ子の存在量化の証人として入れ、四つの原子を妥当性のパスに沿って逆向きに輸送する。

```agda
    mapFo-in : (q p x y x' y' : S) → Chain q p x y x' y' → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
    mapFo-in q p x y x' y' (h1 , h2 , h3 , h4) =
      ∣ x , ∣ y , ∣ x' , ∣ y'
      , ( transport (sym (at1 q p x y x' y')) h1
        , ( transport (sym (at2 q p x y x' y')) h2
```

最後の二つの適用原子が四つの主張からなる入れ子の連言を完成させ、`mapFo` の証人が得られる。

```agda
        , ( transport (sym (at3 q p x y x' y')) h3
          , transport (sym (at4 q p x y x' y')) h4 ))) ∣₁ ∣₁ ∣₁ ∣₁
```

一意性は、グラフの論理式が値を定めることを述べる。グラフの中で `p` と対にされる任意の `q` は、正準な像 `fn p mp` に等しくなる。証明は切り詰められた連鎖を対の等式の中で消費し、目標は h-集合における等式である。

```agda
  only : (p : S) (mp : Mem p) (q : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩ → q ≡ fn p mp
  only p mp q h = rec₁ (isSetS q (fn p mp)) step (mapFo-out q p h)
    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
```

要素 `p` の四つの成分には、像の補題と同じように一度名前が与えられ、一意性の計算がそれらを直接参照できる。

```agda
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
    e = comp p mp .snd .snd .snd .snd
```

連鎖の等式は `q` を `(x₁',y₁')` と書き、固定した分解は `p` を `(x,y)` と書く。単値性により `x₁'` は `val x` と、`y₁'` は `val y` と同一視されるので、`q` は正準な像 `(val x,val y)` である。

```agda
    step : Σ[ x₁ ∶ S ] Σ[ y₁ ∶ S ] Σ[ x₁' ∶ S ] Σ[ y₁' ∶ S ] Chain q p x₁ y₁ x₁' y₁'
         → q ≡ fn p mp
    step (x₁ , y₁ , x₁' , y₁' , (e₁ , e₂ , h3 , h4)) =
      Σ≡Prop (λ v → (isL v) .snd)
        (e₂ ∙ cong₂ pr ex ey ∙ sym (prʟ-fst (val x mx) (val y my)))
```

順序対の単射性が対の等式を二つに分ける。`x₁` の基底集合は `x` のそれに等しく、`y₁` の基底集合は `y` のそれに等しいのである。

```agda
      where
      x₁≡x : x₁ .fst ≡ x .fst
      x₁≡x = pr-inj (sym e₁ ∙ e) .fst
      y₁≡y : y₁ .fst ≡ y .fst
      y₁≡y = pr-inj (sym e₁ ∙ e) .snd
```

二つのグラフへの所属は、`F` の単値性を通して読まれる。`x₁` が `x` を名指すことが分かれば、`x₁` と対にされた項目の第一射影は、記録された値 `val x mx` と一致せざるを得ない。

```agda
      ex : x₁' .fst ≡ (val x mx) .fst
      ex = svAt-out zero (F ∷ a ∷ []) sv x x₁' (val x mx)
             (subst (λ w → ⟨ pr w (x₁' .fst) ∈ F .fst ⟩) x₁≡x h3) (val-graph x mx)
      ey : y₁' .fst ≡ (val y my) .fst
      ey = svAt-out zero (F ∷ a ∷ []) sv y y₁' (val y my)
```

第二座標もまったく同じように扱われ、みずからの所属と、みずからに記録された値が用いられる。

```agda
             (subst (λ w → ⟨ pr w (y₁' .fst) ∈ F .fst ⟩) y₁≡y h4) (val-graph y my)
```

したがって `mapFo` は座標ごとの像 `fn` を定義する。各積要素はこのグラフ値をもち、`into` がその値を `prodL b` に入れる。

```agda
  M : DefinableMap
  M = record
    { dom = prodL a ; cod = prodL b ; fn = fn ; into = into ; graph = mapFo
    ; defines = λ p mp →
        mapFo-in (fn p mp) p (comp p mp .fst) (comp p mp .snd .fst)
```

定義の節は連鎖であり、`p` の正準な像のところで実例化される。二つの値、積の要素の対の等式、そして二つのグラフの補題が、グラフが像とその入力について成り立つことを証明する。

```agda
          (val (comp p mp .fst) (comp p mp .snd .snd .fst))
          (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
          ( comp p mp .snd .snd .snd .snd
          , prʟ-fst _ _
          , val-graph (comp p mp .fst) (comp p mp .snd .snd .fst)
```

一意性定理により別のグラフ値はありえないため、この論理式は `prodL a` 上の実際の関数を表す。

```agda
          , val-graph (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst) )
    ; only = only }
```

持ち上げられた写像の単射性は直接証明される。像が基底集合として等しい二つの積の要素は、それ自身も等しくなければならない。証明は各要素をその成分から組み立て直す。

```agda
  inj : (p : S) (mp : Mem p) (p' : S) (mp' : Mem p')
      → (fn p mp) .fst ≡ (fn p' mp') .fst → p .fst ≡ p' .fst
  inj p mp p' mp' e = e₀ ∙ cong₂ pr ex ey ∙ sym e₀'
    where
    x = comp p mp .fst
```

二つの要素の成分にはそれぞれ一度名前が与えられ、二つの分解を座標ごとに比較できる。

```agda
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
    e₀ = comp p mp .snd .snd .snd .snd
    x' = comp p' mp' .fst
```

仮定された像の相等は内部の対の相等であり、その単射性がそれを、第一の像どうしの相等と第二の像どうしの相等に分ける。

```agda
    y' = comp p' mp' .snd .fst
    mx' = comp p' mp' .snd .snd .fst
    my' = comp p' mp' .snd .snd .snd .fst
    e₀' = comp p' mp' .snd .snd .snd .snd
    q : ((val x mx) .fst ≡ (val x' mx') .fst) × ((val y my) .fst ≡ (val y' my') .fst)
```

各成分の等式は値の写像の単射性に渡され、第一座標の相等と第二座標の相等が得られる。対の等式の二つの座標はこれらに沿って輸送される。

```agda
    q = pr-inj (sym (prʟ-fst (val x mx) (val y my)) ∙ e ∙ prʟ-fst (val x' mx') (val y' my'))
    ex : x .fst ≡ x' .fst
    ex = val-inj x mx x' mx' (q .fst)
    ey : y .fst ≡ y' .fst
    ey = val-inj y my y' my' (q .snd)
```

定義可能な写像とその単射性が内部の単射として組み上がる。`L` の内部で `prodL a` は `prodL b` へ単射する。

```agda
  injL : InjL (prodL a) (prodL b)
  injL = Inj.injL M inj
```

</div>
</details>

`InjL` は命題的に切り詰められているため、グラフを大域的に選ばずに符号化された単射 `a ↪ b` を持ち上げられる。

```agda
prod-inj : (a b : S) → InjL a b → InjL (prodL a) (prodL b)
prod-inj a b = rec₁ squash₁
  (λ { (F , sv , dm , ij , ran) → ProdMap.injL a b F sv dm ij ran })
```

## 無限基数の平方律

無限順序数に加わる頂点を吸収するには、その後続をもとの順序数へ単射すれば十分である。

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

```agda
module Shift (mL : S) (om : IsOrd (mL .fst)) (m∉ω : ⟨ mL .fst ∈ˢ ω ⟩ → ⊥₀) where
```

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

`mL` の基底にある順序数を `m` と書く。所属と有限性の判定はこの集合について行い、`mL` はそれが `L` の要素である証拠を保持する。

```agda
  private
    m : V ℓ
    m = mL .fst
```

移し変えの定義域は内部の後続 `D = sucʟ mL` である。`L` の内部での順序数の後続であり、`m` の要素と `m` 自身の両方を含む。

```agda
    D : S
    D = sucʟ mL
```

`L` の二つの要素の相等は、その基底集合の相等である。構成可能性の成分は命題だからである。この小さな等式は、移し変えの内部のあらゆる同一視で使われる。

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

`m` は無限なので、`ω` のすべての要素は `m` に属する。この包含は計数の事実から引用されたもので、有限の要素の後続が `m` の内側にとどまる理由でもある。

```agda
    ω⊆m : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ m ⟩
    ω⊆m = ω⊆ m om m∉ω
```

移し変えの定義域への所属を述べ、最初の判定を定義する。要素は `ω` に属するか、その所属が反証されるかのいずれかである。これは排中律が与える明示的な判定である。

```agda
    Mem : S → Type (ℓ-suc ℓ)
    Mem x = ⟨ x .fst ∈ˢ D .fst ⟩
    Fin? : S → Type (ℓ-suc ℓ)
    Fin? x = Dec ⟨ x .fst ∈ˢ ω ⟩
```

第二の判定は後続の要素を分ける。`sucʟ mL` の要素は `m` に属するか `m` と等しいかであり、これが後続への所属の意味そのものである。

```agda
    Top? : S → Type (ℓ-suc ℓ)
    Top? x = ⟨ x .fst ∈ˢ m ⟩ ⊎ (x .fst ≡ m)
```

最初の判定は排中律の一つの実例であり、`x` の `ω` への所属の命題に適用される。

```agda
    fin? : (x : S) → Fin? x
    fin? x = FOL.Semantics.decideMembership 𝒮ᵥ lem (x .fst) ω
```

第二の判定も排中律の実例であり、後続の消去によって洗練される。`sucʟ mL` の要素は `m` に属するか `m` と等しいかであり、所属が反証されれば等しいことだけが残る。

```agda
    top? : (x : S) → Mem x → Top? x
    top? x h = go (FOL.Semantics.decideMembership 𝒮ᵥ lem (x .fst) m)
      where
      go : Dec ⟨ x .fst ∈ˢ m ⟩ → Top? x
      go (yes k) = inl k
```

反証された場合では、消去が後続の切り詰められた所属を消費する。二つの結果は排他的である。ある要素が `m` に属し、かつ `m` に等しいことはあり得ない。それは `m` がみずからに属することになり、所属の非反射性によって退けられるからである。

```agda
      go (no nk) = inr (∈sucV-elim {A = m} {x = x .fst} (setIsSet (x .fst) m)
        (subst (λ w → ⟨ x .fst ∈ˢ w ⟩) (sucʟ-fst mL) h) (λ k → ⊥₀-rec (nk k)) (λ q → q))
    not-both : (x : S) → ⟨ x .fst ∈ˢ m ⟩ → x .fst ≡ m → ⊥₀
    not-both x k q = ∈-irrefl m (subst (λ w → ⟨ w ∈ˢ m ⟩) q k)
```

有限の場合と頂点の場合は重ならない。`x` が `ω` に属し、しかも `m` に等しいなら、その等しさに沿って所属を移送することで `m ∈ ω` が得られ、`m` が無限であるという仮定に反する。

```agda
    ω-fin : (x : S) → ⟨ x .fst ∈ˢ ω ⟩ → x .fst ≡ m → ⊥₀
    ω-fin x k q = m∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) q k)
```

後続が空集合になることはない。実際、`a` は `sucV a` に属する。もし `sucV a = ∅` なら、この所属を等しさに沿って移送することで、空集合の要素が得られてしまう。

```agda
    suc≢∅ : (a : V ℓ) → sucV a ≡ ∅ → ⊥₀
    suc≢∅ a e = ∅-empty a
      (∈∈ₛ {a = a} {b = ∅} .fst (subst (λ w → ⟨ a ∈ˢ w ⟩) e (self∈sucV a)))
```

三つの場合が、移し変えの値を定義する。有限の要素はみずからの内部の後続へ送られ、`m` の非有限の要素はみずからへ送られ、頂点の要素 `m` は `L` の空集合へ送られる。これらは、二つの判定が区別する三つの選択肢にほかならない。

```agda
    value : (x : S) → Fin? x → Top? x → S
    value x (yes _) _       = sucʟ x
    value x (no _) (inl _) = x
    value x (no _) (inr _) = ∅ʟ
```

値は `m` の中に収まることが保証される。有限の要素については、その後続が極限の性質によって `ω` の要素となり、`ω` は `m` に含まれる。`m` の要素については、所属がその判定そのものであり、空集合は `ω` の、したがって `m` の要素である。

```agda
    value-in : (x : S) (f : Fin? x) (t : Top? x) → ⟨ (value x f t) .fst ∈ˢ m ⟩
    value-in x (yes k) _ =
      subst (λ w → ⟨ w ∈ˢ m ⟩) (sym (sucʟ-fst x)) (ω⊆m (sucV (x .fst)) (ω-limit (x .fst) k))
    value-in x (no _) (inl k) = k
    value-in x (no _) (inr _) = ω⊆m ∅ (#∈ω zero)
```

グラフの論理式の証人の型が宣言される。`x` が有限で `y` はその後続、`x` が非有限で `m` に属し `y` は `x` に等しい、あるいは `x` が頂点 `m` に等しく `y` は空である、の三つの選択肢である。三つは切り詰めの下にあり、それぞれがみずからの所属と等式を運ぶ。

```agda
    Wit : (y x : S) → Type (ℓ-suc ℓ)
    Wit y x = ∥ (⟨ x .fst ∈ˢ ω ⟩ × (y .fst ≡ sucV (x .fst)))
              ⊎ ( ((⟨ x .fst ∈ˢ ω ⟩ → ⊥₀) × ⟨ x .fst ∈ˢ m ⟩ × (y .fst ≡ x .fst))
                ⊎ ((x .fst ≡ m) × (y .fst ≡ ∅)) ) ∥₁
```

グラフの論理式は対象言語で述べられる。その第一の選言肢は、`x` が内部の `ω` に属し `y` がその後続であることを、後続の節によって読み取る。第二の選言肢はまず、`x` が有限であることを否定する。

```agda
  opaque
    graph : Formula S 2
    graph = ((var (suc zero) ∈̇ con ωʟ) ∧̇ sucAtL (suc zero) zero)
          ∨̇ ( ( (¬̇ (var (suc zero) ∈̇ con ωʟ))
              ∧̇ ((var (suc zero) ∈̇ con mL) ∧̇ (var zero ≐ var (suc zero))) )
```

その内側の二つの守られた選択肢が第二と第三の選言肢を完成させる。`m` の非有限の要素はみずからと対にされ、頂点の要素は `L` の空集合と対にされる。

```agda
            ∨̇ ((var (suc zero) ≐ con mL) ∧̇ (var zero ≐ con ∅ʟ)) )
```

後続の節の妥当性が一度記録される。二項目の文脈での後続の原子の充足は、`y` と周囲の後続 `sucV x` との間の等式である。

```agda
    private
      sa : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ sucAtL (suc zero) zero ⟩ ≡ (y .fst ≡ sucV (x .fst))
      sa y x = cong ⟨_⟩ (sucAtL-adequate (suc zero) zero (y ∷ x ∷ []))
```

論理式を外向きに読むと、命題的切り詰めの下の論理和を、やはり命題である証人型へ除去する。後続の節は妥当性によって変換し、中間の節の反証は命題リサイズによって持ち上げられた宇宙から必要なレベルへ戻す。頂点の節はすでに必要な形である。

```agda
    graph-out : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → Wit y x
    graph-out y x = rec₁ squash₁
      (λ { (inl (k , e)) → ∣ inl (k , transport (sa y x) e) ∣₁
         ; (inr h) → map₁ (λ { (inl (n , (k , e))) →
                                  inr (inl ((λ hx → lower (n hx)) , k , e))
```

第三の選言肢は頂点の場合の二つの等式だけを運ぶので、その翻訳は直接である。

```agda
                              ; (inr (q , e)) → inr (inr (q , e)) }) h })
```

三つの内向きの補題が、それぞれの証人から論理式を組み立て直す。有限の要素では、後続の等式が妥当性に沿って逆向きに輸送され、第一の選言肢に入る。

```agda
    in-fin : (y x : S) → ⟨ x .fst ∈ˢ ω ⟩ → y .fst ≡ sucV (x .fst) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-fin y x k e = ∣ inl (k , transport (sym (sa y x)) e) ∣₁
```

`m` の非有限な要素については、`x ∈ ω` の反証を対象レベルの否定へ持ち上げる。これを `x ∈ m` および `y = x` と合わせると、中間の選言肢が得られる。

```agda
    in-mid : (y x : S) → (⟨ x .fst ∈ˢ ω ⟩ → ⊥₀) → ⟨ x .fst ∈ˢ m ⟩ → y .fst ≡ x .fst
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-mid y x n k e = ∣ inr ∣ inl ((λ hx → lift (n hx)) , (k , e)) ∣₁ ∣₁
```

頂点の要素では、頂点の場合の二つの等式が第三の選言肢に直接組み立てられる。

```agda
    in-top : (y x : S) → x .fst ≡ m → y .fst ≡ ∅ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-top y x q e = ∣ inr ∣ inr (q , e) ∣₁ ∣₁
```

移し変えの関数は、二つの判定を通して定義される。判定が入力を分類する仕方に応じて、値は後続、要素そのもの、あるいは空集合である。

```agda
  private
    fn : (x : S) → Mem x → S
    fn x h = value x (fin? x) (top? x h)
```

定義の節は三つの場合すべてで確かめられる。有限の場合は後続の等式を引用し、中間の場合は定義的であり、頂点の場合は空集合と頂点の要素を対にする。

```agda
    defines' : (x : S) (f : Fin? x) (t : Top? x) → ⟨ (value x f t ∷ x ∷ []) ⊨ graph ⟩
    defines' x (yes k) _       = in-fin (sucʟ x) x k (sucʟ-fst x)
    defines' x (no n) (inl k) = in-mid x x n k refl
    defines' x (no n) (inr q) = in-top ∅ʟ x q refl
```

一意性はグラフを逆向きに読む。グラフの中で `x` と対にされる任意の `y` は、選ばれた値に等しくなる。証明は切り詰められた選言を、h-集合における等式という目標の中へ消費する。

```agda
    only' : (x : S) (f : Fin? x) (t : Top? x) (y : S)
          → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ value x f t
    only' x f t y hy = rec₁ (isSetS y (value x f t)) (go f t) (graph-out y x hy)
      where
      go : (f : Fin? x) (t : Top? x)
```

場合分けの関数は、展開された選択肢と選ばれた判定を受け取る。有限の場合に有限の肯定が組になるとき、後続の等式と内部の対の等式は、後続の第一射影の同定に沿って輸送されれば一致する。

```agda
         → (⟨ x .fst ∈ˢ ω ⟩ × (y .fst ≡ sucV (x .fst)))
           ⊎ ( ((⟨ x .fst ∈ˢ ω ⟩ → ⊥₀) × ⟨ x .fst ∈ˢ m ⟩ × (y .fst ≡ x .fst))
             ⊎ ((x .fst ≡ m) × (y .fst ≡ ∅)) )
         → y ≡ value x f t
      go (yes k) _       (inl (_ , e))             = S≡ (e ∙ sym (sucʟ-fst x))
```

続く五つの節では、選ばれた有限の場合または非有限な要素の場合を、グラフの証人と照合する。有限という選択は、中間の証人に含まれる反証とも頂点の等式とも矛盾する。非有限な要素という選択は、有限の証人とは矛盾し、中間の証人とはその等式によって一致し、`m` の要素は `m` 自身に等しくなれないことから頂点の証人を排除する。

```agda
      go (yes k) _       (inr (inl (n , _ , _)))   = ⊥₀-rec (n k)
      go (yes k) _       (inr (inr (q , _)))       = ⊥₀-rec (ω-fin x k q)
      go (no n) (inl k) (inl (k' , _))            = ⊥₀-rec (n k')
      go (no n) (inl k) (inr (inl (_ , _ , e)))   = S≡ e
      go (no n) (inl k) (inr (inr (q , _)))       = ⊥₀-rec (not-both x k q)
```

選ばれた入力が頂点なら、有限の証人はその非有限性と矛盾し、中間の証人は `m` の要素が `m` 自身に等しくなれないことと矛盾する。頂点の証人からは、空集合を値とする等式によって必要な等しさが直接得られる。

```agda
      go (no n) (inr q) (inl (k' , _))            = ⊥₀-rec (n k')
      go (no n) (inr q) (inr (inl (_ , k , _)))   = ⊥₀-rec (not-both x k q)
      go (no n) (inr q) (inr (inr (_ , e)))       = S≡ e
```

以上のデータにより、`sucʟ mL` から `mL` への定義可能な関数が定まる。各入力には `m` に属するシフト値が割り当てられ、上の論理式がそのグラフになる。

```agda
    M : DefinableMap
    M = record
      { dom = D ; cod = mL ; fn = fn
      ; into = λ x h → value-in x (fin? x) (top? x h)
      ; graph = graph
```

排中律は各入力について二つの判定を与える。先の存在性と一意性の議論により、このグラフがちょうど選ばれた値について成り立つことが分かる。

```agda
      ; defines = λ x h → defines' x (fin? x) (top? x h)
      ; only = λ x h → only' x (fin? x) (top? x h) }
```

単射性は、二つの入力について場合を比較して証明する。両方が有限なら、シフト後の値の等しさはそれぞれの後続の等しさなので、順序数の後続の単射性から元の二つの順序数が等しいと分かる。

```agda
    inj' : (x : S) (f : Fin? x) (t : Top? x) (x' : S) (f' : Fin? x') (t' : Top? x')
         → (value x f t) .fst ≡ (value x' f' t') .fst → x .fst ≡ x' .fst
    inj' x (yes k) _ x' (yes k') _ e =
      ord-suc-inj (x .fst) (x' .fst) (mem-ord {A = ω} ω-ord (x .fst) k)
        (sym (sucʟ-fst x) ∙ e ∙ sucʟ-fst x')
```

有限な入力が非有限な要素と同じシフト値をもつことはない。その等しさから、後者の値、したがって後者自身が `ω` に属することになるからである。頂点の入力とも値を共有できない。そうすると後続が空集合に等しくなってしまう。

```agda
    inj' x (yes k) _ x' (no n') (inl _) e =
      ⊥₀-rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x) ∙ e) (ω-limit (x .fst) k)))
    inj' x (yes k) _ x' (no n') (inr _) e =
      ⊥₀-rec (suc≢∅ (x .fst) (sym (sucʟ-fst x) ∙ e))
    inj' x (no n) (inl _) x' (yes k') _ e =
```

有限と非有限の順序を逆にした場合も、同じ矛盾になる。二つの非有限な要素は、値が等しければ直ちに等しくなる。一方、非有限な要素は頂点と同じ値をもてない。空集合に等しければ `ω` に属することになるからである。

```agda
      ⊥₀-rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x') ∙ sym e) (ω-limit (x' .fst) k')))
    inj' x (no n) (inl _) x' (no n') (inl _) e = e
    inj' x (no n) (inl _) x' (no n') (inr _) e =
      ⊥₀-rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym e) (#∈ω zero)))
    inj' x (no n) (inr _) x' (yes k') _ e =
```

頂点の入力について、有限な入力の値と等しければ後続が空集合になり、非有限な要素の値と等しければその要素が空集合、したがって有限な順序数になってしまう。両方の入力が頂点なら、それぞれを `m` と結ぶ等式から両者が等しいと分かる。したがって、このシフトは `L` の内部で単射である。

```agda
      ⊥₀-rec (suc≢∅ (x' .fst) (sym (sucʟ-fst x') ∙ sym e))
    inj' x (no n) (inr _) x' (no n') (inl _) e =
      ⊥₀-rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (#∈ω zero)))
    inj' x (no n) (inr q) x' (no n') (inr q') e = q ∙ sym q'
  injL : InjL (sucʟ mL) mL
```

定義可能なシフトと先の分類により、符号化された単射 `sucʟ mL ↪ mL` が得られる。さらに、ある集合の二つの要素が同じファイバー添字で表されるなら両者は等しい、という基本的な事実を用いる。添字の等しさに提示写像を作用させると、表された要素の等しさが復元される。

```agda
  injL = Inj.injL M (λ x h x' h' → inj' x (fin? x) (top? x h) x' (fin? x') (top? x' h'))
```

</div>
</details>

```agda
opaque
  fiber-inj : (g : V ℓ) {x y : V ℓ} (mx : ⟨ x ∈ˢ g ⟩) (my : ⟨ y ∈ˢ g ⟩)
            → fiber g mx .fst ≡ fiber g my .fst → x ≡ y
  fiber-inj g mx my e = sym (fiber g mx .snd) ∙ cong ⟪ g ⟫↪ e ∙ fiber g my .snd
```

構成可能な無限順序数 `a` が内部の基数でもあるとき、帰納目標はその直積平方 `a × a` から `a` への符号化された単射である。この主張を `Goal a` としてまとめることで、所属に関する帰納法を `a` より下の対象へ一様に適用できる。

```agda
Goal : V ℓ → Type (ℓ-suc ℓ)
Goal a = (la : ⟨ isL a ⟩) → IsOrd a → IsCardinalL (a , la)
       → (⟨ a ∈ˢ ω ⟩ → ⊥₀) → InjL (prodL (a , la)) (a , la)
```

帰納の段階は、集合 `a`、`a` の各要素に対する帰納仮定、そして四つの仮定を受け取る。構成可能性、順序数性、内部の基数性、無限性である。基数性の仮定は、`κ` がみずからの要素へ内部的に単射することを排除するもので、崩壊の計数が用いる形そのものである。

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

```agda
module Step (a : V ℓ) (ih : (a' : V ℓ) → ⟨ a' ∈ˢ a ⟩ → Goal a')
            (la : ⟨ isL a ⟩) (oa : IsOrd a) (carda : IsCardinalL (a , la))
            (a∉ω : ⟨ a ∈ˢ ω ⟩ → ⊥₀) where
```

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

台となる順序数が `a` である構成可能集合を `κ` と書く。これにより、内部の構成を行うたびに、周囲の順序数のデータとそれが `L` に属することの証明を一緒に扱える。

```agda
  κ : S
  κ = a , la
```

ここから、Gödel 順序を備えた `κ × κ` と、その整列順序を崩壊して得られる順序数を考える。目標は、この崩壊の各始切片がなお `κ` より下に抑えられることを示すことである。

```agda
  open Order κ oa
  open Coll κ oa
```

順序数 `a` は有限順序数ではないので、すべての有限順序数を含む。さらに後続について閉じていることが必要である。`m ∈ a` に対し、三分法は `sucV m` が `a` より下、`a` と等しい、または `a` より上のいずれかであるとする。続く場合分けで後二者を排除する。

```agda
  ω⊆a : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
  ω⊆a = ω⊆ a oa a∉ω
  suc∈ : (m : V ℓ) → ⟨ m ∈ˢ a ⟩ → ⟨ sucV m ∈ˢ a ⟩
  suc∈ m m∈a = go (ord-tri (sucV m) (suc-ord om) a oa)
    where
```

`m` は順序数 `a` の要素なので、それ自身も順序数である。また、構成可能集合 `a` に属することから `m` も構成可能であり、内部の論域の要素 `mL` を定める。

```agda
    om : IsOrd m
    om = mem-ord {A = a} oa m m∈a
    mL : S
    mL = ordL m om
```

`sucV m` と `a` に三分法を適用する。第一の場合は、求める所属そのものである。`sucV m = a` なら、さらに `m` と `ω` を比較することで、矛盾を有限の場合と、続いて扱う二つの無限の場合に分ける。

```agda
    go : ⟨ sucV m ∈ˢ a ⟩ ⊎ ((sucV m ≡ a) ⊎ ⟨ a ∈ˢ sucV m ⟩) → ⟨ sucV m ∈ˢ a ⟩
    go (inl h) = h
    go (inr (inl e)) = ⊥₀-rec (fin (ord-tri m om ω ω-ord))
      where
      fin : ⟨ m ∈ˢ ω ⟩ ⊎ ((m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩) → ⊥₀
```

`m` が `ω` の要素なら、その後続も `ω` の要素となり、基数 `a` が `ω` の内側に入って無限性の仮定と矛盾する。`m` が `ω` に等しいか `ω` を含む場合は、要素 `m` のところで `a` の内部の基数性を適用すると、移し変えの単射 `sucʟ mL ↪ mL`、すなわち基数のある要素への内部の単射が退けられる。

```agda
      fin (inl m∈ω) = a∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (ω-limit m m∈ω))
      fin (inr r) =
        carda mL m∈a (subst (λ w → InjL w mL) sucL≡κ (Shift.injL mL om m∉ω))
        where
        m∉ω : ⟨ m ∈ˢ ω ⟩ → ⊥₀
```

局所的な非有限性は、同じ三分法から読み取られる。`m` が `ω` に等しいなら、仮定された所属が `ω` をみずからの内側に置き、`ω` が `m` に属するなら、推移性が再び `ω` をみずからの内側に置く。どちらも所属の非反射性と矛盾する。

```agda
        m∉ω h = rr r
          where
          rr : (m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩ → ⊥₀
          rr (inl e') = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e' h)
          rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
```

等式 `sucV m = a` は内部の後続 `sucʟ mL` を `κ` と同一視するので、シフトから、基数性に反する `κ` から `m` への単射が得られる。三分法の残る場合では、`a ∈ sucV m` は `a ∈ m` または `a = m` を意味する。どちらからも順序数の自己所属が導かれるため、不可能である。

```agda
        sucL≡κ : sucʟ mL ≡ κ
        sucL≡κ = Σ≡Prop (λ v → (isL v) .snd) (sucʟ-fst mL ∙ e)
    go (inr (inr h)) = ⊥*-rec
      (∈sucV-elim {A = m} {x = a} {P = ⊥* {ℓ-suc ℓ}} isProp⊥* h
        (λ a∈m → lift (∈-irrefl a (oa .fst a∈m m∈a)))
```

後続についての閉性が得られたので、以下で必要となるより小さい順序数に帰納仮定を適用できる。より一般に、無限順序数 `γ` が `a` より下にあるなら、`γ` の内部基数代表を選び、その代表に帰納仮定を適用して `prodL γ ↪ γ` を得る。

```agda
        (λ a≡m → lift (∈-irrefl m (subst (λ w → ⟨ m ∈ˢ w ⟩) a≡m m∈a))))
  prod-into : (γ : S) → IsOrd (γ .fst) → ⟨ γ .fst ∈ˢ a ⟩
            → (⟨ γ .fst ∈ˢ ω ⟩ → ⊥₀) → InjL (prodL γ) γ
  prod-into γ oγ γ∈a γ∉ω = rec₁ squash₁ build (cardOf γ oγ)
    where
```

基数の代表は、切り詰められた形でデータを渡す。順序数 `μ` は内部の基数であり `γ` に含まれ、`γ` から `μ` へ、`μ` から `γ` への単射が伴う。関数 `build` はこのデータを積の単射へ変える。

```agda
    build : Σ[ μ ∶ S ]
              ( IsOrd (μ .fst) × IsCardinalL μ
              × ((z : V ℓ) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ γ .fst ⟩)
              × InjL γ μ × InjL μ γ )
          → InjL (prodL γ) γ
```

単射は三つの単射を合成する。積の単射が `γ ↪ μ` を座標ごとに持ち上げ、帰納仮定が内部の基数 `μ` において適用されて `prodL μ ↪ μ` を与え、さらに `μ ↪ γ` によって結果が `γ` の中へ合成される。

```agda
    build (μ , oμ , cardμ , μ⊆γ , γ↪μ , μ↪γ) =
      injl-trans (prodL γ) (prodL μ) γ (prod-inj γ μ γ↪μ)
        (injl-trans (prodL μ) μ γ (ih (μ .fst) μ∈a (μ .snd) oμ cardμ μ∉ω) μ↪γ)
      where
      μ∈a : ⟨ μ .fst ∈ˢ a ⟩
```

代表 `μ` も `a` より下にある。`μ ∈ γ` なら、`γ ∈ a` と推移性から `μ ∈ a` が従う。`μ = γ` なら、所属をその等しさに沿って移送する。残る `γ ∈ μ` は不可能である。包含 `μ ⊆ γ` によって `γ ∈ γ` が導かれるからである。

```agda
      μ∈a = go (ord-tri (μ .fst) oμ (γ .fst) oγ)
        where
        go : ⟨ μ .fst ∈ˢ γ .fst ⟩ ⊎ ((μ .fst ≡ γ .fst) ⊎ ⟨ γ .fst ∈ˢ μ .fst ⟩) → ⟨ μ .fst ∈ˢ a ⟩
        go (inl h)       = oa .fst h γ∈a
        go (inr (inl e)) = subst (λ w → ⟨ w ∈ˢ a ⟩) (sym e) γ∈a
```

代表 `μ` も無限でなければならない。もし `μ ∈ ω` なら、無限順序数 `γ` に対する `ω ↪ γ` と `γ ↪ μ` を合成して、`ω` を有限順序数 `μ` へ単射できてしまう。これは不可能である。後で用いるため、`Seg p b` は `r ≺ p` であり崩壊値が `b` である先行者 `r` を記録する。

```agda
        go (inr (inr h)) = ⊥₀-rec (∈-irrefl (γ .fst) (μ⊆γ (γ .fst) h))
      μ∉ω : ⟨ μ .fst ∈ˢ ω ⟩ → ⊥₀
      μ∉ω h = no-fin γ μ oγ γ∉ω oμ h γ↪μ
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∶ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))
```

節は一意である。崩壊の値が等しい `p` の二つの先行者は等しくなる。崩壊の写しは添字の上で単射であり、この命題が以降の消去のために一度記録される。

```agda
  isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b)
  isPropSeg p b (r , _ , e) (r' , _ , e') =
    Σ≡Prop (λ r → isProp× (OT.isProp≺ r p) (setIsSet _ _)) (I.col-inj r r' (e ∙ sym e'))
```

崩壊の値のすべての要素は、崩壊の外向きの読みと証明されたばかりの一意性によって、その節を確定する。ついで対の最大値が名指される。その二つの座標のホストの順序における大きい方である。

```agda
  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = rec₁ (isPropSeg p b) (λ z → z) (C.col-out p b h)
  mx : OT.Dom → ⟪ K ⟫
  mx p = maxOrd (φ p .fst) (φ p .snd)
```

`p` の二つの座標の最大値が表す周囲の順序数を `mV p` とする。崩壊された Gödel 順序で `r ≺ p` なら、`r` の第一座標はこの最大値の後続より下にある。これは Gödel 順序が与える第一座標の上界である。

```agda
  mV : OT.Dom → V ℓ
  mV p = ↑ (mx p)
  opaque
    seg-fst : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ sucV (mV p) ⟩
    seg-fst p r k = fst∈suc (φ r) (φ p) (≺-fwd r p k)
```

すべての `r ≺ p` について、第二座標も同じ上界を満たす。そこで `gfin p = sucV (mV p)` を両座標に共通の台として用いる。有限の場合の仮定 `mV p ∈ ω` のもとでは、この台自身も有限順序数である。

```agda
    seg-snd : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ sucV (mV p) ⟩
    seg-snd p r k = snd∈suc (φ r) (φ p) (≺-fwd r p k)
  gfin : OT.Dom → V ℓ
  gfin p = sucV (mV p)
  opaque
```

各先行者 `r ≺ p` について、二つの座標の上界から `gfin p` の提示における二つの添字が選ばれ、`h p r` はその順序対である。`mV p` が有限なら、この対は `r` を有限順序数の平方の中に符号化する。

```agda
    h : (p r : OT.Dom) (k : r OT.≺ p) → ⟪ gfin p ⟫ × ⟪ gfin p ⟫
    h p r k = fiber (gfin p) (seg-fst p r k) .fst , fiber (gfin p) (seg-snd p r k) .fst
```

二つの符号 `h p r` と `h p r'` が等しければ、その等しさに第一射影を作用させることで、第一の添字が等しいと分かる。これは符号から `r` の座標を復元する前半である。

```agda
    h-fst : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k'
          → fiber (gfin p) (seg-fst p r k) .fst
          ≡ fiber (gfin p) (seg-fst p r' k') .fst
    h-fst p r r' k k' e = cong (λ p → p .fst) e
```

同じ符号の等しさに第二射影を作用させると、第二の添字も等しいと分かる。したがって、ファイバー対の等しさは二つの成分をそれぞれ決定する。

```agda
    h-snd : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k'
          → fiber (gfin p) (seg-snd p r k) .fst
          ≡ fiber (gfin p) (seg-snd p r' k') .fst
    h-snd p r r' k k' e = cong (λ p → p .snd) e
```

第一のファイバー添字が等しければ、それらのファイバーが表す周囲の順序数も等しくなる。`K` の提示写像は単射なので、第一座標 `φ r .fst` と `φ r' .fst` が等しいと従う。

```agda
  step-e1 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k' → φ r .fst ≡ φ r' .fst
  step-e1 p r r' k k' e =
    ↪-inj {a = K} (fiber-inj (gfin p) (seg-fst p r k) (seg-fst p r' k') (h-fst p r r' k k' e))
```

第二の移送の補題は第二の座標についても同じことをし、ファイバーの対の相等がもとの対の両座標を確定する。崩壊の有限の場合に必要なのはまさにこれである。

```agda
  step-e2 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k' → φ r .snd ≡ φ r' .snd
  step-e2 p r r' k k' e =
    ↪-inj {a = K} (fiber-inj (gfin p) (seg-snd p r k) (seg-snd p r' k') (h-snd p r r' k k' e))
```

二つのファイバー対の符号が等しければ、`φ r` と `φ r'` の二つの座標はそれぞれ等しくなる。対の外延性でこれらの座標の等しさをまとめ、さらに `φ` の単射性を用いると `r = r'` が得られる。したがって、`p` の先行者の符号化は単射である。示すべき有限の場合は、`p` の最大座標が `ω` に属するなら `C.col p` も `ω` に属する、という主張である。

```agda
  step-inj : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
           → h p r k ≡ h p r' k' → r ≡ r'
  step-inj p r r' k k' e =
    φ-inj r r' (pair≡ (step-e1 p r r' k k' e) (step-e2 p r r' k k' e))
  col-fin : (p : OT.Dom) → ⟨ mV p ∈ˢ ω ⟩ → ⟨ C.col p ∈ˢ ω ⟩
```

証明は三分法によって崩壊の値と `ω` を比較し、まず有限の台に名前を与える。`g` は `p` の周囲の最大値の後続であり、すべての先行者の二つの座標が収まると示された集合である。

```agda
  col-fin p m∈ω = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
    where
    g : V ℓ
    g = sucV (mV p)
    og : IsOrd g
```

`mV p ∈ ω` なので、この最大値は順序数であり、その後続 `g` も順序数である。`ω` の極限性から `g ∈ ω` が従うため、`g` は有限順序数である。これらは、`ω` から `g × g` への単射を排除するために必要な仮定である。

```agda
    og = suc-ord (ω-mem-ord (mV p) m∈ω)
    g∈ω : ⟨ g ∈ˢ ω ⟩
    g∈ω = ω-limit (mV p) m∈ω
```

反証は、`ω` が崩壊の値に含まれると仮定する。すると `ω` のすべての添字が `col p` の節を名指す。包含が名指された要素を崩壊の内側に置き、節の補題が先行者を復元するのである。

```agda
    refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → ⊥₀
    refute sub = finite-excl-ω g og g∈ω f f-inj
      where
      s : (x : ⟪ ω ⟫) → Seg p (⟪ ω ⟫↪ x)
      s x = seg p (⟪ ω ⟫↪ x) (sub (⟪ ω ⟫↪ x) (member ω x))
```

各 `x ∈ ω` に対し、崩壊値が `x` である `p` の一意な先行者を `s x` とする。写像 `f` は `x` を、その先行者の二つの座標を符号化するファイバー添字の対、したがって有限な平方 `g × g` の要素へ送る。このような符号が等しければ、もとの `ω` の要素も等しいことを示せばよいのである。

```agda
      f : ⟪ ω ⟫ → ⟪ g ⟫ × ⟪ g ⟫
      f x = h p (s x .fst) (s x .snd .fst)
      f-inj : (x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y
      f-inj x y e = ↪-inj {a = ω}
        (sym (s x .snd .snd)
```

単射性は三つの等式の合成として証明される。`x` の節の崩壊の値は `x` に等しく、二つの節は証明されたばかりの有限の場合の単射によって先行者として一致し、`y` の節の崩壊の値は `y` に等しい。合成すると、`x` と `y` が一致することが迫られる。

```agda
         ∙ cong C.col (step-inj p (s x .fst) (s y .fst) (s x .snd .fst) (s y .snd .fst) e)
         ∙ s y .snd .snd)
```

これで三分法から `C.col p ∈ ω` が従う。`C.col p = ω` なら、すでに排除した包含 `ω ⊆ C.col p` が得られる。`ω ∈ C.col p` の場合も、順序数 `C.col p` の推移性から同じ包含が得られる。一般の逆崩壊を構成するため、先行者の上界 `p` と構成可能な台 `g` を固定する。

```agda
    go : ⟨ C.col p ∈ˢ ω ⟩ ⊎ ((C.col p ≡ ω) ⊎ ⟨ ω ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ ω ⟩
    go (inl k)         = k
    go (inr (inl e))   = ⊥₀-rec (refute (λ z z∈ω → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω))
    go (inr (inr ω∈c)) = ⊥₀-rec (refute (λ z z∈ω → C.col-ord p .fst z∈ω ω∈c))
```

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

```agda
  module Inv (p : OT.Dom) (g : S)
             (bfst : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ g .fst ⟩)
             (bsnd : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ g .fst ⟩) where
```

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

各 `r ≺ p` について、`φ r` が表す二つの座標がとも `g` の台に属すると仮定する。この二つの上界により、`r` が表す対は内部の積 `prodL g` に属する。この積が逆崩壊の終域になる。

崩壊の値のすべての要素 `x` はみずからの節を確定する。節は一意なので、切り詰められた所属は消去され、崩壊の値が `x` の基底集合である先行者 `r` が得られる。

```agda
    private
      pre : (x : S) → ⟨ x .fst ∈ˢ C.col p ⟩ → Σ[ r ∶ OT.Dom ] (C.col r ≡ x .fst)
      pre x mx = seg p (x .fst) mx .fst , seg p (x .fst) mx .snd .snd
```

`x ∈ C.col p` から選ばれた先行者 `r` について、提示の等式は `OT.↪ r` を、`φ r` が表す二つの座標の順序対と同一視する。したがって `prodL g` への所属は二つの座標の上界に帰着し、`bfst` が第一の上界を与える。

```agda
      bound : (x : S) (mx : ⟨ x .fst ∈ˢ C.col p ⟩) → ⟨ OT.↪ (pre x mx .fst) ∈ˢ (prodL g) .fst ⟩
      bound x mx = subst (λ w → ⟨ w ∈ˢ (prodL g) .fst ⟩) (sym (φ-eq (seg p (x .fst) mx .fst)))
        (prodL-in g (upK (φ (seg p (x .fst) mx .fst) .fst))
                    (upK (φ (seg p (x .fst) mx .fst) .snd))
                    (bfst _ (seg p (x .fst) mx .snd .fst))
```

`bsnd` が第二座標の所属を与える。二つの上界を合わせると、表された順序対が `g × g` に属することが分かり、必要な終域の証明が完成する。

```agda
                    (bsnd _ (seg p (x .fst) mx .snd .fst)))
```

したがって、`p` より下の始切片上の崩壊には `prodL g` への定義可能な逆写像がある。`C.col p` の各要素は一意な先行者へ戻り、異なる崩壊値は異なる対へ戻る。これにより、内部の単射 `C.colʟ p ↪ prodL g` が得られる。主帰納では、各 `p` について `C.col p ∈ a` を示す。まず、その最大座標に三分法を適用する。

```agda
    open I.Inverse (C.colʟ p) (prodL g) pre bound public
      using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )
```

</div>
</details>

```agda
  colIn : (p : OT.Dom) → ⟨ C.col p ∈ˢ a ⟩
  colIn p = go (ord-tri (mV p) (ord↑ (mx p)) ω ω-ord)
    where
```

対の最大値が有限なら、有限の場合によって崩壊の値も有限であり、`ω` が `a` に含まれることで `a` の中に入る。そうでなければ最大値は無限で、崩壊の値と `a` の三分法が検討される。

```agda
    go : ⟨ mV p ∈ˢ ω ⟩ ⊎ ((mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩) → ⟨ C.col p ∈ˢ a ⟩
    go (inl m∈ω) = ω⊆a (C.col p) (col-fin p m∈ω)
    go (inr inf) = go' (ord-tri (C.col p) (C.col-ord p) a oa)
      where
      m∉ω : ⟨ mV p ∈ˢ ω ⟩ → ⊥₀
```

無限の場合に `mV p ∈ ω` と仮定して矛盾を導く。`mV p = ω` なら、この所属を等しさに沿って移送すると `ω ∈ ω` が得られる。一方 `ω ∈ mV p` なら、`ω` の推移性で二つの所属を合成すると、やはり `ω ∈ ω` が得られる。非反射性が両方を排除するので、`mV p` は有限順序数ではない。

```agda
      m∉ω h = rr inf
        where
        rr : (mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩ → ⊥₀
        rr (inl e)   = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e h)
        rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
```

台 `g` は最大値の後続であり、最大値が順序数 `κ` の要素であるため `g` も順序数である。ついでこの順序数は `L` の要素 `gL` としてまとめられる。

```agda
      g : V ℓ
      g = sucV (mV p)
      og : IsOrd g
      og = suc-ord (ord↑ (mx p))
      gL : S
```

台は、上で証明した後続の閉性によって `a` に属し、さらに無限である。`g` が `ω` に属すれば、`g` の要素である最大値も推移性によって `ω` に属することになり、確立されたばかりの無限性と矛盾する。

```agda
      gL = ordL g og
      g∈a : ⟨ g ∈ˢ a ⟩
      g∈a = suc∈ (mV p) (member K (mx p))
      g∉ω : ⟨ g ∈ˢ ω ⟩ → ⊥₀
      g∉ω h = m∉ω (ω-ord .fst (self∈sucV (mV p)) h)
```

各 `r ≺ p` について、上界 `seg-fst` と `seg-snd` は `r` の二つの座標をとも `g = sucV (mV p)` に入れる。したがって逆崩壊の構成により、`C.colʟ p` から `prodL gL` への内部の単射が得られる。

```agda
      module IV = Inv p gL (seg-fst p) (seg-snd p) using (injL)
```

逆崩壊の単射と `prod-into gL` を合成すると、`C.colʟ p ↪ gL` が得られる。後者は `gL` に帰納仮定を直接適用したものではない。`prod-into` はまず `gL` の内部基数代表 `μ` を選び、`μ` で帰納仮定を適用し、`μ` と `gL` の間の単射に沿って、得られた平方の単射を移す。

```agda
      col↪g : InjL (C.colʟ p) gL
      col↪g = injl-trans (C.colʟ p) (prodL gL) gL IV.injL (prod-into gL og g∈a g∉ω)
      absurd : ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ C.col p ⟩) → ⊥₀
      absurd sub = carda gL g∈a
        (injl-trans κ (C.colʟ p) gL (inclusion-coded κ (C.colʟ p) sub) col↪g)
```

基数が崩壊の値に含まれるなら、その包含と `gL` への単射を合成することで、`κ` がみずからの要素 `gL` へ単射することになり、`κ` の内部の基数性と矛盾する。したがって崩壊の値と `a` の三分法に残るのは直接の所属だけである。

```agda
      go' : ⟨ C.col p ∈ˢ a ⟩ ⊎ ((C.col p ≡ a) ⊎ ⟨ a ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ a ⟩
      go' (inl h)       = h
      go' (inr (inl e)) = ⊥₀-rec (absurd (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈a))
      go' (inr (inr h)) = ⊥₀-rec (absurd (λ z z∈a → C.col-ord p .fst z∈a h))
  result : InjL (prodL κ) κ
```

まず積を崩壊の順序型 `C.otL` へ単射する。この順序型の各要素 `z` は、ある `b : OT.Dom` に対する `C.col b` と等しく、`colIn b` によってその崩壊値は `a` に属する。したがって `C.otL ⊆ κ` である。最初の単射と、この符号化された包含を合成すると、必要な内部の単射 `prodL κ ↪ κ` が得られる。

```agda
  result = injl-trans P C.otL κ injL-ot (inclusion-coded C.otL κ ot⊆a)
    where
    ot⊆a : (z : V ℓ) → ⟨ z ∈ˢ C.otL .fst ⟩ → ⟨ z ∈ˢ a ⟩
    ot⊆a z hz = rec₁ ((z ∈ˢ a) .snd)
      (λ { (b , e) → subst (λ w → ⟨ w ∈ˢ a ⟩) e (colIn b) }) (C.otL-out z hz)
```

</div>
</details>

これで所属関係に関する整礎帰納法から平方則が得られる。内部の基数であり `ω ∈ κ` を満たす順序数 `κ` に対し、`κ` が有限順序数ではないことを示せば、上で構成した帰納段階から内部の単射 `prodL κ ↪ κ` が得られる。

```agda
square-law-L :
    (κ : S) → IsOrd (κ .fst) → IsCardinalL κ → ⟨ ω ∈ˢ κ .fst ⟩
  → InjL (prodL κ) κ
square-law-L κ oκ cκ ω∈κ =
  WF.WFI.induction regularityV {P = Goal} Step.result (κ .fst) (κ .snd) oκ cκ
```

最後に、`κ` が `ω` に属することはない。もし属するなら、順序数 `ω` の推移性により `ω ∈ κ` と `κ ∈ ω` から `ω ∈ ω` が従い、非反射性に反する。これで帰納段階に必要な無限性の仮定が得られる。

```agda
    (λ κ∈ω → ∈-irrefl ω (ω-ord .fst ω∈κ κ∈ω))
```