---
title: "各段階上の整列順序"
module: L.Choice.StageOrders
lang: ja
site: "Bedrock"
description: "各段階上の整列順序"
stage: "正準整列順序と選択公理"
reading_order: 76
canonical: https://bedrock.institute/ja/L.Choice.StageOrders.html
html: L.Choice.StageOrders.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/StageOrders.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Stage, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.FiniteStageOrders, L.Choice.CanonicalNames, L.WellOrder.Base]
routes: [canonical-order, hulls-and-counting]
translations: [https://bedrock.institute/en/L.Choice.StageOrders.md, https://bedrock.institute/zh/L.Choice.StageOrders.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 各段階上の整列順序

各順序数 `γ` に対して、この章では周囲の型理論において `Lset γ` の要素上の狭義整列順序を構成する。構成は二重になっている。まず各集合に、それが初めて定義可能な部分集合として現れるときの基礎となる順序数を割り当てる。誕生順序数が異なる集合はその順序数で比較し、同時に生まれた集合は共通の直前段階上の最小の名前で比較する。次に所属帰納法によって、各段階の順序を同時に得る。得られるのは各段階における周囲の型理論の整列順序であり、集合論内部の関係でも、`L` 全体の単一の整列順序でもない。

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

古典的仮定は、単に非空である名前の族を、その確定した最小要素へ変える箇所で用いられる。どの添字に対しても、`stepAt` はこの最小名の構成から一様に得られる。

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

すべての構成は、固定した宇宙レベルと一つの仮定 `LEM (ℓ-suc ℓ)` のもとで行われる。同じ仮定が名前順序の構成と最小名の探索に渡され、段階順序を族へ組み立てる際には新たな古典的前提を加えない。

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

ここで順序づける対象は、周囲の型理論から見た累積階層の要素である。所属の証明も要素とともに運ばれるが、それらは命題なので、同じ要素の余分な複製を生じさせない。この区別は、のちに同じ順序を `L` の内部で記述し表現するときに重要になる。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( IsOrd; isL; Lset; Lset→isL )
```

集合の誕生順序数を定めるには、まずそれを含む最も早い順序数段階を取る。その段階は後続段階なので先行者をもち、この先行者が、集合が初めて定義可能な部分集合として現れるときの基礎段階である。のちに順序数の三分性を用いて、この誕生順序数が集合を含むどの順序数段階よりも真に下にあることを示す。

```agda
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( IsPredOf; predOf; carveAt )
```

ある段階が整列順序づけられると、その論理式とパラメータ列は次の段階の整列順序づけられた名前をなす。後続段階の一つの要素が多くの名前をもつこともあるので、構成はその最小のものを選び、選ばれた代表を通して要素を比較する。ここで一意なのは最小代表であり、名前一般ではない。

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Tri-map )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; isPropLeastOf )
```

この構成では表現を何度か変える。表示の添字からそれが表す集合へ、集合から所属証明を伴う要素へ、さらに要素からその最小名へと移る。どの変更も単射なので、異なる要素を同一視することなく等しさと狭義比較を移せる。

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
```

名前の完全性が与えるのは存在の命題的切り詰めだけである。すなわち、指示する名前が単に存在すると述べるだけで、選ばれた名前を示さない。後の最小要素の議論がこの切り詰めを除去できるのは、最小名の全体型そのものが命題だからである。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

階層の集合には、小さな表示型と周囲の所属型の両方がある。表示写像は前者を後者へ埋め込む。この橋により、名前を作るときには小さなパラメータを使いながら、`Lset γ` の要素上に直接述べられた順序を保てる。

```agda
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV )
```

ここから `S` は集合の周囲の台を表す。したがって `x ∈ˢ Lset γ` のような主張は、構成可能段階への所属を表す外部の型であり、まだ対象理論で評価される論理式ではない。

```agda
open hPropStructure 𝒮ᵥ
```

## 集合が切り出される段階

一般の切り出しの議論を、「`x` がある段階に属する」という性質に適用する。`stage x p` はこの性質を満たす最も早い段階なので、その結果は、後続がちょうど `stage x p` となる順序数 `δ` を与える。したがって `δ` は最初の包含段階の先行者であり、独立に選ばれた別の最小段階ではない。

```agda
theCarve : (x : S) (p : ⟨ isL x ⟩) → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
theCarve x p = predOf (λ σ → x ∈ˢ Lset σ) (stage x p) (stage-ord x p)
  (stage-earliest x p)
  (carveAt (λ σ → x ∈ˢ Lset σ) (stage x p) x (stage-mem x p) (λ δ hz → hz))
```

順序数 `birth x p` はこの先行者である。数学的には、`x` が初めて定義可能な部分集合として現れるときの基礎段階を記録する。これを `x` のフォン・ノイマン階数と読んではならない。ここで示される同一視は、その後続が `x` を含む最も早い構成可能段階であることだけである。

```agda
opaque
  birth : (x : S) → ⟨ isL x ⟩ → S
  birth x p = theCarve x p .fst
```

`theCarve x p` の先行者データには、選ばれた先行者が順序数であることの証明と、その後続を `stage x p` と同一視する等式の両方が含まれる。`birth-ord` は前者を読み出すので、後で `birth x p` を他の順序数と比較し、所属帰納法の添字として用いることができる。

```agda
opaque
  unfolding birth
  birth-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (birth x p)
  birth-ord x p = theCarve x p .snd .fst
```

第二の射影は定義的な等式 `sucV (birth x p) ≡ stage x p` を与える。この等式は二つの有用な見方を結ぶ。`stage` は `x` が初めて属する段階を示し、`birth` は `x` がどの直前段階を基礎として作られたかを示す。

```agda
  birth-suc : (x : S) (p : ⟨ isL x ⟩) → sucV (birth x p) ≡ stage x p
  birth-suc x p = theCarve x p .snd .snd
```

`x` はその最も早い段階に属し、その段階は `sucV (birth x p)` なので、`x` は誕生順序数の後続段階に属する。この所属こそ、`x` を `Lset (birth x p)` の定義可能な部分集合と見なし、そこで名前を与えるために必要なものである。

```agda
birth-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (sucV (birth x p)) ⟩
birth-mem x p =
  subst (λ w → ⟨ x ∈ˢ Lset w ⟩) (sym (birth-suc x p)) (stage-mem x p)
```

誕生順序数自身はその後続順序数に属し、先行者の等式がこの所属を `stage x p` へ移す。したがって `x` を含む最も早い段階は、`x` が作られるときの基礎となった順序数も含む。

```agda
birth-stage : (x : S) (p : ⟨ isL x ⟩) → ⟨ birth x p ∈ˢ stage x p ⟩
birth-stage x p =
  subst (λ w → ⟨ birth x p ∈ˢ w ⟩) (birth-suc x p) (self∈sucV (birth x p))
```

`birth` は `x` が構成可能であることの証明 `p` を受け取るが、その値はそのような証明の数学的な選択を含まない。構成可能性は命題なので、任意の二つの証明 `p` と `q` は等しい。その等式に関数 `birth x` を作用させれば、どちらの入力からも同じ順序数が得られる。

```agda
birth-proof : (x : S) (p q : ⟨ isL x ⟩) → birth x p ≡ birth x q
birth-proof x p q = cong (birth x) (snd (isL x) p q)
```

`x ∈ Lset γ` であり、`γ` が順序数であるとする。三分性により `γ` と最初の段階 `stage x p` を比較する。`γ ∈ stage x p` の場合は不可能である。すでに `x` を含む、より早い順序数段階が得られ、`stage x p` の定義上の最小性に反するからである。

```agda
private
  decideIn : (γ x : S) → IsOrd γ → (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset γ ⟩
           → ⟨ γ ∈ˢ stage x p ⟩ ⊎ ((γ ≡ stage x p) ⊎ ⟨ stage x p ∈ˢ γ ⟩)
           → ⟨ birth x p ∈ˢ γ ⟩
  decideIn γ x ordγ p h (inl γ∈) = Empty.rec (stage-earliest x p γ ordγ h γ∈)
```

`γ` が最初の段階に等しければ、`birth-stage` を移すことで求める所属が直ちに得られる。最初の段階が `γ` に属するなら、順序数 `γ` の推移性が `birth x p ∈ stage x p` と `stage x p ∈ γ` を合成する。これらが矛盾しない二つの可能な場合である。

```agda
  decideIn γ x ordγ p h (inr (inl e)) =
    subst (λ w → ⟨ birth x p ∈ˢ w ⟩) (sym e) (birth-stage x p)
  decideIn γ x ordγ p h (inr (inr s∈)) = ordγ .fst (birth-stage x p) s∈
```

したがって `x` が順序数段階 `Lset γ` の要素であれば、その誕生順序数は `γ` に属する。この結論は狭義である。のちに `γ` における順序を構成するとき、この事実によって各要素の誕生順序数は、帰納法の仮定がすでに順序を与えている小さい順序数の中に置かれる。

```agda
birth-in : (γ : S) → IsOrd γ → (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset γ ⟩
         → ⟨ birth x p ∈ˢ γ ⟩
birth-in γ ordγ x p h =
  decideIn γ x ordγ p h (ord-tri γ ordγ (stage x p) (stage-ord x p))
```

## 単射に沿って整列順序を移す

周囲の集合 `A` に対し、型 `Mem A` の要素は、集合とそれが `A` に属することの証拠との対である。この証拠を伴わせることで、後の順序関係が正しく型づけられる。所属は命題値なので、基礎となる集合が同じ二つの要素が、所属の証拠の得方だけによって異なることはない。

```agda
Mem : S → Type (ℓ-suc ℓ)
Mem A = Σ[ x ∈ S ] ⟨ x ∈ˢ A ⟩
```

型 `A` 上の狭義整列順序 `w` を固定する。次の構成はこの構造に含まれる関係と法則だけを使うので、名前の順序、段階要素の順序、およびそれらの表現の変更に同じように適用できる。

```agda
module _ {ℓc : Level} {A : Type ℓc} (w : SWO A) where
  open SWO w using () renaming ( _<∙_ to _<ʷ_ )
```

`w` に含まれる狭義比較を `relOf w a b` と書くことで、整列順序の組み立て方を展開せずに関係を論じられる。とくに、この記法によって関係が内部集合論の対象になるわけではない。それは依然として周囲の型理論における型値の関係である。

```agda
  relOf : A → A → Type (ℓ-suc ℓ)
  relOf a b = a <ʷ b
```

`f : B → C` が単射であり、`C` が狭義整列順序づけられているとする。`B` の `u` と `v` を `f u` と `f v` の比較によって比べれば、その関係は狭義整列順序を受け継ぐはずである。単射性が本質的に必要なのは、`C` における等しい場合を `B` へ反映するときである。

```agda
module _ {ℓb ℓc : Level} (B : Type ℓb) (C : Type ℓc) (w : SWO C)
         (f : B → C) (finj : (u v : B) → f u ≡ f v → u ≡ v) where
  open SWO w using () renaming
    ( _<∙_ to _<ᶜ_ ; tri∙ to triᶜ ; irr∙ to irrᶜ
    ; trans∙ to transᶜ ; wf∙ to wfᶜ )
```

引き戻された関係では、像 `f u` が `f v` より小さいとき、かつそのときに限って `u` が `v` より小さいと定める。したがって `B` は `C` 内の像が表す順序づけられた部分として並べられるのであり、全射性も順序同型も主張しない。

```agda
  private
    _<ᵇ_ : B → B → Type (ℓ-suc ℓ)
    u <ᵇ v = f u <ᶜ f v
```

`C` の三分性は二つの像について三つの場合を与える。二つの狭義の場合はそのまま引き戻された関係の比較であり、像が等しい場合には単射性からもとの点の等しさが得られる。したがって `B` 上の関係も三分的である。

```agda
    pullTri : (u v : B) → Tri (u <ᵇ v) (u ≡ v) (v <ᵇ u)
    pullTri u v = Tri-map id (finj u v) id (triᶜ (f u) (f v))
```

整礎性も引き戻せる。`f u` が `C` で到達可能なら、その到達可能性の木は、下にある各 `f v` に対する部分木を含む。`u` の先行元 `v` はまさにその比較を与え、対応する部分木を再帰的に引き戻すことで、`v` が `B` で到達可能だと分かる。したがって `f` に沿って移されるのは、単に下降列が提示されていないという弱い主張ではなく、到達可能性そのものである。

```agda
    pullAcc : (u : B) → Acc _<ᶜ_ (f u) → Acc _<ᵇ_ u
    pullAcc u (acc r) = acc (λ v h → pullAcc v (r (f v) h))
```

非反射性は直ちに移る。引き戻された関係で点が自分自身より小さければ、その像も `C` で自分自身より小さくなってしまう。先に示した三分性と合わせて、これで源の上の最初の順序法則が得られる。

```agda
  pullOrder : SWO B
  pullOrder = record
    { _<∙_   = _<ᵇ_
    ; tri∙   = pullTri
    ; irr∙   = λ u h → irrᶜ (f u) h
```

推移性は `C` における三つの像の比較を合成することで従い、到達可能性の議論が整礎性を与える。これらの法則によって `pullOrder`、すなわち単射 `f` を通して `B` の要素を見ることで得られる狭義整列順序が完成する。

```agda
    ; trans∙ = λ u v z → transᶜ (f u) (f v) (f z)
    ; wf∙    = λ u → pullAcc u (wfᶜ (f u)) }
```

小さな表示 `⟪ A ⟫` の各添字は `A` の実際の要素を指す。その像をこの所属の証拠と対にすることで、表示の添字から、段階順序が構成される形 `Mem A` への写像が得られる。

```agda
memOf : (A : S) (m : ⟪ A ⟫) → ⟨ ⟪ A ⟫↪ m ∈ˢ A ⟩
memOf A m = ∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)
```

関数 `carry` はこの写像に沿って、周囲の要素対上の順序を小さな表示型へ引き戻す。これは名前の構成が必要とする向きである。そのパラメータ列は `⟪ A ⟫` から取られる一方、のちに構成する段階順序は自然に `Mem A` を順序づけるからである。

```agda
carry : (A : S) → SWO (Mem A) → SWO ⟪ A ⟫
carry A w = pullOrder ⟪ A ⟫ (Mem A) w (λ m → ⟪ A ⟫↪ m , memOf A m) inj
  where
  inj : (u v : ⟪ A ⟫)
      → _≡_ {A = Mem A} (⟪ A ⟫↪ u , memOf A u) (⟪ A ⟫↪ v , memOf A v) → u ≡ v
```

表示写像は埋め込みなので、得られた要素対が等しければ、その基礎となる表示要素が等しくなり、したがってもとの添字も等しくなる。これで `pullOrder` に必要な単射性が確認されるが、各要素について任意の表示を選んだと主張するものではない。

```agda
  inj u v q = isEmbedding→Inj isEmb⟪ A ⟫↪ u v (cong fst q)
```

## ステップ

段階の添字 `δ` に対し、`New δ` は `Lset (sucV δ)` のすべての要素を、それぞれ所属の証拠と対にした型である。この名前は一段階の構成を述べるのに便利だが、各要素がちょうど `δ` で生まれたという意味ではない。より早く生まれた要素もこの後続段階に残りうる。

```agda
New : S → Type (ℓ-suc ℓ)
New δ = Mem (Lset (sucV δ))
```

添字 `δ` と `Lset δ` の小さな要素上の狭義整列順序を固定する。これで、この段階上の名前を比較できる。名前のパラメータ部分が、まさに与えられた順序によって比較されるからである。これが、どの添字でも用いられる一様な局所構成を与える。

```agda
module _ (δ : S) (w : SWO ⟪ Lset δ ⟫) where
  private
    module NM = Naming (Lset δ) w
```

名前の意味値が集合 `x` に等しいとき、その名前は `x` を指示するという。階層の集合の等しさは命題なので、指示は `hProp` 値の族をなす。この命題値の形が、一般の最小要素構成に必要である。

```agda
  denotesAt : S → NM.Name → hProp (ℓ-suc ℓ)
  denotesAt x n = (NM.denote n ≡ x) , setIsSet (NM.denote n) x
```

`a : New δ` に対して名前が付けられるのは、基礎となる集合 `a.fst` だけである。その所属の証拠は集合が後続段階にあることを示すが、指示の等式の一部ではなく、どの名前が最小であるかには影響しない。

```agda
  private
    denotes : New δ → NM.Name → hProp (ℓ-suc ℓ)
    denotes a = denotesAt (a .fst)
```

`Lset (sucV δ)` への所属を、後続段階の等式によって `Lset δ` 上の定義可能冪集合への所属へ書き換える。すると名前の完全性から、名前とそれが `a.fst` を指示する証拠との対の命題的切り詰めが得られる。この時点では、まだ名前は一つも選ばれていない。

```agda
    hasName : (a : New δ) → ∥ Σ[ n ∈ NM.Name ] ⟨ denotes a n ⟩ ∥₁
    hasName a = NM.names-complete (a .fst)
      (subst (λ v → ⟨ a .fst ∈ˢ v ⟩) (Lset-suc δ) (a .snd))
```

名前の順序は狭義整列順序なので、単に非空である指示名の族には最小要素がある。最小要素の構成は、その降下に古典的仮定を用いる。命題的切り詰めを除去してよいのは、名前とそれが最小であることの証明との全体型が命題だからである。そのような二つの名前は三分性によって等しくなる。

```agda
    leastOfNew : (a : New δ)
               → Σ[ n ∈ NM.Name ] IsLeast NM.nameOrder (denotes a) n
    leastOfNew a = NM.leastName (denotes a) (hasName a)
```

`theName a` を、この最小証人の名前成分として定める。この構成は、整列順序が与える正確な意味で標準的である。完全性は任意の代表を示さなかったが、最小代表は一意に定まる。

```agda
    theName : New δ → NM.Name
    theName a = leastOfNew a .fst
```

最小性には、最小化している族に属するという条件も含まれる。したがって選ばれた名前は実際に `a.fst` を指示する。最小性の制約だけでは足りない。指示名の族に属さない名前は、周囲の名前順序のどこにあってもよいからである。

```agda
    theName-denote : (a : New δ) → NM.denote (theName a) ≡ a .fst
    theName-denote a = leastOfNew a .snd .fst
```

二つの後続段階の要素が同じ選ばれた最小名をもつなら、指示を適用することで基礎となる集合が等しいと分かる。所属成分は命題なので、この等しさは要素対の等しさへ持ち上がる。したがって最小名を選ぶ写像は単射であるが、すべての名前上の指示写像が単射である必要はない。

```agda
    nameInj : (u v : New δ) → theName u ≡ theName v → u ≡ v
    nameInj u v q = Σ≡Prop (λ x → snd (x ∈ˢ Lset (sucV δ)))
      (sym (theName-denote u) ∙ cong NM.denote q ∙ theName-denote v)
```

この単射に沿って名前の狭義整列順序を引き戻す。すると `Lset (sucV δ)` の二つの要素は、それぞれ選ばれた最小名によって比較される。後の `stepAt` が用いる構成はこれ一つだけであり、どの `δ` も同じ最小名による道をたどる。

```agda
  byName : SWO (New δ)
  byName = pullOrder (New δ) NM.Name NM.nameOrder theName nameInj
```

`IsLeastName t x` は二つのことを述べる。`t` が `x` を指示することと、名前の順序において `x` を指示する別の名前が `t` より真に下にはないことである。範囲を `x` を指示する名前に限ることが重要であり、他の集合を指示する名前はこの最小性の主張に関係しない。

```agda
  IsLeastName : NM.Name → S → Type (ℓ-suc ℓ)
  IsLeastName t x = IsLeast NM.nameOrder (denotesAt x) t
```

各要素 `a : New δ` に対し、この構成は名前と、それが基礎となる集合について `IsLeastName` を満たす証拠を与える。したがって後続の証明は、探索がそれを見つけた方法を展開せず、命題的切り詰めを任意の選択に置き換えることもなく、最小名を用いて推論できる。

```agda
  leastNameOf : (a : New δ) → Σ[ t ∈ NM.Name ] IsLeastName t (fst a)
  leastNameOf a = leastOfNew a
```

`t` が `IsLeastName t (fst c)` を満たす任意の名前であるとする。`(theName c, leastOfNew c .snd)` と `(t,h)` は、同じ指示述語に対する最小証人である。このような最小証人の全体型は命題である。三分性が、一方の名前が他方より真に小さい二つの場合を排除し、二つの名前の等しさを強制する。その等しさを射影すれば `theName c ≡ t` を得る。したがって一意なのは最小名であり、その集合はなお多くの最小でない名前をもちうる。

```agda
  private
    pin : (c : New δ) (t : NM.Name) → IsLeastName t (fst c) → theName c ≡ t
    pin c t h = cong fst
      (isPropLeastOf NM.nameOrder (denotes c) (leastOfNew c) (t , h))
```

比較の事実が、それぞれの候補の最小の名前を固定します。`t₁` が `a` の最小の名前であり、`t₂` が `b` の最小の名前であるならば、引き戻された順序が計算する関係は、二つの最小の名前の順序そのものです。ピン止めされた名前が、それぞれ計算された最小値に等しいので、引き戻された順序がそれらの等式に沿って運ばれるからです。

```agda
    byName-least : (a b : New δ) (t₁ t₂ : NM.Name)
                 → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                 → relOf byName a b ≡ NM._≺ₙ_ t₁ t₂
    byName-least a b t₁ t₂ h₁ h₂ = cong₂ NM._≺ₙ_ (pin a t₁ h₁) (pin b t₂ h₂)
```

どの順序数 `δ` に対しても、ステップ順序は一つの `byName` です。`Lset (sucV δ)` の要素は、`Lset δ` 上で一意に定まる最小の名前を通して比較されます。この構成には、有限段階用や極限段階用の別の分岐はありません。

```agda
  opaque
    stepAt : SWO (New δ)
    stepAt = byName
```

次の二つの橋渡し補題により、すでに最小だと証明された任意の代表を通して `stepAt` を扱える。二つの要素の最小名をそれぞれ `t₁`、`t₂` とすれば、`stepAt` による要素の比較と `t₁`、`t₂` の名前としての比較は互いを決定する。したがって後の議論に必要なのは選ばれた名前の仕様であり、それを得た探索の具体的な過程ではない。

```agda
  opaque
    unfolding stepAt
```

充填の読み出しはこう言います。二つの名前がそれぞれの要素の最小の名前であれば、名前の順序が要素の順序を決めます。証明は、ピン止めされた名前と計算された最小値の間の一致に沿って、名前の比較を運びます。

```agda
    stepAt-fill : (a b : New δ) (t₁ t₂ : NM.Name)
                → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                → NM._≺ₙ_ t₁ t₂ → relOf stepAt a b
    stepAt-fill a b t₁ t₂ h₁ h₂ =
      transport (sym (byName-least a b t₁ t₂ h₁ h₂))
```

読み出しの補題はその逆を言います。ステップの順序が二つの要素の間で成立するならば、それらの要素の最小の名前も同じように順序づけられます。

```agda
    stepAt-read : (a b : New δ) (t₁ t₂ : NM.Name)
                → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                → relOf stepAt a b → NM._≺ₙ_ t₁ t₂
    stepAt-read a b t₁ t₂ h₁ h₂ =
      transport (byName-least a b t₁ t₂ h₁ h₂)
```

## 順序の族

関係 `Under δ v x y` は、特定の所属証明をあらかじめ固定せずに、基礎の集合 `x` と `y` の比較を記録します。二つを `Lset (sucV δ)` に置く証明と、それによって得られる要素を `v` で比較した証拠から成ります。これは通常の Sigma 型であって命題的切り詰めではなく、命題的に一意なのは所属証明の部分です。

```agda
Under : (δ : S) → SWO (New δ) → S → S → Type (ℓ-suc ℓ)
Under δ v x y = Σ[ hx ∈ ⟨ x ∈ˢ Lset (sucV δ) ⟩ ]
                Σ[ hy ∈ ⟨ y ∈ˢ Lset (sucV δ) ⟩ ]
                relOf v (x , hx) (y , hy)
```

任意に選んだ所属証明 `hx` と `hy` に対し、`under-at` はその提示で `Under` の比較を読み出します。`Under` が保持する証明は `hx` や `hy` と同じ項である必要はなく、それらの等しさは所属が命題であることから従います。

```agda
under-at : (δ : S) (v : SWO (New δ)) (x y : S)
           (hx : ⟨ x ∈ˢ Lset (sucV δ) ⟩) (hy : ⟨ y ∈ˢ Lset (sucV δ) ⟩)
         → Under δ v x y → relOf v (x , hx) (y , hy)
under-at δ v x y hx hy (kx , ky , h) =
  subst2 (λ p q → relOf v (x , p) (y , q))
```

この証明の整合があるからこそ、`Under` を再帰的な順序の族で用いられる。誕生順序数が等しいとき、同じ集合が異なる証明によって同じ後続段階に置かれることがある。`under-at` は、比較の型そのものが命題だと仮定せずに、証拠を取り替えた後も局所比較を使えるようにする。

```agda
    (snd (x ∈ˢ Lset (sucV δ)) kx hx) (snd (y ∈ˢ Lset (sucV δ)) ky hy) h
```

順序数 `γ` を固定します。この段階の順序を構成するため、各順序数 `δ ∈ γ` について `Mem (Lset δ)` 上の狭義整列順序がすでに得られていると再帰的に仮定します。モジュール `Family` は、まさにこれらの小さい段階の順序から `Lset γ` の要素上の順序を構成します。

```agda
module Family (γ : S)
              (IH : (δ : S) → ⟨ δ ∈ˢ γ ⟩ → IsOrd δ → SWO (Mem (Lset δ)))
              (ordγ : IsOrd γ) where
  private
    Member : Type (ℓ-suc ℓ)
```

この段階での台は `Member = Mem (Lset γ)` です。累積階層の集合と、それが段階 `Lset γ` に属するという証拠の組です。

```agda
    Member = Mem (Lset γ)
```

`γ` は順序数なので、`Lset γ` に属する集合は構成可能です。したがって各 `a : Member` には、その誕生順序数を作るために必要な構成可能性の証明があります。

```agda
    memberL : (a : Member) → ⟨ isL (a .fst) ⟩
    memberL a = Lset→isL γ ordγ (a .fst) (a .snd)
```

層のそれぞれの要素は、自分自身の誕生の順序数の後続に属します。誕生の構成の所属の読み出しによるものです。

```agda
    newIn : (a : Member) → ⟨ a .fst ∈ˢ Lset (sucV (birth (a .fst) (memberL a))) ⟩
    newIn a = birth-mem (a .fst) (memberL a)
```

要素の誕生は、順序数の添字 `γ` の要素としてまとめられます。誕生の順序数と、それが `γ` より下にあるという証明です。後者は、要素が `γ` での層に属することから従います。

```agda
  bornAt : Member → Mem γ
  bornAt a = birth (a .fst) (memberL a)
           , birth-in γ ordγ (a .fst) (memberL a) (a .snd)
```

`d : Mem γ` に対し、帰納の仮定は `Lset (d .fst)` の証明つき要素上の順序を与えます。`carry` はそれを名前が用いる小さい表示型へ移し、続いて `stepAt` が最小の名前によって `Lset (sucV (d .fst))` の証明つき要素を整列します。これが `d .fst` 上で誕生した集合を比較する局所順序です。

```agda
  stepIn : (d : Mem γ) → SWO (New (d .fst))
  stepIn d = stepAt (d .fst) (carry (Lset (d .fst))
    (IH (d .fst) (d .snd) (mem-ord {A = γ} ordγ (d .fst) (d .snd))))
```

組にされた順序数 `d : Mem γ` に対し、`UnderAt d a b` は、証明の選び方に依存しない関係 `Under` を `d` での局所ステップ順序に適用します。以下の同じ誕生の場合には、`d` は `a` と `b` の共通の誕生順序数になります。

```agda
  UnderAt : (d : Mem γ) → Member → Member → Type (ℓ-suc ℓ)
  UnderAt d a b = Under (d .fst) (stepIn d) (a .fst) (b .fst)
```

主関係は辞書式です。`a` の誕生順序数が `b` の誕生順序数に属するなら `a ≺ b` です。二つの誕生順序数が等しいときは、`a` の誕生順序数での局所ステップ順序によって基礎の集合を比較します。等式は `b` の誕生から `a` の誕生へ向けてあり、第二の集合を同じ局所順序へ直接置けるようになっています。

```agda
  _≺_ : Member → Member → Type (ℓ-suc ℓ)
  a ≺ b = ⟨ bornAt a .fst ∈ˢ bornAt b .fst ⟩
        ⊎ ((bornAt b .fst ≡ bornAt a .fst) × UnderAt (bornAt a) a b)
```

まとめの補助は、同じ基礎の順序数をもつ順序数の添字の二つの要素が等しいと言います。順序数の中の所属が命題だからです。

```agda
  private
    packBirth : (d z : Mem γ) → d .fst ≡ z .fst → d ≡ z
    packBirth d z = Σ≡Prop (λ v → snd (v ∈ˢ γ))
```

主順序の非反射性は、辞書式関係の二つの意味から従う。`a ≺ a` が早い誕生の証拠から得られたなら、順序数 `birth(a)` が自分自身に属することになる。同じ誕生の証拠から得られたなら、`a` とそれ自身との局所比較になる。そこに保存された所属証明は `newIn a` と異なりうるが、`under-at` が後者の証明で同じ比較を読み出すので、局所順序の非反射性を適用できる。

```agda
  private
    ≺-irr : (a : Member) → a ≺ a → Empty.⊥
    ≺-irr a (inl h) = ∈-irrefl (bornAt a .fst) h
    ≺-irr a (inr (_ , u)) =
      SWO.irr∙ (stepIn (bornAt a)) (a .fst , newIn a)
```

ここで取り替えるのは所属証明だけである。その命題性によって `a` の二つの表示が同一視され、局所比較の証明は、狭義整列順序が自己比較を禁じる表示へそのまま輸送される。

```agda
        (under-at (bornAt a .fst) (stepIn (bornAt a)) (a .fst) (a .fst)
          (newIn a) (newIn a) u)
```

推移性には四つの場合があります。早い・早いの場合は、誕生の順序数の推移性が二つの厳密な所属を合成します。早い・等しいの場合は、等式が誕生の所属を共通の誕生の順序数の先へ運びます。

```agda
    ≺-trans : (a b c : Member) → a ≺ b → b ≺ c → a ≺ c
    ≺-trans a b c (inl h) (inl k) =
      inl (birth-ord (c .fst) (memberL c) .fst h k)
    ≺-trans a b c (inl h) (inr (e , _)) =
      inl (subst (λ v → ⟨ bornAt a .fst ∈ˢ v ⟩) (sym e) h)
```

残る混合の場合では、誕生順序数の間の真の大小関係を、それらの等式に沿って移します。二つの比較がともに同じ誕生の場合なら、二つの等式が誕生順序数を一つに同定し、推移性はその局所ステップ順序で二つの比較を合成することに帰着します。

```agda
    ≺-trans a b c (inr (e , _)) (inl k) =
      inl (subst (λ v → ⟨ v ∈ˢ bornAt c .fst ⟩) e k)
    ≺-trans a b c (inr (e , u)) (inr (eb , v)) = inr (eb ∙ e , joined)
      where
      d : Mem γ
```

同じ誕生どうしの場合には、`d = bornAt a` を共通の、証明と組にされた誕生とする。第一の比較はすでに局所順序 `stepIn d` の中にある。組にされた誕生の等しさに沿って、第二の比較を `bornAt b` を添字とする局所順序から同じ `stepIn d` へ移す必要がある。局所順序が組にされた添字に依存するためである。

```agda
      d = bornAt a
      moved : UnderAt d b c
      moved = subst (λ z → UnderAt z b c) (packBirth (bornAt b) d e) v
      joined : UnderAt d a c
      joined = u .fst , (moved .snd .fst
```

これで二つの前提を一つの狭義整列順序の中で読める。二つの `UnderAt` の証拠が運ぶ所属証明を中間の集合 `b` でそろえ、`stepIn d` の推移性によって `a` から `b`、`b` から `c` への局所比較を合成する。

```agda
        , SWO.trans∙ (stepIn d) (a .fst , u .fst) (b .fst , moved .fst)
            (c .fst , moved .snd .fst)
            (under-at (d .fst) (stepIn d) (a .fst) (b .fst)
              (u .fst) (moved .fst) u)
            (under-at (d .fst) (stepIn d) (b .fst) (c .fst)
```

合成した局所比較と、共通の誕生においてすでに得られた両端の所属証明を合わせると、`UnderAt d a c` の証拠になる。したがって同じ誕生の場合が推移的なのは、その下にある名前順序と同じ理由による。三つの集合が一つの固定した局所順序で比較されているからである。

```agda
              (moved .fst) (moved .snd .fst) moved))
```

三分性を示すには、まず二つの誕生順序数を比較する。それぞれの順序数性の証明によって順序数の三分性を適用でき、「第一の誕生が早い」「誕生が等しい」「第二の誕生が早い」という三つの場合が得られる。局所的なステップ順序で比較する必要があるのは、中央の場合だけである。

```agda
    ≺-tri : (a b : Member) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
    ≺-tri a b = byBirth (ord-tri (bornAt a .fst) (birth-ord (a .fst) (memberL a))
                                 (bornAt b .fst) (birth-ord (b .fst) (memberL b)))
      where
      byBirth : ⟨ bornAt a .fst ∈ˢ bornAt b .fst ⟩
```

誕生が異なる場合、その順序数としての狭義比較だけで主順序が決まる。この二つの場合には、どちらの集合の名前も調べない。最小名の順序を使うのは、共通の誕生順序数をもつ集合に限られる。

```agda
              ⊎ ((bornAt a .fst ≡ bornAt b .fst) ⊎ ⟨ bornAt b .fst ∈ˢ bornAt a .fst ⟩)
              → Tri (a ≺ b) (a ≡ b) (b ≺ a)
      byBirth (inl h)       = lt (inl h)
      byBirth (inr (inr h)) = gt (inl h)
      byBirth (inr (inl e)) =
```

等しい誕生の場合は、共通の誕生の順序数での局所のステップの順序が比較を決めます。二つの要素の証明は、共通の誕生の順序数へと揃え直されます。

最初の証明の揃えは、その要素自身の後続の所属です。

```agda
        bySteps (SWO.tri∙ (stepIn (bornAt a)) (a .fst , ha) (b .fst , hb))
        where
        same : bornAt b .fst ≡ bornAt a .fst
        same = sym e
        ha : ⟨ a .fst ∈ˢ Lset (sucV (bornAt a .fst)) ⟩
```

第一の集合はもともと自分の誕生順序数の後続段階に属します。誕生順序数の等しさによって、第二の集合の対応する証明も同じ後続段階へ移されるので、局所的な三分性は一つの台の中で両者を比較できます。

```agda
        ha = newIn a
        hb : ⟨ b .fst ∈ˢ Lset (sucV (bornAt a .fst)) ⟩
        hb = subst (λ v → ⟨ b .fst ∈ˢ Lset (sucV v) ⟩) (sym e) (newIn b)
        bySteps : Tri (relOf (stepIn (bornAt a)) (a .fst , ha) (b .fst , hb))
                      ((a .fst , ha) ≡ (b .fst , hb))
```

局所順序の三分性から、証明つきの二つの後続段階要素について、いずれかの向きの比較または等しさが得られる。等しい場合には基礎の集合の等しさが直ちに従い、`Lset γ` への所属は命題なので、その等しさは元の段階要素 `a` と `b` の等しさへ持ち上がる。

```agda
                      (relOf (stepIn (bornAt a)) (b .fst , hb) (a .fst , ha))
                → Tri (a ≺ b) (a ≡ b) (b ≺ a)
        bySteps (lt h) = lt (inr (same , (ha , hb , h)))
        bySteps (eq q) = eq (Σ≡Prop (λ v → snd (v ∈ˢ Lset γ)) (cong fst q))
        bySteps (gt h) = gt (inr (sym same
```

局所的な三分性が `b` を `a` より下に置く場合、共通の誕生順序数の等式の向きを変え、それに合わせて組にされた誕生の添字を移します。これにより、主な三分性の右側の選択肢 `b ≺ a` が得られます。

```agda
          , subst (λ z → UnderAt z b a)
              (packBirth (bornAt a) (bornAt b) (sym same)) (hb , ha , h)))
```

整礎性には、連携する二つの降下が必要である。証明と組にされた誕生順序数 `d` を固定する。外側の仮定は、誕生が `d` より真に下にある要素の到達可能性を与え、`stepIn d` の到達可能性の木は、`d` で生まれた要素間の内側の降下を扱う。`accInside` の役割は、外側の仮定を使えるまま、この内側の木を主辞書式関係についての到達可能性へ持ち上げることである。

```agda
  private
    accInside : (d : Mem γ)
              → ((z : Mem γ) → ⟨ z .fst ∈ˢ d .fst ⟩
                 → (b : Member) → bornAt b ≡ z → Acc _≺_ b)
              → (u : New (d .fst)) → Acc (relOf (stepIn d)) u
```

局所要素 `u` が `stepIn d` で到達可能であり、段階要素 `b` の誕生が `d` で、その基礎の集合が `u` と等しいとする。主関係について `b` が到達可能だと示すには、任意の先行元 `c ≺ b` を考える。主関係の定義から、`c` に二つの降下資源のどちらを使うべきかが分かる。

```agda
              → (b : Member) → bornAt b ≡ d → b .fst ≡ u .fst → Acc _≺_ b
    accInside d ih u (acc r) b q qu = acc step
      where
      step : (c : Member) → c ≺ b → Acc _≺_ c
      step c (inl h) = ih (bornAt c)
```

`c` がより早い誕生によって `b` より前に置かれたなら、その誕生は `d` より真に下にあり、外側の帰納仮定から `c` の到達可能性が得られる。誕生が等しいなら、`c` は固定した局所順序における `u` の先行元であり、`u` の到達可能性の木が対応する小さい内側の部分木を与える。これは辞書式関係の二つの条項にちょうど対応する。

```agda
        (subst (λ v → ⟨ bornAt c .fst ∈ˢ v ⟩) (cong fst q) h) c refl
      step c (inr (eb , v)) =
        accInside d ih (c .fst , hc) (r (c .fst , hc) below) c qc refl
        where
        qc : bornAt c ≡ d
```

同じ誕生の条項では、まず基礎となる誕生順序数の等しさを、それらを `γ` の要素として証明と組にしたものの等しさへ持ち上げる。これにより `UnderAt` の比較を固定した添字 `d` へ輸送でき、その第一成分から、`c` が `stepIn d` の定義域である後続段階に属することが分かる。

```agda
        qc = packBirth (bornAt c) d (sym eb ∙ cong fst q)
        moved : UnderAt d c b
        moved = subst (λ z → UnderAt z c b) qc v
        hc : ⟨ c .fst ∈ˢ Lset (sucV (d .fst)) ⟩
        hc = moved .fst
```

輸送した `UnderAt` の証拠を、そろえた所属証明で読むと、`c` の局所代表から `b` の局所代表への比較が得られる。`b` と `u` の基礎の集合が等しいという仮定によって右端を `u` に替えると、得られた局所的な先行元の証明が `u` の下の部分木を選ぶ。再帰によって、その部分木が主順序についての `c` の到達可能性へ持ち上げられる。

```agda
        below : relOf (stepIn d) (c .fst , hc) u
        below = subst (λ z → relOf (stepIn d) (c .fst , hc) z)
          (Σ≡Prop (λ x → snd (x ∈ˢ Lset (sucV (d .fst)))) qu)
          (under-at (d .fst) (stepIn d) (c .fst) (b .fst)
            hc (moved .snd .fst) moved)
```

外側の降下は誕生順序数についての所属帰納法である。その動機は、証明と組にされた誕生が `(δ , i)` であるすべての段階要素が、主関係について到達可能だと述べる。したがって `δ` における帰納段階の仮定は、誕生順序数が真に `δ` に属する要素をちょうど覆う。

```agda
    accByBirth : (δ : S) (i : ⟨ δ ∈ˢ γ ⟩)
               → (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
    accByBirth = ∈-induction {P = Motive} outer
      where
      Motive : S → Type (ℓ-suc ℓ)
```

誕生順序数 `δ` を固定すると、局所的な狭義整列順序によって、対応する `b` の代表はすでに到達可能である。外側の帰納段階は、この局所的な到達可能性と、より早いすべての誕生に対する帰納仮定とを `accInside` に渡す。ここで外側の所属帰納法の内部に内側の降下が始まる。

```agda
      Motive δ = (i : ⟨ δ ∈ˢ γ ⟩) (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
      outer : (δ : S) → ((z : S) → ⟨ z ∈ˢ δ ⟩ → Motive z) → Motive δ
      outer δ ih i b q = accInside (δ , i) inner (b .fst , hb)
        (SWO.wf∙ (stepIn (δ , i)) (b .fst , hb)) b q refl
        where
```

等式 `q` は、証明と組にされた `b` の誕生を `(δ , i)` と同一視する。そのため `birth-mem` を輸送して、`b` を `Lset (sucV δ)` に置く証明 `hb` を得られる。より小さい、証明と組にされた誕生 `z` については、その第一成分が `δ` に属する。その順序数における外側の帰納仮定と、`z` が `γ` に属することの証明から、`z` で生まれたすべての要素の到達可能性が得られる。

```agda
        hb : ⟨ b .fst ∈ˢ Lset (sucV δ) ⟩
        hb = subst (λ z → ⟨ b .fst ∈ˢ Lset (sucV (z .fst)) ⟩) q (newIn b)
        inner : (z : Mem γ) → ⟨ z .fst ∈ˢ δ ⟩
              → (c : Member) → bornAt c ≡ z → Acc _≺_ c
        inner z h c qz = ih (z .fst) h (z .snd) c qz
```

したがって、すべての要素は主関係について到達可能である。この結論には二つの層がともに必要である。外側の所属帰納法は誕生がより早い先行元を扱い、各誕生順序数を固定したところでは、局所ステップ順序の到達可能性の木が同じ誕生の先行元を扱う。どちらか一方だけでは、この辞書式順序の整礎性は示せない。

```agda
    ≺-wf : WellFounded _≺_
    ≺-wf a = accByBirth (bornAt a .fst) (bornAt a .snd) a refl
```

ここまでに得た辞書式関係とその証明から、`Mem (Lset γ)` 上の狭義整列順序ができます。誕生順序数が第一の比較を与え、誕生が等しい場合を最小の名前によるステップ順序が決めます。

```agda
  famOrder : SWO (Mem (Lset γ))
  famOrder = record
    { _<∙_   = _≺_
    ; tri∙   = ≺-tri
    ; irr∙   = ≺-irr
```

推移性と二段階の整礎性の議論によって順序法則が揃い、すべての小さい順序数段階で仮定した順序から `famOrder` が得られます。

```agda
    ; trans∙ = ≺-trans
    ; wf∙    = ≺-wf }
```

関数 `famStep` はこの再帰の一段をまとめます。`γ` において、各要素順序数 `δ ∈ γ` ですでに構成された順序を受け取り、上で証明した `Mem (Lset γ)` 上の狭義整列順序を返します。同じ構成がどの順序数にも一様に適用され、零、後続、極限の別々の節はありません。

```agda
famStep : (γ : S) → ((δ : S) → ⟨ δ ∈ˢ γ ⟩ → IsOrd δ → SWO (Mem (Lset δ)))
        → IsOrd γ → SWO (Mem (Lset γ))
famStep = Family.famOrder
```

所属帰納法によって、すべての順序数添字で `famStep` を同時に適用します。得られる `orderAt γ` は、単一の段階 `Lset γ` の証明つき要素上にあるホスト側の狭義整列順序です。対象言語内の関係でも、`L` 全体の上の一つの関係でもありません。

```agda
opaque
  orderAt : (γ : S) → IsOrd γ → SWO (Mem (Lset γ))
  orderAt = ∈-induction famStep
```

等式 `orderAt-step` は再帰を一段だけ開きます。`γ` での順序は、各 `δ ∈ γ` ですでに構成された `orderAt δ` に `famStep γ` を適用したものです。これにより後の議論は、所属再帰全体を展開せずに誕生を先に比較する記述を使えます。

```agda
opaque
  unfolding orderAt
  orderAt-step : (γ : S) → orderAt γ ≡ famStep γ (λ δ _ → orderAt δ)
  orderAt-step = ∈-induction-compute famStep
```

最後に `stageOrder γ` は、同じ段階ごとの順序を小さい添字型 `⟪ Lset γ ⟫` 上に提示します。標準的な埋め込みは各添字を、それが表す要素と所属証明の組へ送り、`carry` はこの単射に沿って `orderAt γ` を引き戻します。変わるのは台の表示だけで、別の比較を構成するわけではありません。

```agda
stageOrder : (γ : S) → IsOrd γ → SWO ⟪ Lset γ ⟫
stageOrder γ oγ = carry (Lset γ) (orderAt γ oγ)
```

## まとめ

各順序数 `γ` に対し、`orderAt γ` は `Lset γ` の証明つき要素上にある、周囲の型理論での狭義整列順序である。まず各要素を最初に含む段階の先行者を比較し、誕生順序数が等しい場合に限って、共通の前段階上で一意に定まる最小名を比較する。局所構成 `stepAt` はどの添字でもこの一つの最小名による形をとり、大域的な整礎性の証明は、誕生順序数の降下と局所的な名前順序の降下を組み合わせる。この関係はまだ対象言語の論理式にも、`L` に属する集合にもなっていない。それらの内部化は後の章で行う。