---
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, 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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L の無限基数における平方律

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

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

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

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

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

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

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

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
```

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

```agda
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 {ℓ}
```

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

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

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

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

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

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

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

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

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

```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×; isSetΣSndProp )
```

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

```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
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

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

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

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

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

内側の台は h-集合であり、そのため要素の等しさを扱えます。要素は第二成分が命題である対なので、二つの要素が等しいのは基底集合が等しいときに限ります。対のパスの補題は、各成分の等しさから二つの対の等しさを構成します。

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
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
open import L.InjectionComposition {ℓ} lem public using ( module Relation )
private
  module Product (K : S) = Relation K K
```

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

```agda
    ((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K))
    (λ x y → (fst x ∈ˢ fst K) ⊓ (fst y ∈ˢ fst K))
    (λ 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 ]
               (⟨ fst a ∈ˢ fst K ⟩ × ⟨ fst b ∈ˢ fst K ⟩
                × (e ≡ pr (fst a) (fst b))) ∥₁
```

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

```agda
prodL-in : (K a b : S) → ⟨ fst a ∈ˢ fst K ⟩ → ⟨ fst b ∈ˢ fst K ⟩
         → ⟨ pr (fst a) (fst b) ∈ˢ fst (prodL K) ⟩
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) → ⟨ fst e ∈ˢ fst (prodL K) ⟩ → InProd K (fst e)
prodL-out K e h = PT.map (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h)
prodL-fst : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩
          → Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
              (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))
```

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

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

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

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

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

```agda
  isPropFib : isProp (Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
                        (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner
    (↪-inj {a = fst K} (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 =
  ∥ (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
  ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a)) ∥₁
```

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

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

最大値は有界な論理式として書けます。`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 (fst a) (fst b)) × (q ≡ pr (fst c) (fst d))
           × 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} → S ^ k → S → S → S → S → S → S
        → 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) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩
        ≡ (fst (lookup p γ) ≡ pr (fst a) (fst b))
    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) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩
        ≡ (fst (lookup q γ) ≡ pr (fst c) (fst d))
    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) (γ : S ^ k) → ⟨ γ ⊨ ltAt p q ⟩
         → Lt (fst (lookup p γ)) (fst (lookup q γ))
  lt-out p q γ = PT.rec squash₁ (λ { (a , ha) → PT.rec squash₁ (λ { (b , hb) →
    PT.rec squash₁ (λ { (c , hc) → PT.rec squash₁ (λ { (d , hd) →
    PT.rec squash₁ (λ { (m , hm) → PT.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
        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM
```

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

```agda
        , PT.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) (γ : S ^ k)
        → Lt (fst (lookup p γ)) (fst (lookup q γ)) → ⟨ γ ⊨ ltAt p q ⟩
  lt-in p q γ = PT.rec (snd (γ ⊨ ltAt p q))
    (λ { (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'
        , ( PT.map (λ { (inl h) → inl h
                      ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM
          , ( PT.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 → (fst p ∈ˢ fst P) ⊓ ((fst q ∈ˢ fst P) ⊓ (Lt (fst p) (fst q) , 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) → ⟨ fst p ∈ˢ fst P ⟩ → ⟨ fst q ∈ˢ fst P ⟩
         → Lt (fst p) (fst q) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
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 (fst p) (fst q) ∈ˢ fst (godel P) ⟩
          → ⟨ fst p ∈ˢ fst P ⟩ × ⟨ fst q ∈ˢ fst P ⟩ × Lt (fst p) (fst q)
godel-out = Godel.pair-out
```

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

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

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

`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 ℓ)
  _≺₁_ = SQ._≺₁_ K oκ
```

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

```agda
  _≺ₚ_ : Pair → Pair → Type (ℓ-suc ℓ)
  _≺ₚ_ = SQ._≺_ 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 ⟫) → fst a ≡ ↑ a' → fst b ≡ ↑ b'
          → MaxIs m a b → fst m ≡ ↑ (maxOrd a' b')
  max-out a b m a' b' ea eb = PT.rec (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))
```

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

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

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

```agda
    go (lt h) (inl (_ , e))   = e ∙ eb
    go (lt h) (inr (na , _))  =
      Empty.rec (na (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (sym ea) (sym eb) h))
    go (eq p) (inl (a∈b , _)) =
      Empty.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 , _)) =
      Empty.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 (↑ (fst p)) (↑ (snd p))
```

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

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

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

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

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

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

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

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

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

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

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

```agda
      inner : ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩)
            → (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 : ⟨ fst m ∈ˢ fst n ⟩
            ⊎ ((fst m ≡ fst n)
               × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁)
            → Empty.⊥
      outer (inl h)       = nk (inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) em en h))
```

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

```agda
      outer (inr (e , h)) = PT.rec Empty.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) → Empty.⊥) → p ≺ₚ q
    refuted nk = Empty.rec (PT.rec Empty.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 ⟫) → SQ._≤₁_ K oκ x 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 ⟫) → SQ._≤₁_ K oκ x 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
          → ⟨ ↑ (fst r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  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
          → ⟨ ↑ (snd r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  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
module Coll (κ : S) (oκ : IsOrd (fst κ)) where
```

これらの評価は 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 → ⟨ fst y ∈ fst P ⟩ × ⟨ fst x ∈ fst P ⟩
  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 ∣₁
```

## 三つの計数事実

続いて三分法が崩壊写像の単射性を与えるので、そのグラフが内部単射 `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 → ⟪ fst a ⟫ ↪ ⟪ fst b ⟫
  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 ∈ˢ ω ⟩ → Empty.⊥)
   → (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)         = Empty.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 (fst a) → (⟨ fst a ∈ˢ ω ⟩ → Empty.⊥)
       → IsOrd (fst b) → ⟨ fst b ∈ˢ ω ⟩ → InjL a b → Empty.⊥
no-fin a b oa a∉ω ob b∈ω = PT.rec Empty.isProp⊥ (λ c →
  finite-excl-ω (fst b) 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 fst e))))
  where
  ι : ⟪ ω ⟫ ↪ ⟪ fst a ⟫
  ι = incl ω (fst a) (ω⊆ (fst a) oa a∉ω)
```

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

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

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

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

```agda
module ProdMap (a b F : S)
               (sv : ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩)
```

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

```agda
               (ij : ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩)
               (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                    → ⟨ fst y ∈ fst b ⟩) where
```

抽出のモジュールは、グラフから実際の関数を読み取ります。`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 = ⟨ fst p ∈ˢ fst (prodL a) ⟩
  Comp : S → Type (ℓ-suc ℓ)
  Comp p = Σ[ x ∈ S ] Σ[ y ∈ S ]
             (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩ × (fst p ≡ pr (fst x) (fst y)))
```

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

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

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

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

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

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

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

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

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

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

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

```agda
    val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩) (x' : S) (mx' : ⟨ fst x' ∈ˢ fst a ⟩)
            → fst (val x mx) ≡ fst (val x' mx') → fst x ≡ fst x'
    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) → ⟨ fst (fn p mp) ∈ˢ fst (prodL b) ⟩
  into p mp =
    subst (λ w → ⟨ w ∈ˢ fst (prodL b) ⟩) (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' =
      (fst p ≡ pr (fst x) (fst y)) × (fst q ≡ pr (fst x') (fst y'))
    × ⟨ pr (fst x) (fst x') ∈ fst F ⟩ × ⟨ pr (fst y) (fst y') ∈ fst F ⟩
```

グラフの論理式 `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 → 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 ⟩ ≡ (fst p ≡ pr (fst x) (fst y))
      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 ⟩ ≡ (fst q ≡ pr (fst x') (fst y'))
      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 (fst x) (fst x') ∈ fst F ⟩
      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 (fst y) (fst y') ∈ fst F ⟩
      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 = PT.rec squash₁ (λ { (x , hx) → PT.rec squash₁ (λ { (y , hy) →
      PT.rec squash₁ (λ { (x' , hx') → PT.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 = PT.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 → snd (isL v))
        (e₂ ∙ cong₂ pr ex ey ∙ sym (prʟ-fst (val x mx) (val y my)))
```

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

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

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

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

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

```agda
             (subst (λ w → ⟨ pr w (fst y₁') ∈ fst F ⟩) 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')
      → fst (fn p mp) ≡ fst (fn p' mp') → fst p ≡ fst p'
  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 : (fst (val x mx) ≡ fst (val x' mx')) × (fst (val y my) ≡ fst (val y' my'))
```

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

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

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

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

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

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

## 無限基数の平方律

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

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

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

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

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

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

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

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

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

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

移し変えの定義域への所属を述べ、最初の判定を定義します。要素は `ω` に属するか、その所属が反証されるかのいずれかです。この選言は本当の場合分けであり、排中律が与えるものです。

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

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

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

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

```agda
    fin? : (x : S) → Fin? x
    fin? x = lem (fst x ∈ˢ ω)
```

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

```agda
    top? : (x : S) → Mem x → Top? x
    top? x h = go (lem (fst x ∈ˢ m))
      where
      go : ⟨ fst x ∈ˢ m ⟩ ⊎ (⟨ fst x ∈ˢ m ⟩ → Empty.⊥) → Top? x
      go (inl k)  = inl k
```

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

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

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

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

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

```agda
    suc≢∅ : (a : V ℓ) → sucV a ≡ ∅ → Empty.⊥
    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 (inl _) _       = sucʟ x
    value x (inr _) (inl _) = x
    value x (inr _) (inr _) = ∅ʟ
```

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

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

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

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

グラフの論理式は対象言語で述べられます。その第一の選言肢は、`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 ⟩ ≡ (fst y ≡ sucV (fst x))
      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 = PT.rec squash₁
      (λ { (inl (k , e)) → ∣ inl (k , transport (sa y x) e) ∣₁
         ; (inr h) → PT.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) → ⟨ fst x ∈ˢ ω ⟩ → fst y ≡ sucV (fst x) → ⟨ (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) → (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) → ⟨ fst x ∈ˢ m ⟩ → fst y ≡ fst x
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-mid y x n k e = ∣ inr ∣ inl ((λ hx → lift (n hx)) , (k , e)) ∣₁ ∣₁
```

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

```agda
    in-top : (y x : S) → fst x ≡ m → fst y ≡ ∅ → ⟨ (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 (inl k) _       = in-fin (sucʟ x) x k (sucʟ-fst x)
    defines' x (inr n) (inl k) = in-mid x x n k refl
    defines' x (inr 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 = PT.rec (isSetS y (value x f t)) (go f t) (graph-out y x hy)
      where
      go : (f : Fin? x) (t : Top? x)
```

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

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

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

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

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

```agda
      go (inr n) (inr q) (inl (k' , _))            = Empty.rec (n k')
      go (inr n) (inr q) (inr (inl (_ , k , _)))   = Empty.rec (not-both x k q)
      go (inr 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')
         → fst (value x f t) ≡ fst (value x' f' t') → fst x ≡ fst x'
    inj' x (inl k) _ x' (inl k') _ e =
      ord-suc-inj (fst x) (fst x') (mem-ord {A = ω} ω-ord (fst x) k)
        (sym (sucʟ-fst x) ∙ e ∙ sucʟ-fst x')
```

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

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

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

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

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

```agda
      Empty.rec (suc≢∅ (fst x') (sym (sucʟ-fst x') ∙ sym e))
    inj' x (inr n) (inr _) x' (inr n') (inl _) e =
      Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (#∈ω zero)))
    inj' x (inr n) (inr q) x' (inr 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'))
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 ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL (a , la)) (a , la)
```

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

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

台となる順序数が `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)) = Empty.rec (fin (ord-tri m om ω ω-ord))
      where
      fin : ⟨ m ∈ˢ ω ⟩ ⊎ ((m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩) → Empty.⊥
```

`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 ∈ˢ ω ⟩ → Empty.⊥
```

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

```agda
        m∉ω h = rr r
          where
          rr : (m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩ → Empty.⊥
          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 → snd (isL v)) (sucʟ-fst mL ∙ e)
    go (inr (inr h)) = Empty.rec*
      (∈sucV-elim {A = m} {x = a} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.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 γ ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL γ) γ
  prod-into γ oγ γ∈a γ∉ω = PT.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)) = Empty.rec (∈-irrefl (fst γ) (μ⊆γ (fst γ) h))
      μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
      μ∉ω 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 = PT.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 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 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 ⟩) → Empty.⊥
    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))   = Empty.rec (refute (λ z z∈ω → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω))
    go (inr (inr ω∈c)) = Empty.rec (refute (λ z z∈ω → C.col-ord p .fst z∈ω ω∈c))
  module Inv (p : OT.Dom) (g : S)
```

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

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

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

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

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

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

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

```agda
                    (bsnd _ (seg p (fst x) 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 )
  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 ∈ˢ ω ⟩ → Empty.⊥
```

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

```agda
      m∉ω h = rr inf
        where
        rr : (mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩ → Empty.⊥
        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 ∈ˢ ω ⟩ → Empty.⊥
      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 ⟩) → Empty.⊥
      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)) = Empty.rec (absurd (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈a))
      go' (inr (inr h)) = Empty.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 ∈ˢ fst C.otL ⟩ → ⟨ z ∈ˢ a ⟩
    ot⊆a z hz = PT.rec (snd (z ∈ˢ a))
      (λ { (b , e) → subst (λ w → ⟨ w ∈ˢ a ⟩) e (colIn b) }) (C.otL-out z hz)
```

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