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

本章では、数項で添字づけられた各段階が有限であることを証明し、最初の相違による整列順序を与える。さらに段階番号と局所順序を組み合わせて極限段階を整列順序づける。

先の選択の構成は、族の各セルについて、そのセルが初めて要素を持つ段階を特定し、その段階が後者であることを示した。したがって、ちょうどそこに現れるセルの各要素は、同一の集合上の定義可能部分集合、すなわち単一の段階に書かれた名前である。いまだ欠けているのは、それらの名前を**比較**する方法であり、本章が塔の底部で築くのはまさにこの比較である。

本章は二つの主張に依拠する。第一に、数項で添字づけられた各段階は有限である、という主張である。その正確な意味は下で述べる。すなわち、その段階は自身のすべての要素を含む有限な集合のリストを備える。第二に、有限段階は整列順序を担う、という主張である。これは、二つの要素をそれらが最初に相違する位置で比較し、その位置を含むほうを大きいとするものである。

第二の主張こそが数学的内容であり、本質的に**有限**集合についての主張である。同じ方式を自然数の部分集合に適用すると、無限降下が生じる。まず全自然数、次に 1 以上の全体、さらに 2 以上の全体、というように、各歩で生存者の中の最初の点を削り、厳密に低いところへ落ちていく。方式そのものはこれを禁じない。有限の基底でこれを禁じるのは、有限の基底の部分集合が有限個しかなく、したがって最小元を探す探索が必ず終わることである。以下の整礎性の証明はまさにこの方法をとる。有限なリストと線形順序があれば、非空な任意の性質に対し、リストを走査して各歩でそれまでの最小候補を保持することにより最小の要素が得られる。「非空な任意の性質は最小元を持つ」が、古典的には整礎性にほかならない。

有限性は塔を上へと伝播する。有限集合の定義可能部分集合はそのすべての部分集合であり、リストを持つ集合の部分集合は、そのリスト上の各ビットベクトルに一つずつ、有限個しかないからである。よって段階のリストから次の段階のリストが得られ、この帰納だけで構成全体を進められる。

極限段階の構成には、有限段階の順序どうしの整合性を仮定したり証明したりする必要がない。まず要素が初めて現れる段階番号を比較し、番号が等しいときだけ、その段階自身の順序を用いる。したがって異なる段階の要素は段階番号で、同じ段階に初めて現れる要素は局所順序で比較される。

舞台となるのは、周囲の累積階層 $V$ の上に構成される構成可能宇宙です。排中律はここで明示的な仮定として現れます。モジュールは、階層 `ℓ-suc ℓ` のすべての命題に対する判定を与えるパラメータ `lem` を受け取ります。本章が必要とするのはこの一つの階層だけで、以下の構成はどれもこの固定された判定を用います。表示されている定理が実際に証明する範囲を超えて、他の階層の命題については何も主張しません。

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

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

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

以下で使う名前は構成可能階層のものです。塔の段階 `Lset α`、段階の定義可能部分集合を生み出す演算子 `𝒟ₒ`、そして数項 `# n` が順序数であるという事実 `numeral-ord` です。したがって各有限段階 `Lset (# n)` は正真正銘の段階であり、これが後の節の帰納が数項を登れる理由です。ここではさらに `Lset-suc` と `FinOf` の仕組みも取り込み、段階とその内部の有限集合とを結びつけます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import L.Constructible {ℓ} using ( IsOrd; Lset; Lset-out; 𝒟ₒ; 𝒟ₒ∋⊆ )
open import L.Ordinal {ℓ} using ( numeral-ord )
open import L.Axioms.Basic {ℓ}
```

比較には三分律を満たす基底順序が必要です。自然数上の順序 `natOrder` は、厳格で強整礎な線形順序であり、`SWO` としてまとめられ、その三つの場合の比較 `Tri` は `lt`、`eq`、`gt` に分かれます。後の節の探索手続きはこのインターフェースに対して書かれているため、任意の `SWO` に適用でき、自然数の実例が数項を順序づけるものになります。

```agda
  using ( finSet; finSet-in; finSet-out; Lset-suc; module FinOf )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; leastOf; natOrder )

open import Cubical.Data.Bool using ( Bool; true; false; false≢true )
open import Cubical.Data.Nat using ( _+_ )
```

ブール値はマスクとして登場します。数え上げられた集合の部分集合を列挙するには、各項目を保持するか捨てるかを `Bool` の `true` か `false` で記録し、`false≢true` が両者を区別します。添字の側では、自然数を厳格順序 `_<_` で比較します。これは推移的かつ整礎で、`¬m<m` によりループを排除し、`_≟_` で判定可能です。これらは、ある性質を証拠立てる最小の添字を見つけるため、また走査の中で各歩の判定を下すために、まさに必要となる性質です。

```agda
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
```

ここでの整礎性は、到達可能性の述語 `Acc` で表されます。ある点が到達可能であるのはそのすべての先行元が到達可能なときであり、構成子 `acc` でまとめられます。関係のすべての点が到達可能なとき、その関係は型 `WellFounded` を持ちます。`Acc` に関する証明義務は命題であり、この事実は `isPropAcc` として記録され、「単に存在する」データから到達可能性の主張への除去に使われます。モジュール `WFI` は整礎な関係を消費する帰納原理を提供します。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded; isPropAcc; module WFI )
```

累積階層の集合 `x` に対し、`⟪ x ⟫` はその小さな表示型であり、`⟪ x ⟫↪` はその型を階層へ埋め込む。同値 `∈∈ₛ` は表示上の所属と階層の所属を結び、`∈-asFiber` は所属証明から添字とその同一視のパスを取り出す。空集合が零段階を与え、フォン・ノイマン数項 `# n` とその極限 `ω` が有限段階と極限の添字になる。

```agda
open import Cubical.Relation.Nullary using ( isProp¬ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
```

以下の所属命題は命題に値を取る。したがって `⟨ x ∈ˢ A ⟩` は `x` が `A` に属する証拠の型であり、数え上げはこの形を、各項の所属の証明と全要素が表現されるという主張の双方に用いる。

```agda
open InfinitySet using ( #_; ω )

open hPropStructure 𝒮ᵥ
```

## 有限な数え上げ

`Tally` は集合の全要素を有限添字族で提示し、重複を許し、単射性も決定可能な等しさも要求しない。

有限性は**数え上げ**として導入されます。それは、一つの数、その個数だけの集合からなりすべて `A` に属する族、そして「`A` のすべての要素はそれらのうちのどれかである」という主張です。`onto` は、すべての要素がこの族の中に単に表現されていることを記録します。

重複も等しさの決定不能性も問題にならない。走査は同じ要素を再び訪れてよく、二つの位置が同じ集合を指していても、ビットベクトルは位置ごとに選択を記録できる。したがって、この意図的に弱い有限性の概念は次の段階の構成で保たれる。

集合 `A` の数え上げは三つのデータ欄を持ちます。数 `size` が列挙する項目数を決め、`item` が各正当な位置、すなわち `Fin size` の要素を集合 `item i` に対応させ、欄 `inside` が列挙された各項目が実際に `A` に属することを証明します。これがなければ、長いリストは小さな集合を自明に被覆してしまいます。同じ要素が複数の位置に現れても構いません。record はそれを禁じず、二つの位置の集合が等しいかを尋ねる欄もありません。

```agda
record Tally (A : S) : Type (ℓ-suc ℓ) where
  field
    size   : ℕ
    item   : Fin size → S
    inside : (i : Fin size) → ⟨ item i ∈ˢ A ⟩
```

第四の欄は被覆を述べる。`x` とその `A` への所属証明から、`onto` は添字 `i` とパス `item i ≡ x` の命題的切断を返す。したがって添字は単に存在するだけで、選ばれた位置は外へ現れない。後では、この切断された証人を目標が命題である場合にだけ除去する。

```agda
    onto   : (x : S) → ⟨ x ∈ˢ A ⟩ → ∥ Σ[ i ∈ Fin size ] (item i ≡ x) ∥₁
```

## 有限添字を分割する

`splitFin` と `joinFin` は和より小さい添字を一方の加数の添字に対応させ、マスクの列挙に必要な算術を与える。

冪集合を数え上げることはビットベクトルを列挙することであり、長さ `n + 1` のベクトルの個数は長さ `n` のもののちょうど二倍です。そこで一つの添字算術が必要になります。`a + b` より小さい添字とは、`a` より小さい添字か `b` より小さい添字のどちらかであり、逆も成り立ちます。往復のうち片方向しか後で使われないため、その方向だけが証明されます。`bumpLeft` は `a` 上の再帰が型検査を通るようにするずらしです。

具体的な図が助けになります。`a = 2`、`b = 3` とすると、`5` より小さい添字とは「`2` より小さい添字か `3` より小さい添字」のいずれかにほかなりません。`joinFin` は左の加数を最初の二つの枠に、右の加数を残り三つの枠に送り、`splitFin` は一つの添字がどちらの領域に落ちたかを尋ねます。ここで重複は無関係です。これらの写像は位置についてのものであり、後にそこへ置かれる項目についてのものではないからです。

最初の写像は、左側が一つ伸びる和に関するものです。`bumpLeft` は `a` か `b` のいずれかの添字を受け取り、`suc a` か `b` のいずれかの添字を返します。左の添字は一つ先へずらされ、右の添字はそのままです。それ自体には内容はなく、`splitFin` の再帰の各歩が左の加数から一つを剥がすため、左の添字を正しい型へ戻すずらしが必要だというだけのものです。`joinFin` は `Fin a ⊎ Fin b` から `Fin (a + b)` への方向だけが与えられ、`a` は再帰がパターン照合できるよう明示されている点にも注意してください。

```agda
bumpLeft : {a b : ℕ} → Fin a ⊎ Fin b → Fin (suc a) ⊎ Fin b
bumpLeft (inl i) = inl (suc i)
bumpLeft (inr j) = inr j

joinFin : (a : ℕ) {b : ℕ} → Fin a ⊎ Fin b → Fin (a + b)
joinFin zero    (inr j)       = j
```

`joinFin` と `splitFin` は形の上では互いの逆ですが、証明される往復は一方向だけです。`joinFin` は `a` 上の再帰です。`a` が零のとき、`0 + b` より小さい添字はそのまま `b` より小さい添字であり、後者のときは最初の枠が左の加数に属するので、位置零の左の添字は零番の枠へ写り、残りはすべて一つ上へずれます。`splitFin` は同じ再帰を逆向きにたどります。`a + b` より小さい添字はまず `a` より小さいかを問い、後者の場合は `bumpLeft` で剥がされた型を復元します。

```agda
joinFin (suc a) (inl zero)    = zero
joinFin (suc a) (inl (suc i)) = suc (joinFin a (inl i))
joinFin (suc a) (inr j)       = suc (joinFin a (inr j))

splitFin : (a : ℕ) {b : ℕ} → Fin (a + b) → Fin a ⊎ Fin b
splitFin zero    j       = inr j
```

往復 `split-join` は、つねに合されたばかりの添字を分割すればもとの左か右かの添字に戻る、という主張です。各節は `refl` か再帰呼び出しに対する合同性のどちらかです。`splitFin (joinFin x)` の計算はすでに再帰の答えへの `bumpLeft` の適用に簡約され、`cong bumpLeft` がそのずらしを通して帰納仮定を運びます。逆向きの合成は主張されず、ここでは合が単射であるという主張も一切ありません。

```agda
splitFin (suc a) zero    = inl zero
splitFin (suc a) (suc i) = bumpLeft (splitFin a i)

split-join : (a : ℕ) {b : ℕ} (x : Fin a ⊎ Fin b) → splitFin a (joinFin a x) ≡ x
split-join zero    (inr j)       = refl
split-join (suc a) (inl zero)    = refl
```

この算術がマスクの節にもたらすのは、規模の正確な簿記です。長さ `suc n` のマスクの列挙が `maskCount n` で添字を半分に分けるとき、`splitFin` が先頭ビットが `false` か `true` かを決め、残りの添字を `n` での再帰に渡します。そこで `mask-onto` と `split-join` が合わさって、すべてのビットベクトルが届くことを示します。

```agda
split-join (suc a) (inl (suc i)) = cong bumpLeft (split-join a (inl i))
split-join (suc a) (inr j)       = cong bumpLeft (split-join a (inr j))
```

## マスクを列挙する

`maskAt` は固定長のすべてのブール・ベクトルを列挙し、`mask-onto` は各選択パターンが現れることを証明する。

長さ `n` の**マスク**とは `n` ビットのベクトルであり、数え上げられた集合についてどの項目を残すかを指示します。その個数は `maskCount n`、すなわち繰り返し二倍として書かれた 2 の `n` 乗です。`maskAt` は添字をマスクとして読みます。添字を半分に分け、どちらの半分に落ちたかで先頭ビットが決まり、残りが尾を与えます。すべてのマスクがなんらかの添字から読み出されること、これが `mask-onto` であり、この列挙について必要とされる唯一の性質です。逐点的な単射性は要求されません。

`n = 2` では、四つの添字が `false ∷ false ∷ []` から `true ∷ true ∷ []` までの四つのマスクを与える。この構成は実際には重複なく列挙するが、後の数え上げの議論が用いるのは証明済みの被覆 `mask-onto` だけであり、単射性には依存しない。

マスクの個数は、それを列挙する再帰そのものに沿って定義されます。長さ零のマスクはちょうど一つ、長さ `suc n` のマスクは先頭ビットと長さ `n` のマスクの組であり、個数は `maskCount n + maskCount n` となります。これは繰り返し二倍として書かれた 2 の `n` 乗であり、加えられる二つの数が等しいので、`splitFin` が期待する形に正確に一致します。

```agda
maskCount : ℕ → ℕ
maskCount zero    = 1
maskCount (suc n) = maskCount n + maskCount n

maskCons : (n : ℕ) → (Fin (maskCount n) → Vec Bool n)
         → Fin (maskCount n) ⊎ Fin (maskCount n) → Vec Bool (suc n)
```

`maskCons` は先頭ビットを、添字の対応する半分から読んだ尾に接ぎます。左の加数なら `false`、右なら `true` を選びます。そして `maskAt` が添字をマスクとして読みます。長さ零では唯一のマスクは空ベクトル、長さ `suc n` では `maskCount (suc n) = maskCount n + maskCount n` より小さい添字が半分に分けられ、落ちた半分が先頭ビットを、内側の添字が尾を名指します。この読みは定理ではなく定義であり、ただ計算するだけのものです。

```agda
maskCons n r (inl j) = false ∷ r j
maskCons n r (inr j) = true  ∷ r j

maskAt : (n : ℕ) → Fin (maskCount n) → Vec Bool n
maskAt zero    j = []
maskAt (suc n) j = maskCons n (maskAt n) (splitFin (maskCount n) j)
```

被覆こそが `mask-onto` の内容であり、ここでは意図的に切断を行いません。ベクトル `v` が与えられると、この主張は実際の添字と、そこから読んだマスクから `v` への経路とをともに作り出します。基底の場合、空ベクトルは零番の添字から来ます。列挙の中で単なる存在ではなくデータを渡さねばならないのはここだけですが、再帰がベクトルそのものに沿って進むため、それが可能になります。

```agda
mask-onto : (n : ℕ) (v : Vec Bool n) → Σ[ j ∈ Fin (maskCount n) ] (maskAt n j ≡ v)
mask-onto zero    []          = zero , refl
mask-onto (suc n) (false ∷ v) =
  joinFin (maskCount n) (inl (mask-onto n v .fst))
  , (cong (maskCons n (maskAt n)) (split-join (maskCount n) (inl (mask-onto n v .fst)))
```

後者の段階ではベクトルが分岐を決めます。先頭が `false` なら、尾の添字は `joinFin` で左半分に合され、経路は二歩で組み立てられます。まず `split-join` によって、合された添字の分割が主張どおり左半分を復元することを示し、次に `cong (false ∷_)` で再帰の経路を先頭ビットの下へ運びます。`true` の場合は右半分に替わるだけで、それ以外はそっくり同じです。個数と合わせて、これは数え上げられた集合のマスクが `Fin (maskCount size)` に被覆されることを意味し、まさに `Tally` の欄が期待する形です。

```agda
     ∙ cong (false ∷_) (mask-onto n v .snd))
mask-onto (suc n) (true ∷ v)  =
  joinFin (maskCount n) (inr (mask-onto n v .fst))
  , (cong (maskCons n (maskAt n)) (split-join (maskCount n) (inr (mask-onto n v .fst)))
     ∙ cong (true ∷_) (mask-onto n v .snd))
```

## 部分族を選び出す

`select` はブール・マスクで有限族を絞り込み、その要素補題は選ばれた項と真に印づけられた位置を対応させる。

`select` はマスクを族に適用します。ビットが `true` の項目を残し、それらを再び族として、その長さとともに返します。長さは**再帰が生み出す**ものであり、これが要点です。何かを数える必要はなく、答えとマスクを結びつける算術も要りません。

二つの仕様が結果に何が含まれるかを述べ、どちらも切断を含みません。どちらも同じ再帰から直接読み取れるからです。`marks` は逆向きに走り、項目への判定を、それを記録するマスクへ変えます。

小さな例が重複との相互作用を示します。同じ項目が二度現れる族と、両方の写しを残すマスクを取ると、選ばれた族はその項目を二度含み、二つの写しはそれぞれ固有のもとの位置とともに補題によって答えられます。何かが失われたり併合されたりすることはありません。一意であることはそもそも要求されていないからです。

補助関数 `selectStep` は絞り込みの一歩を行います。項目 `x` とすでに選ばれた族が与えられると、`x` を先頭に付け、新しい長さ `suc k` を報告します。その結果の型は族と長さを依存対としてまとめるため、再帰はマスクに算術を一切用いずに長さを伸ばせます。

```agda
selectStep : {ℓ' : Level} {X : Type ℓ'} → X → Σ[ k ∈ ℕ ] (Fin k → X)
           → Σ[ k ∈ ℕ ] (Fin k → X)
selectStep {X = X} x (k , g) = suc k , h
  where
  h : Fin (suc k) → X
```

`select` はマスク上の再帰です。空のマスクは何も選ばず、それを荒謬パターンで示します。長さ零の族には位置が存在しないからです。先頭が `false` なら頭を落としてずらした族に再帰し、`true` なら `selectStep` で頭を残します。各歩で族が一つずらされること、これが随所の `λ i → f (suc i)` が記録しているものです。

```agda
  h zero    = x
  h (suc i) = g i

select : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) → (Fin n → X) → Vec Bool n
       → Σ[ k ∈ ℕ ] (Fin k → X)
select zero    f v           = zero , λ ()
```

最初の仕様 `select-out` は選択を順方向に読みます。選ばれた族の各位置 `j` は、ビットが `true` であるもとの位置 `i` から来ており、そこにある項目は実際にもとの項目 `f i` です。この主張は単なる存在ではなくデータです。実際の証人が作り出され、ビットも等式も明示的に与えられます。

```agda
select (suc n) f (false ∷ v) = select n (λ i → f (suc i)) v
select (suc n) f (true ∷ v)  = selectStep (f zero) (select n (λ i → f (suc i)) v)

select-out : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (v : Vec Bool n)
             (j : Fin (select n f v .fst))
           → Σ[ i ∈ Fin n ] ((lookup i v ≡ true) × (select n f v .snd j ≡ f i))
```

証明は定義と同じ再帰をたどります。`false` の場合は頭が落ちているため、尾で `j` に答えるもとの位置は、全ベクトルでは `suc i` ずり上げられます。局所的な `step` がこの簿記を、証人三つ組に対してまさに行います。

```agda
select-out zero    f []          ()
select-out (suc n) f (false ∷ v) j       = step (select-out n (λ i → f (suc i)) v j)
  where
  step : Σ[ i ∈ Fin n ] ((lookup i v ≡ true)
           × (select n (λ i → f (suc i)) v .snd j ≡ f (suc i)))
```

`true` の場合は二つの下位の場合に分かれます。選ばれた位置が最初なら、答えは頭そのものであり、`select` が頭をそのまま零番の枠として返すため、二つの等式はともに `refl` で成立します。そうでなければ再帰が尾の位置に答え、同じずらしがそのまま当てはまります。

```agda
       → Σ[ i ∈ Fin (suc n) ] ((lookup i (false ∷ v) ≡ true)
           × (select (suc n) f (false ∷ v) .snd j ≡ f i))
  step (i , e , q) = suc i , (e , q)
select-out (suc n) f (true ∷ v)  zero    = zero , (refl , refl)
select-out (suc n) f (true ∷ v)  (suc j) = step (select-out n (λ i → f (suc i)) v j)
```

第二の下位の場合は同じずらしの簿記を、頭がある状態で繰り返します。`true ∷ v` の選ばれた族は頭に尾の選択が続いたものなので、頭より先の位置は尾で答えられ、`suc i` へと写し戻されます。二つの分岐が異なるのはこの配置替えだけであり、だからこそそれぞれに `step` が必要なのです。

```agda
  where
  step : Σ[ i ∈ Fin n ] ((lookup i v ≡ true)
           × (select n (λ i → f (suc i)) v .snd j ≡ f (suc i)))
       → Σ[ i ∈ Fin (suc n) ] ((lookup i (true ∷ v) ≡ true)
           × (select (suc n) f (true ∷ v) .snd (suc j) ≡ f i))
```

逆の仕様 `select-in` は、印づけられた項目はすべて選ばれることを述べます。ビットが `true` であるもとの位置 `i` には、項目が `f i` である選ばれた位置 `j` が対応します。ここでも主張は明示的なデータ、実際の `j` と経路です。どちらの向きも切断を含まないことが、後の所属の議論で選択の両側に実際の証人を渡せる理由です。

```agda
  step (i , e , q) = suc i , (e , q)

select-in : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (v : Vec Bool n)
            (i : Fin n) → lookup i v ≡ true
          → Σ[ j ∈ Fin (select n f v .fst) ] (select n f v .snd j ≡ f i)
select-in zero    f []          ()      e
```

その証明は同じ再帰を逆向きに映します。空の族の位置は荒謬であり、`false` の場合は頭が真に印づけられることはないので仮定 `e` は `false≢true` と矛盾し、ずらされた位置は再帰します。`true` の場合は頭が零番の位置で答え、より深い位置は再帰します。

```agda
select-in (suc n) f (false ∷ v) zero    e = Empty.rec (false≢true e)
select-in (suc n) f (false ∷ v) (suc i) e = select-in n (λ i → f (suc i)) v i e
select-in (suc n) f (true ∷ v)  zero    e = zero , refl
select-in (suc n) f (true ∷ v)  (suc i) e = step (select-in n (λ i → f (suc i)) v i e)
  where
```

最後の節は先頭付けの簿記を行います。尾で見つかった位置は、頭が前に付いた族では `suc j` となり、項目の等式はそのまま保たれます。二つの仕様を合わせると、選択はマスクが印づけたものより大きくも小さくもないことが分かりますが、位置の対応の二つの仕方が互いに逆であるという主張はありません。

```agda
  step : Σ[ j ∈ Fin (select n (λ i → f (suc i)) v .fst) ]
           (select n (λ i → f (suc i)) v .snd j ≡ f (suc i))
       → Σ[ j ∈ Fin (select (suc n) f (true ∷ v) .fst) ]
           (select (suc n) f (true ∷ v) .snd j ≡ f (suc i))
  step (j , q) = suc j , q
```

`marks` は絞り込みを逆向きに使います。マスクを読んで項目を残す代わりに、項目へのブールの判定 `d` を受け取り、それを記録するマスクを書き出します。一位置につき一ビットです。基底は空ベクトルで、ステップは頭で `d` を尋ね、ずらした族に再帰します。

```agda
marks : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) → (Fin n → X) → (X → Bool) → Vec Bool n
marks zero    f d = []
marks (suc n) f d = d (f zero) ∷ marks n (λ i → f (suc i)) d

marks-lookup : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (d : X → Bool)
               (i : Fin n) → lookup i (marks n f d) ≡ d (f i)
```

`marks-lookup` は、記録されたマスクが各位置で判定に正しく答えることを裏付けます。`marks n f d` の位置 `i` を参照すると `d (f i)` が得られます。頭の場合は `marks` の計算規則により `refl` であり、深い位置は再帰します。この補題があるため、後の `maskOf` が書き出したマスクが与えられた部分集合を再現することを証明できるのです。

```agda
marks-lookup (suc n) f d zero    = refl
marks-lookup (suc n) f d (suc i) = marks-lookup n (λ i → f (suc i)) d i
```

## 真理値を一ビットに決定する

排中律は各命題をマスクで使うブール値へ変え、二つの仕様はそのビットから真と偽をそれぞれ読み戻す。

排中律が渡すのは論理和であり、マスクが必要とするのは一ビットです。そこで両者をつなぐ必要があります。判定は定義の内部で求めるのではなく実引数として受け取ります。これにより二つの往復補題は判定に対する照合で証明でき、真理値そのものも明示的に与え、往復の仕様が意図した命題を引数に取るようにします。

この変換は、数え上げの構成における排中律の具体的な用途の一つである。所属命題を判定し、その答えを一ビットとして記録する。

`decideOf` は判定を一ビットへ変えます。左の選択肢、すなわち `⟨ P ⟩` の証明は `true` として記録され、右の選択肢、`⟨ P ⟩` の反証は `false` となります。命題 `P` 自体は計算に関係せず、照合されるのは判定だけです。だからこそこの定義は一組の等式であって証明ではありません。

```agda
decideOf : (P : hProp (ℓ-suc ℓ)) → (⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → Bool
decideOf P (inl _) = true
decideOf P (inr _) = false

decide-true : (P : hProp (ℓ-suc ℓ)) (s : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → ⟨ P ⟩ → decideOf P s ≡ true
decide-true P (inl _)  p = refl
```

二つの往復がビットを真理値へと結び戻します。`decide-true` は、`⟨ P ⟩` の証明がビットを `true` に強いることを述べます。反証の分岐ではその証明自体が反証され、それが矛盾です。`decide-sound` は逆向きに読みます。ビットが `true` なら `⟨ P ⟩` の証明が得られ、左の分岐から直接取られるか、右の分岐が `false ≡ true` を強いることになるために得られます。合わせて、渡された判定に対してビットが `⟨ P ⟩` の成立を忠実に答えることを示します。

```agda
decide-true P (inr np) p = Empty.rec (np p)

decide-sound : (P : hProp (ℓ-suc ℓ)) (s : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → decideOf P s ≡ true → ⟨ P ⟩
decide-sound P (inl p) _ = p
decide-sound P (inr _) e = Empty.rec (false≢true e)
```

## 数え上げられた段階の定義可能部分集合

有限性はこの節を通して塔を一段ずつ上ります。順序数 `σ` と段階 `Lset σ` の数え上げを固定し、目標は `𝒟ₒ (Lset σ)` (この段階の定義可能部分集合全体) の数え上げを得ることです。与えられた数え上げの各項目はその段階の要素ですから、段階の小さな要素型の中に対応する名前を持ちます。マスクはどの名前を残すかを指定し、`part` は残った名前を有限集合に張り合わせます。基本公理の章の `finSet∈𝒟ₒ` により、こうして張られた集合はその段階の定義可能部分集合であり、「これらの項目のいずれかに等しい」という有限論理和で定義されます。逆に、段階の任意の定義可能部分集合 `x` も復元できます。各項目を `x` への決定可能な所属関係に従って印づけると、そのマスクで張った集合はちょうど `x` になります。ここで包含 `𝒟ₒ∋⊆` が、`x` の各要素がそもそも数え上げに列挙されていることを保証します。したがって `maskCount size` 個のマスクがすべての定義可能部分集合を単に覆っており、これこそ `Tally` が要求する性質です。

`Lset σ` の要素は集合としてその段階にありますが、`finSet` には小さな要素型 `⟪ Lset σ ⟫` の名前が必要です。埋め込み `⟪ Lset σ ⟫↪` はその名前を集合として読みます。所属は切り詰められたファイバーとして提示されますが、この埋め込みのファイバーは命題なので、`∈-asFiber` は切り詰めを消去し、明示的な名前と、それが `item i` に等しいというパスを返せます。`index i` と `index-eq i` は、このファイバー要素の二つの射影です。重複を許す有限な数え上げの任意のファイバーから添字を選ぶこととは異なり、そちらのファイバーは命題とは限りません。

```agda
module PowerStep (σ : S) (oσ : IsOrd σ) (t : Tally (Lset σ)) where
  open Tally t
  open FinOf σ oσ using ( finSet∈𝒟ₒ )

  index : Fin size → ⟪ Lset σ ⟫
  index i = ∈-asFiber {a = item i} {b = Lset σ} (inside i) .fst
```

同じファイバーの第二成分が経路 `index-eq i` であり、埋め込まれた名前が定義等式ではなく経路を介して `item i` に戻ることを記録します。以後、集合 `item i` と名前 `index i` の間のすべての移し替えは、この経路に沿った輸送を通して行われます。名前がそろったところで、数え上げ上のマスク `v` は選択に変換されます。`chosen v` は長さと、選ばれた名前をちょうど列挙する関数の組であり、以前の `select` が構成したものです。

```agda
  index-eq : (i : Fin size) → ⟪ Lset σ ⟫↪ (index i) ≡ item i
  index-eq i = ∈-asFiber {a = item i} {b = Lset σ} (inside i) .snd

  chosen : Vec Bool size → Σ[ k ∈ ℕ ] (Fin k → ⟪ Lset σ ⟫)
  chosen v = select size index v

  part : Vec Bool size → S
```

`part` は張り合わせた集合です。選ばれた各名前を埋め込みを通して読み出し、その結果の有限集合を作り、集合の型 `S` に着地します。`Lset σ` の要素からなる有限族はその段階の定義可能部分集合を張るので、`part-def` は `finSet∈𝒟ₒ` から証明書 `⟨ part v ∈ˢ 𝒟ₒ (Lset σ) ⟩` を追加の仕事なしに得ます。最初の仕様は所属を逆向きに読みます。`y` が `part v` に属するなら、ビットが `true` でありその項目が `y` に等しい数え上げの位置が、単に存在するということです。

```agda
  part v = finSet (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j))

  part-def : (v : Vec Bool size) → ⟨ part v ∈ˢ 𝒟ₒ (Lset σ) ⟩
  part-def v = finSet∈𝒟ₒ (chosen v .fst) (chosen v .snd)

  part-out : (v : Vec Bool size) (y : S) → ⟨ y ∈ˢ part v ⟩
           → ∥ Σ[ i ∈ Fin size ] ((lookup i v ≡ true) × (item i ≡ y)) ∥₁
```

証明は二つの段階を合成します。まず `finSet-out` が張り合わせた有限集合における所属をほどき、選択の中の位置 `j` と、埋め込まれた名前が `y` に等しいことを単に生み出します。次に `select-out` がその位置を完全な数え上げの中での由来までたどり、`lookup i v ≡ true` と `chosen v .snd j ≡ index i` を満たす添字 `i` を回復します。どちらの段階でもデータは截断の中で生み出されるので、単なる存在主張から選ばれた証人が取り出されることはありません。

```agda
  part-out v y y∈ = PT.map step
    (finSet-out (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j)) y y∈)
    where
    step : Σ[ j ∈ Fin (chosen v .fst) ] (⟪ Lset σ ⟫↪ (chosen v .snd j) ≡ y)
         → Σ[ i ∈ Fin size ] ((lookup i v ≡ true) × (item i ≡ y))
```

最後に必要な等式の向きは `item i ≡ y` です。まず `sym (index-eq i)` で `item i` から埋め込まれた名前 `index i` へ進みます。次に `select-out` が `chosen v .snd j ≡ index i` を与えるので、その対称を埋め込みの下へ写して、選ばれた埋め込み名へ進みます。最後に有限集合への所属が与えるパス `q` で `y` に到達します。この三つの合成が、証明に表示されたパス列そのものです。

```agda
    step (j , q) = out .fst
                 , ( out .snd .fst
                   , (sym (index-eq (out .fst))
                      ∙ cong ⟪ Lset σ ⟫↪ (sym (out .snd .snd)) ∙ q) )
      where
```

逆向きの仕様は順方向に働きます。位置 `i` のビットが `true` なら、項目 `item i` は実際に `part v` に属します。理由は、選択がその名前を本当に含んでいるからです。`select-in` は印づけられた各位置に対して、選ばれた族の中で同じ名前を保持する枠を見つけ、続いて `finSet-in` がその埋め込み形の所属を証明します。

```agda
      out : Σ[ i ∈ Fin size ] ((lookup i v ≡ true) × (chosen v .snd j ≡ index i))
      out = select-out size index v j

  part-mem : (v : Vec Bool size) (i : Fin size) → lookup i v ≡ true
           → ⟨ item i ∈ˢ part v ⟩
  part-mem v i e = subst (λ w → ⟨ w ∈ˢ part v ⟩) path
```

張り合わせた集合における所属は埋め込まれた名前について述べられているのに対し、目標は項目 `item i` に関するので、両者は下の経路 `path` で結ばれ、`subst` がその経路に沿って所属の証明を移します。補助の `ins` は `select-in` が生み出す枠を保持します。選ばれた族の中で、その項目が `index i` に等しい位置です。

```agda
    (finSet-in (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j))
      (⟪ Lset σ ⟫↪ (chosen v .snd (ins .fst))) ∣ ins .fst , refl ∣₁)
    where
    ins : Σ[ j ∈ Fin (chosen v .fst) ] (chosen v .snd j ≡ index i)
    ins = select-in size index v i e
```

残りの経路 `path` は枠の等式と `index-eq i` をつなぎ合わせるので、輸送された所属はまさに `item i` の所属です。両方向がそろったところで、構成を逆向きに走らせます。`maskOf` は任意の集合 `x` に対して、各数え上げの項目が `x` に属するかどうかを判定して得られる判定マスクを割り当てます。排中律 `lem` が論理和を供給し、`decideOf` がそれを一ビットに変えます。目標 `part-mask` は、段階の定義可能部分集合 `x` に対して、このマスクで張った集合が `x` そのものであると述べています。

```agda
    path : ⟪ Lset σ ⟫↪ (chosen v .snd (ins .fst)) ≡ item i
    path = cong ⟪ Lset σ ⟫↪ (ins .snd) ∙ index-eq i

  maskOf : S → Vec Bool size
  maskOf x = marks size item (λ y → decideOf (y ∈ˢ x) (lem (y ∈ˢ x)))

  part-mask : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩ → part (maskOf x) ≡ x
```

階層の集合における所属は命題なので、外延性 `extensionalV` は主張された等式 `part (maskOf x) ≡ x` を、所属の主張の各点ごとの同値へと帰着させます。`⇔toPath` が二つの方向を経路へと組み立てます。順方向は、張り合わせた集合の各要素が `x` に属することを示します。

```agda
  part-mask x x∈ = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
    where
    fwd : (y : S) → ⟨ y ∈ˢ part (maskOf x) ⟩ → ⟨ y ∈ˢ x ⟩
    fwd y y∈ = PT.rec (snd (y ∈ˢ x)) step (part-out (maskOf x) y y∈)
      where
```

順方向の仮定はそれ自体が単なる存在主張です。ビットが `true` で項目が `y` に等しい位置が何かあるということです。目標 `⟨ y ∈ˢ x ⟩` は命題なので、截断はその中へと消去できます。記録された証人は位置 `i` であり、そのビットは `true` で項目は `y` です。このビットはまさにその項目の `x` への所属を判定して計算されたものですから、`decide-sound` でビットを読み戻せば `item i` の `x` への所属が得られ、等式 `item i ≡ y` によってそれを `y` へと輸送します。

```agda
      step : Σ[ i ∈ Fin size ] ((lookup i (maskOf x) ≡ true) × (item i ≡ y))
           → ⟨ y ∈ˢ x ⟩
      step (i , e , q) = subst (λ w → ⟨ w ∈ˢ x ⟩) q
        (decide-sound (item i ∈ˢ x) (lem (item i ∈ˢ x))
          (sym (marks-lookup size item
```

逆方向は `y` の `x` への所属から出発し、張り合わせた集合への所属を生み出さねばなりません。この目標も再び命題なので、その截断された仮定は消去できます。ここでの仮定は数え上げの被覆から来ます。`x` は段階の定義可能部分集合であり、`𝒟ₒ∋⊆` は `Lset σ` の定義可能部分集合の各要素が `Lset σ` 自身の要素でもあると言うので、数え上げの `onto` が `y` をある項目 `item i` として単に列挙します。

```agda
                 (λ z → decideOf (z ∈ˢ x) (lem (z ∈ˢ x))) i) ∙ e))
    bwd : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ part (maskOf x) ⟩
    bwd y y∈x = PT.rec (snd (y ∈ˢ part (maskOf x))) step
      (onto y (𝒟ₒ∋⊆ (Lset σ) x x∈ y y∈x))
      where
```

`y` に等しい項目 `i` が与えられれば、`item i` が張り合わせた集合に属することを示し、`item i ≡ y` に沿って輸送すれば十分です。`part-mem` により、所属には位置 `i` のビットが `true` であることが必要です。そして実際そうです。マスクは `item i ∈ˢ x` の判定を記録しており、`y` が `x` に属するので、経路 `item i ≡ y` がその証明を輸送し、`decide-true` がビットを `true` に強制します。

```agda
      step : Σ[ i ∈ Fin size ] (item i ≡ y) → ⟨ y ∈ˢ part (maskOf x) ⟩
      step (i , q) = subst (λ w → ⟨ w ∈ˢ part (maskOf x) ⟩) q
        (part-mem (maskOf x) i
          (marks-lookup size item (λ z → decideOf (z ∈ˢ x) (lem (z ∈ˢ x))) i
           ∙ decide-true (item i ∈ˢ x) (lem (item i ∈ˢ x))
```

`part-mask` の両方向がこれで組み上がり、この節の収穫が目の前にあります。`mask-onto` によりすべてのマスクがある添字から生じるので、マスクは (繰り返しを許して、単に)`Lset σ` のすべての定義可能部分集合を列挙します。その個数は `maskCount size` ですから、`powerTally` はその大きさの数え上げを記録します。添字 `j` における項目は、マスク `maskAt size j` で張った集合です。残りの欄が記録を完成させます。各項目は定義可能性の証明書を伴い、被覆の条項はこの次に与えられます。

```agda
               (subst (λ w → ⟨ w ∈ˢ x ⟩) (sym q) y∈x)))

  powerTally : Tally (𝒟ₒ (Lset σ))
  powerTally = record
    { size   = maskCount size
    ; item   = λ j → part (maskAt size j)
```

記録の `inside` の欄は、列挙された各マスクで証明書 `part-def` を再利用するので、`powerTally` の各項目は実際に段階の定義可能部分集合です。残るは `onto`、つまり截断された被覆の確認です。`Lset σ` の任意の定義可能部分集合 `x` が与えられたとき、列挙された項目が `x` に等しい添字を単に示せばよいことになります。

```agda
    ; inside = λ j → part-def (maskAt size j)
    ; onto   = cover }
    where
    cover : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩
          → ∥ Σ[ j ∈ Fin (maskCount size) ] (part (maskAt size j) ≡ x) ∥₁
```

証人となる添字は、判定マスク `maskOf x` に対して `mask-onto` が生み出すものです。その添字で列挙される項目は `part (maskAt size j)` であり、生み出された経路に沿ってマスクを書き換えれば `part (maskOf x)` に等しく、続いて `part-mask` がそれを `x` と同一視します。命題全体が截断の中に着地します。これが `Tally` の被覆が要求するすべてであり、すべての定義可能部分集合が命中するものの、一意なマスクによるとは限りません。

```agda
    cover x x∈ = ∣ mask-onto size (maskOf x) .fst
                 , (cong part (mask-onto size (maskOf x) .snd) ∙ part-mask x x∈) ∣₁
```

## 最小要素と整礎性

この節では、先につくった数え上げを使う側の議論を進めます。型と、その上の三岐・非反射・推移的な関係を固定します。これは整列順序が要求する性質のうち整礎性を除くすべてです。手続き `scan` は有限族をたどり、截断を一切伴わずに、述語を満たし満たすものの中で最小である項目か、満たす項目が存在しないことの反駁を返します。長さについての素朴な再帰です。各段階で排中律が頭部での述語を判定し、三岐性が頭部とそれまでの最良の候補を比較します。四つの組み合わせが四つの節です。どこにも截断がないことが重要です。呼び出し側が求めるのは単なる存在ではなく実際の要素だからです。族が型全体を単に被覆するという仮定の下で、`Search.Over.least` はこれを「型全体上の任意の単に非空な述語の最小要素」へと引き上げます。満たす項目がないという枝は、述語がそのファイバーを命中させねばならない証人によって反駁されます。整礎性はその後、最小の反例の議論によって導かれ、そのコードのところで述べます。

`A` 上の狭義関係 `≺` が三岐性・非反射性・推移性を満たすとする。整礎性は仮定せず、有限な被覆族から導く。述語 `P` に対し、`Least P m` は `m` が `P` を満たすことと、より小さい充足者がすべて矛盾を導くことを記録する。

```agda
module Search {A : Type (ℓ-suc ℓ)} (_≺_ : A → A → Type (ℓ-suc ℓ))
              (tri : (a b : A) → Tri (a ≺ b) (a ≡ b) (b ≺ a))
              (irr : (a : A) → a ≺ a → Empty.⊥)
              (trans : (a b c : A) → a ≺ b → b ≺ c → a ≺ c) where

  Least : (P : A → hProp (ℓ-suc ℓ)) → A → Type (ℓ-suc ℓ)
```

走査の出力型 `Found P n f` は二つの明示的な選択肢の論理和です。左の選択肢では、ある位置 `i` が `P` を満たす項目を保持し、族の中でそれより下に `P` を満たす他の項目はありません。右の選択肢では、すべての項目が述語を満たしません。どちらの選択肢も截断された存在ではなく完全なデータを運ぶので、後の構成が実際の要素を返せます。

```agda
  Least P m = ⟨ P m ⟩ × ((b : A) → ⟨ P b ⟩ → b ≺ m → Empty.⊥)

  Found : (P : A → hProp (ℓ-suc ℓ)) (n : ℕ) (f : Fin n → A) → Type (ℓ-suc ℓ)
  Found P n f =
    (Σ[ i ∈ Fin n ] (⟨ P (f i) ⟩ × ((j : Fin n) → ⟨ P (f j) ⟩ → f j ≺ f i → Empty.⊥)))
    ⊎ ((i : Fin n) → ⟨ P (f i) ⟩ → Empty.⊥)
```

`scan` は族の長さについての再帰で定義されます。空の族は空虚に右の選択肢を返します。頭部を持つ族では、再帰がまず尾を (位置を一つずらして) 処理し、頭部での `P` に対する排中律の判定が `combine` に渡されます。`combine` は尾の結果と頭部の判定を族全体の結果へと統合します。

```agda
  scan : (P : A → hProp (ℓ-suc ℓ)) (n : ℕ) (f : Fin n → A) → Found P n f
  scan P zero    f = inr (λ ())
  scan P (suc n) f = combine (scan P n (λ i → f (suc i))) (lem (P (f zero)))
    where
    combine : Found P n (λ i → f (suc i))
```

`combine` の最初の節は、尾がすでに最小の充足者 `f (suc i)` を与え、頭部も述語を満たす場合を扱います。ここでは二つの候補が競い、三岐性が `f zero` と `f (suc i)` のどちらが小さいかを判定します。補助の `decide` がその比較の三通りの結果を分析します。

```agda
            → (⟨ P (f zero) ⟩ ⊎ (⟨ P (f zero) ⟩ → Empty.⊥)) → Found P (suc n) f
    combine (inl (i , pi , mi)) (inl p₀) = decide (tri (f zero) (f (suc i)))
      where
      decide : Tri (f zero ≺ f (suc i)) (f zero ≡ f (suc i)) (f (suc i) ≺ f zero)
             → Found P (suc n) f
```

頭部が尾の優位者より狭義に小さければ、頭部が新しい優位者になります。その最小性は位置ごとに確かめられます。頭部自身では `f zero ≺ f zero` の主張は非反射性と直ちに矛盾し、尾の位置では推移性が `f j ≺ f zero ≺ f (suc i)` をつなぎ、その結果を尾で確立済みの最小性 `mi` に渡します。

```agda
      decide (lt h) = inl (zero , (p₀ , minAt))
        where
        minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → Empty.⊥
        minAt zero    pj hj = irr (f zero) hj
        minAt (suc j) pj hj = mi j pj (trans (f (suc j)) (f zero) (f (suc i)) hj h)
```

頭部が尾の現在の最小候補と等しければ、その候補は引き続き最小である。頭部が候補より小さいという仮定は、両者の等式に沿って候補自身より小さいという比較へ輸送され、非反射性に反する。尾の位置は引き続き `mi` が扱う。

```agda
      decide (eq h) = inl (suc i , (pi , minAt))
        where
        minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → Empty.⊥
        minAt zero    pj hj = irr (f (suc i)) (subst (λ w → w ≺ f (suc i)) h hj)
        minAt (suc j) pj hj = mi j pj hj
```

尾の優位者が頭部より狭義に小さければ、優位者は生き残ります。優位者の下にあると仮定した要素には二つの落ち方が生じます。頭部を経由する推移性 `f (suc i) ≺ f zero ≺ f (suc i)` が非反射性で反駁される自己比較を生み、尾自身の位置は `mi` に渡されます。優位者の証明書はどの枝でも古い証明書から組み立て直されるのです。

```agda
      decide (gt h) = inl (suc i , (pi , minAt))
        where
        minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → Empty.⊥
        minAt zero    pj hj = irr (f (suc i)) (trans (f (suc i)) (f zero) (f (suc i)) h hj)
        minAt (suc j) pj hj = mi j pj hj
```

二つ目の節は、頭部が述語を満たさない場合に尾の優位者を保ちます。比較はまったく要りません。頭部は `P` を満たさないので優位者に挑戦できず、頭部での仮想の反例は判定 `n₀` によって直接反駁され、尾の位置はやはり `mi` に渡されます。

```agda
    combine (inl (i , pi , mi)) (inr n₀) = inl (suc i , (pi , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → Empty.⊥
      minAt zero    pj hj = Empty.rec (n₀ pj)
      minAt (suc j) pj hj = mi j pj hj
```

対称的に、尾に充足者がまったくなく頭部が述語を満たす場合は、頭部が新しい優位者です。その最小性は直ちに得られます。頭部自身は非反射性で処理され、述語を満たす尾の位置があれば尾の反駁 `none` と矛盾します。

```agda
    combine (inr none) (inl p₀) = inl (zero , (p₀ , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → Empty.⊥
      minAt zero    pj hj = irr (f zero) hj
      minAt (suc j) pj hj = Empty.rec (none j pj)
```

最後の節は一致の場合です。尾にも頭にも充足者がいないので、族全体が何も満たさないと報告されます。反駁は位置ごとに組み立てられ、頭部は `n₀` に、各尾の位置は `none` に回されます。これで導入部に予告した四つの組み合わせがそろいました。

```agda
    combine (inr none) (inr n₀) = inr atAll
      where
      atAll : (i : Fin (suc n)) → ⟨ P (f i) ⟩ → Empty.⊥
      atAll zero    p = n₀ p
      atAll (suc i) p = none i p
```

副モジュール `Over` は、有限族を数え上げへと変えるための唯一の前提を追加します。`cov` は `A` のすべての要素が族によって単に命中されると言うもので、重複を許す截断的被覆です。この前提のもとで `least` は走査の答えを型全体への最小要素へと引き上げます。入力は「ある要素が `P` を満たす」という截断された証人だけですが、出力は明示的なデータ、すなわち要素と `Least P m` の組です。

```agda
  module Over (n : ℕ) (f : Fin n → A)
              (cov : (a : A) → ∥ Σ[ i ∈ Fin n ] (f i ≡ a) ∥₁) where

    least : (P : A → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ A ] ⟨ P a ⟩ ∥₁ → Σ[ m ∈ A ] Least P m
    least P h = decide (scan P n f)
      where
```

`least` の内部で、補助の `nowhere` は走査の「充足者なし」の枝を処理します。どの項目も `P` を満たさないと仮定したとき、与えられた截断された証人を反駁せねばなりません。この消去が正当なのは、目標が命題である空の型だからで、証人の截断は何も選ばずにほどけます。

```agda
      nowhere : ((i : Fin n) → ⟨ P (f i) ⟩ → Empty.⊥) → Empty.⊥
      nowhere none = PT.rec Empty.isProp⊥ atWitness h
        where
        atWitness : Σ[ a ∈ A ] ⟨ P a ⟩ → Empty.⊥
        atWitness (a , pa) = PT.rec Empty.isProp⊥
```

具体的には、証人が要素 `a` と `⟨ P a ⟩` を与え、被覆 `cov a` が `f i ≡ a` を満たす族の位置 `i` を単に指し示します。ここでも目標は命題なのでファイバーを読めます。`⟨ P a ⟩` の証明を `f i ≡ a` に沿って逆向きに輸送すれば `⟨ P (f i) ⟩` が得られ、仮定した反駁 `none` がそれを矛盾に変えます。続く行がまさにこの輸送を行います。

```agda
          (λ { (i , q) → none i (subst (λ w → ⟨ P w ⟩) (sym q) pa) }) (cov a)
      decide : Found P n f → Σ[ m ∈ A ] Least P m
      decide (inl (i , pi , mi)) = f i , (pi , everywhere)
        where
        everywhere : (b : A) → ⟨ P b ⟩ → b ≺ f i → Empty.⊥
```

先に予告した輸送がここで、両成分にわたって一度に行われます。型全体の中で優位者の下にあると仮定した項目 `b` と `⟨ P b ⟩`、`b ≺ f i` が与えられると、被覆が `f j ≡ b` を満たす族の位置 `j` を単に指し示します。充足と比較の両方をその経路に沿って逆向きに輸送すれば、優位者の族レベルの証明書 `mi` が両者をまとめて反駁します。したがって走査に残る唯一の枝である反駁 `none` は完全に矛盾します。証人が必ず族の中に充足者を引き込むことが示されたからです。

```agda
        everywhere b pb hb = PT.rec Empty.isProp⊥
          (λ { (j , q) → mi j (subst (λ w → ⟨ P w ⟩) (sym q) pb)
                              (subst (λ w → w ≺ f i) (sym q) hb) }) (cov b)
      decide (inr none) = Empty.rec (nowhere none)

    wellFounded : WellFounded _≺_
```

整礎性を示すため、まず任意の `a` の到達可能性を判定する。肯定の場合は証明をそのまま返す。否定の場合、有限走査により、到達可能性が反駁される最小の要素 `m` を得る。`m` のすべての前駆が到達可能なら `acc below` が `m` の到達可能性を与え、`found` に保存された `m` の反駁をこの証明に適用して矛盾を得る。もとの `a` の反駁は、非到達可能という述語が非空であることを示すためだけに用いる。

```agda
    wellFounded a = fromDec (lem (Acc _≺_ a , isPropAcc a))
      where
      fromDec : (Acc _≺_ a ⊎ (Acc _≺_ a → Empty.⊥)) → Acc _≺_ a
      fromDec (inl h) = h
      fromDec (inr nh) = Empty.rec (found .snd .fst (acc below))
```

最小化の対象となる性質は `NotAcc`、すなわち到達不可能性です。その下にある主張は否定であり、否定は命題なので、`NotAcc` は正当な真理値 `Ω` であり、`least` を適用できます。入力は `a` と仮定された反駁 `nh` の截断された組であり、仮定は単に到達不能な要素の集まりが空でないと言っているにすぎません。

```agda
        where
        NotAcc : A → hProp (ℓ-suc ℓ)
        NotAcc b = (Acc _≺_ b → Empty.⊥) , isProp¬ _
        found : Σ[ m ∈ A ] Least NotAcc m
        found = least NotAcc ∣ a , nh ∣₁
```

今求めた最小の到達不能要素を `m` とします。これが到達可能であることを示すには、すべての前駆 `b` が到達可能であることを示さねばならず、`b` の到達可能性もまた命題なので、再び排中律で判定します。補助の `pick` が肯定の枝で証明書を返します。

```agda
        below : (b : A) → b ≺ found .fst → Acc _≺_ b
        below b hb = pick (lem (Acc _≺_ b , isPropAcc b))
          where
          pick : (Acc _≺_ b ⊎ (Acc _≺_ b → Empty.⊥)) → Acc _≺_ b
          pick (inl h)  = h
```

否定の枝では、`b` は最小の到達不能要素 `m` より狭義に小さい到達不能要素となるはずで、`Least NotAcc m` の最小性の条項がまさにそれを反駁します。したがってすべての前駆が到達可能であり、証明書 `acc below` は正当で、仮定された到達可能性の反駁に与えることで矛盾が閉じます。無限下降列が構成されたり排除されたりしたのではなく、議論は完全にこの矛盾によるものです。

```agda
          pick (inr nb) = Empty.rec (found .snd .snd b nb hb)
```

## 最初の相違

この節は、有限段階が担う順序を定義します。集合 `A` と、集合の上の関係 `R` を固定します。`R` は `A` の要素の上の順序と読みます。`A` の二つの部分集合は、どこで食い違うかによって比較されます。「`x` が `y` に先行する」ことの証人は、`A` の要素 `z` であって、`y` に属し `x` には属さず、かつ `x` と `y` が `z` の下で**一致**するものです。つまり `R` が `z` の前に置く `A` の各要素は、一方に属するならばちょうど他方にも属するということです。逆向きに読めば、`z` が最初の相違点であり、それを持つのが `y` です。関係 `precedes R A` はそのような証人の截断された存在であり、非反射性は直ちに成り立ち、まったく仮定を要しません。`x` 自身に対する証人は `x` に属すると同時に属さないことになるからです。続く証明は基底の順序への仮定から三岐性と推移性を確立し、整礎性には有限性を用います。

二つの材料は別々に述べられます。`Agrees R A x y z` は、`R` が `z` の前に置く `A` の各要素 `w` について、`x` への所属と `y` への所属が双方向に一致することを言います。`Witness R A x y z` は続いて完全な証人を組み立てます。`z` は `A` に属し、`y` に属し、`x` には属さず、その下で一致が成り立つ、ということです。所属条項の向きこそが、比較でどちらが勝つかを決めます。

```agda
Agrees : (R : S → S → hProp (ℓ-suc ℓ)) (A x y z : S) → Type (ℓ-suc ℓ)
Agrees R A x y z = (w : S) → ⟨ w ∈ˢ A ⟩ → ⟨ R w z ⟩
                 → (⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩) × (⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩)

Witness : (R : S → S → hProp (ℓ-suc ℓ)) (A x y z : S) → Type (ℓ-suc ℓ)
Witness R A x y z =
```

`precedes R A x y` は、そのような証人が単に存在するという命題であり、`PT.squash₁` とともに真理値としてまとめられています。証人は截断の後ろに隠れているので、主張されるのはその存在だけで、`z` が選ばれることはありません。非反射性はそこで一行で済みます。截断を命題である空の型へと消去すれば、`z ∈ x` と `z ∉ x` を同時に持つ証人が現れ、第二の条項を第一に施せば矛盾です。

```agda
  ⟨ z ∈ˢ A ⟩ × ⟨ z ∈ˢ y ⟩ × (⟨ z ∈ˢ x ⟩ → Empty.⊥) × Agrees R A x y z

precedes : (R : S → S → hProp (ℓ-suc ℓ)) (A : S) → S → S → hProp (ℓ-suc ℓ)
precedes R A x y = ∥ Σ[ z ∈ S ] Witness R A x y z ∥₁ , PT.squash₁

precedes-irrefl : (R : S → S → hProp (ℓ-suc ℓ)) (A x : S) → ⟨ precedes R A x x ⟩ → Empty.⊥
precedes-irrefl R A x = PT.rec Empty.isProp⊥ (λ { (z , _ , z∈ , z∉ , _) → z∉ z∈ })
```

最初の相違による順序の推移性と三岐性は、基底の順序への仮定を indeed 必要とし、しかも両者は異なる仮定を要するので、一つのモジュールにまとめられます。そのパラメータは、`A` の要素の上での `R` の三岐性と推移性、およびそれらの要素の上での `R` の最小要素原理です。塔の中では、これらは下の段階から供給されます。

推移性は二つの証人の比較です。`x` が `p` で `y` に先行し、`y` が `q` で `z` に先行するなら、`p` は `y` に属し `q` は属さないので `p` と `q` は等しくありえず、両者のうち小さいほうが `x` が `z` に先行することの証人となります。どちらの枝でも確かめることは同じ二つです。小さいほうの点が正しい側にあることと、その下での一致が合成できることです。

このモジュールは、最初の相違の順序が受け継ぐ三つの前提を集めます。`baseTri` と `baseTrans` は、`A` の要素に制限した `R` が三岐かつ推移的であると言い、`baseLeast` は `A` の上の最小要素原理です。`A` の要素のある性質が単に非空であることから、その性質を満たし、より小さい `A` の要素がどれも満たさない要素を返します。結論の形に注意してください。呼び出し側が実際の最小要素を必要とするので、截断ではなく明示的なデータです。

```agda
module Difference (R : S → S → hProp (ℓ-suc ℓ)) (A : S)
  (baseTri : (a b : S) → ⟨ a ∈ˢ A ⟩ → ⟨ b ∈ˢ A ⟩ → Tri ⟨ R a b ⟩ (a ≡ b) ⟨ R b a ⟩)
  (baseTrans : (a b c : S) → ⟨ R a b ⟩ → ⟨ R b c ⟩ → ⟨ R a c ⟩)
  (baseLeast : (P : S → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × ⟨ P a ⟩) ∥₁
             → Σ[ m ∈ S ] (⟨ m ∈ˢ A ⟩ × ⟨ P m ⟩
```

推移性の主張は、二つの仮定を `precedes` が生み出す通りの形で受け取ります。`x ≺ y` と `y ≺ z` の截断された証人を受け取り、`x ≺ z` の截断された証人を返します。したがって証明は、最初の截断を消去し、次に第二の截断を消去することから始まります。どちらの目標も再び截断であり、したがって命題です。

```agda
                 × ((b : S) → ⟨ b ∈ˢ A ⟩ → ⟨ P b ⟩ → ⟨ R b m ⟩ → Empty.⊥)))
  where

  precedes-trans : (x y z : S) → ⟨ precedes R A x y ⟩ → ⟨ precedes R A y z ⟩
                 → ⟨ precedes R A x z ⟩
  precedes-trans x y z hxy hyz =
```

両方の証人が現れたところで、`both` は完全なデータを受け取ります。`x` が `y` に先行することの証人である点 `p` とその所属条項 `agp`、そして `y` が `z` に先行することの証人である点 `q` とその `agq` です。二つの基底点の比較は基底の三岐性に委ねられ、補助の `decide` がその三通りの結果を分析します。

```agda
    PT.rec PT.squash₁ (λ wp → PT.rec PT.squash₁ (both wp) hyz) hxy
    where
    both : Σ[ p ∈ S ] Witness R A x y p → Σ[ q ∈ S ] Witness R A y z q
         → ⟨ precedes R A x z ⟩
    both (p , p∈A , p∈y , p∉x , agp) (q , q∈A , q∈z , q∉y , agq) =
```

`p` が `q` より狭義に小さければ、`p` が `x` の `z` への先行の証人であり続けます。それ自身の条項は `x` と `y` だけに関わるのでそのまま引き継がれ、確かめるべきなのは `p` が `z` に属することと、`p` の下で `x` と `z` の一致が成り立つことです。`z` への所属は点 `p` での `agq` から来ます。`p` の `y` への所属を合成された比較を通して輸送するのです。

```agda
      decide (baseTri p q p∈A q∈A)
      where
      decide : Tri ⟨ R p q ⟩ (p ≡ q) ⟨ R q p ⟩ → ⟨ precedes R A x z ⟩
      decide (lt h) = ∣ p , (p∈A , (agq p p∈A h .fst p∈y , (p∉x , ag))) ∣₁
        where
```

`p` の下での一致は条項ごとに合成されます。`w ∈ x` が `w ∈ z` を導くことを示すには、`agp` が `w ∈ x` を `w ∈ y` に引き上げ、続いて `agq` が `y` への所属を `z` まで引き上げます。その際、基底の推移性によって `w` が `q` の下にもあることを使います。逆向きの条項は対称で、`z` を `y` へ、さらに `x` へと下ろします。等しい場合は起こりえません。`p` は `y` に属し `q` は属さないので、経路 `p ≡ q` に沿って所属を輸送すれば矛盾が得られます。

```agda
        ag : Agrees R A x z p
        ag w w∈A hw =
            (λ wx → agq w w∈A (baseTrans w p q hw h) .fst (agp w w∈A hw .fst wx))
          , (λ wz → agp w w∈A hw .snd (agq w w∈A (baseTrans w p q hw h) .snd wz))
      decide (eq h) = Empty.rec (q∉y (subst (λ v → ⟨ v ∈ˢ y ⟩) h p∈y))
```

逆に `q` が `p` より狭義に小さければ、役割が入れ替わり、`q` が `x` の `z` への先行を証明します。`y` と `z` に関する条項はそのまま引き継げますが、`x` への所属と一致を確立せねばなりません。所属については、点 `q` で `agp` を読むと `q` の `x` への所属が `y` への所属へと輸送され、`q ∉ y` と矛盾します。補助の `q∉x` がこの反駁をまとめます。

```agda
      decide (gt h) = ∣ q , (q∈A , (q∈z , (q∉x , ag))) ∣₁
        where
        q∉x : ⟨ q ∈ˢ x ⟩ → Empty.⊥
        q∉x qx = q∉y (agp q q∈A h .fst qx)
        ag : Agrees R A x z q
```

`q` の下での一致は鏡像の順で合成されます。まず `agp` が `q ≺ p` と基底の推移性によって `w` を `p` の下に置き、`x` への所属を `y` へと押し下げ、続いて `agq` がそれを `z` まで引き上げます。逆向きの条項はまず `z` を `y` へ、さらに `x` へと下ろします。二つの非対称な場合が処理され、等しい場合は反駁されたので、推移性が完成します。

```agda
        ag w w∈A hw =
            (λ wx → agq w w∈A hw .fst (agp w w∈A (baseTrans w q p hw h) .fst wx))
          , (λ wz → agp w w∈A (baseTrans w q p hw h) .snd (agq w w∈A hw .snd wz))
```

三分法は、排中律と最小要素原理が実際に使われる箇所である。まず、二つの部分集合が `A` のどこかに相違点を持つかを問う。持たなければ、両者は `A` の至る所で一致する。さらにどちらも `A` の中にとどまるので、もともと至る所で一致しており、外延性が両者を同一視する。持てば、最初の相違点が存在し、もう一つの判定、すなわちその点が第一の部分集合に属するかどうかによって、比較の向きが決まる。その点より下での一致はどちらの分岐でも自動的に成り立つ。その点の選び方から、それより下に相違点はないからである。

排中律は `agree` の内部で二度目に使われ、「相違しない」を「一致する」へ変える。この一歩はまさに二重否定の除去である。

この定理は `A` の二つの部分集合 `x`、`y` を定義可能性の証明書としてではなく、普通の集合として受け取り、それぞれが `A` の中にとどまるという前提を添える。結論は本章で一貫して使われる三分の判断 `Tri`、すなわち `x` が `y` に先立つか、集合として等しいか、`y` が `x` に先立つかである。証明はまず `Some` について排中律を問うことに始まる。`Some` は命題、つまり截断された存在文として構成されるので、`PT.squash₁` をその命題性の証明として `lem` に渡せる。

```agda
  precedes-tri : (x y : S) → ((w : S) → ⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ A ⟩)
                           → ((w : S) → ⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ A ⟩)
               → Tri ⟨ precedes R A x y ⟩ (x ≡ y) ⟨ precedes R A y x ⟩
  precedes-tri x y x⊆ y⊆ = decide (lem (Some , PT.squash₁))
    where
```

二つの截断がこの問いを組織する。述語 `Apart w` は、`w` が二つの部分集合を区別すること、向きは問わず、片方には属しもう片方には属さないことを、単に主張する。截断型 `Some` は、`A` のある要素が相違点であることを単に主張する。どちらも `PT.squash₁` を添え、命題であってデータではない。これこそが、排中律による判定、さらに `Some` の反駁を矛盾への除去を正当化する。

```agda
    Apart : S → hProp (ℓ-suc ℓ)
    Apart w = ∥ (⟨ w ∈ˢ x ⟩ × (⟨ w ∈ˢ y ⟩ → Empty.⊥))
              ⊎ ((⟨ w ∈ˢ x ⟩ → Empty.⊥) × ⟨ w ∈ˢ y ⟩) ∥₁ , PT.squash₁
    Some : Type (ℓ-suc ℓ)
    Some = ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × ⟨ Apart a ⟩) ∥₁
```

補題 `agree` は「相違の不在」を「一致」へ変える。一度に一方向ずつである。前提 `na` は `Apart w` を反駁し、結論は `w` における所属同値の二つの包含節である。証明が否定形の命題から所属蕴含を作り出す必要があるのはここだけで、それは実質的に二重否定の除去となる。

```agda
    agree : (w : S) → (⟨ Apart w ⟩ → Empty.⊥)
          → (⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩) × (⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩)
    agree w na = fwd , bwd
      where
      fwd : ⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩
```

前向きの節では、`w ∈ˢ x` を仮定し、`w ∈ˢ y` について排中律を問う。成り立てばそれで足りる。反駁 `nh` が得られたなら、実は `w` は相違点であり、左の選択肢 `wx , nh` がその証人である。この証人を截断に包んで `na` に渡せば矛盾が得られ、`Empty.rec` がそこから所望の要素、ここでは欠けた所属の証明を作る。目標 `Empty.⊥` は命題なので、截断された `Apart w` をそこへ除去するのは正当である。

```agda
      fwd wx = pick (lem (w ∈ˢ y))
        where
        pick : (⟨ w ∈ˢ y ⟩ ⊎ (⟨ w ∈ˢ y ⟩ → Empty.⊥)) → ⟨ w ∈ˢ y ⟩
        pick (inl h)  = h
        pick (inr nh) = Empty.rec (na ∣ inl (wx , nh) ∣₁)
```

後向きの節はその鏡像である。`w ∈ˢ y` を仮定し、排中律が `w ∈ˢ x` を判定する。反駁が得られたなら、右の選択肢 `nh , wy` を通じて `w` は相違点となり、`na` がまさにそれを反駁する。二つの節を合わせれば、`w` に差異の点が存在しない限り、`x` への所属と `y` への所属は `w` で一致する、ということになる。

```agda
      bwd : ⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩
      bwd wy = pick (lem (w ∈ˢ x))
        where
        pick : (⟨ w ∈ˢ x ⟩ ⊎ (⟨ w ∈ˢ x ⟩ → Empty.⊥)) → ⟨ w ∈ˢ x ⟩
        pick (inl h)  = h
```

次に `Some` が反駁されたとする。つまり `A` の中に相違点はない。補題 `nApart` はこれを `Apart` の各点での反駁として包み、`same` はすべての `w` でそれを用いて二つの集合の相等を証明する。反駁された証人が `A` に属するという前提は次で処理され、その後 `agree` の所属同値が各点で適用できる。

```agda
        pick (inr nh) = Empty.rec (na ∣ inr (nh , wy) ∣₁)
    same : (Some → Empty.⊥) → x ≡ y
    same ns = extensionalV step
      where
      nApart : (w : S) → ⟨ Apart w ⟩ → Empty.⊥
```

二つの部分集合が `A` の中にある限り、相違点は必ず `A` に属する。実際、截断された選言 `ha` は命題 `w ∈ˢ A` へと除去される。左の選言肢が成り立てば `w` は `x` に属し、`x⊆` がそれを `A` へ移す。右が成り立てば `y⊆` が同様に扱う。除去の向きに注意。命題値の所属関係への除去であり、これこそ命題的截断が許すことである。

```agda
      nApart w ha = ns ∣ w , (inA , ha) ∣₁
        where
        inA : ⟨ w ∈ˢ A ⟩
        inA = PT.rec (snd (w ∈ˢ A))
          (λ { (inl (wx , _)) → x⊆ w wx ; (inr (_ , wy)) → y⊆ w wy }) ha
```

各 `w` で、`agree w (nApart w)` の二つの節は、`x` への所属と `y` への所属が同値であると主張する。コンビネータ `⇔toPath` は、二つの命題 `w ∈ˢ x` と `w ∈ˢ y` の間のこの同値を、型としての両者の間のパスへ引き上げる。これは累積階層の外延性が受け取る形である。各点のパスを `extensionalV` に渡せばパス `x ≡ y` が得られ、三分法の `eq` の分岐が閉じる。

```agda
      step : (w : S) → (w ∈ˢ x) ≡ (w ∈ˢ y)
      step w = ⇔toPath (agree w (nApart w) .fst) (agree w (nApart w) .snd)
    decide : (Some ⊎ (Some → Empty.⊥))
           → Tri ⟨ precedes R A x y ⟩ (x ≡ y) ⟨ precedes R A y x ⟩
    decide (inr ns) = eq (same ns)
```

もう一方の分岐では `Some` が成立する。つまり `A` のある要素が相違点である。`A` の要素上の基底順序 `R` に対して使える最小要素原理 `baseLeast` を述語 `Apart` に適用すると、截断された存在ではなく明示的なレコード `found` が返る。`A` に属し相違している点 `m` で、`R` 順序の下ではそれより下に相違点がない。この明示性こそが、最小の相違点を後に証人として使える理由である。

```agda
    decide (inl hs) = side (lem (m ∈ˢ x))
      where
      found : Σ[ m ∈ S ] (⟨ m ∈ˢ A ⟩ × ⟨ Apart m ⟩
                × ((b : S) → ⟨ b ∈ˢ A ⟩ → ⟨ Apart b ⟩ → ⟨ R b m ⟩ → Empty.⊥))
      found = baseLeast Apart hs
```

`found` の各成分は一度ほどいて名前を与えられる。点 `m`、`A` への所属 `m∈A`、相違性 `apartM`、最小性 `belowM` である。それぞれに名を付けておくことで、以下の対称な二つの分岐が読みやすくなる。両者ともこれらの欄のいくつかを引用するからである。

```agda
      m : S
      m = found .fst
      m∈A : ⟨ m ∈ˢ A ⟩
      m∈A = found .snd .fst
      apartM : ⟨ Apart m ⟩
```

最小性の欄 `belowM` は、`m` より真に下にある相違点を反駁する。ここでは比較の仮定が末尾に来るよう引数の順を組み替えており、今後の使用に適する。最小の相違点を手にすれば、最後にもう一度排中律が `m` が `x` に属するかを判定し、`side` がそれぞれの答えを三分法の一分岐へ変える。

```agda
      apartM = found .snd .snd .fst
      belowM : (w : S) → ⟨ w ∈ˢ A ⟩ → ⟨ R w m ⟩ → ⟨ Apart w ⟩ → Empty.⊥
      belowM w w∈A hw ha = found .snd .snd .snd w w∈A ha hw
      side : (⟨ m ∈ˢ x ⟩ ⊎ (⟨ m ∈ˢ x ⟩ → Empty.⊥))
           → Tri ⟨ precedes R A x y ⟩ (x ≡ y) ⟨ precedes R A y x ⟩
```

`m` が実際に `x` に属するなら、`m` は `y` が `x` に先立つことの証人である。第二の集合に属し第一には属さないからである。補題 `m∉y` は、截断された `apartM` の場合分けによって `m ∈ˢ y` を反駁する。左の選言肢では証人自身が `m ∈ˢ y` の反駁を帯びており、右では `m ∈ˢ x` の反駁が `mx` と衝突する。目標 `Empty.⊥` が命題であるため、この截断の除去は許される。

```agda
      side (inl mx) = gt ∣ m , (m∈A , (mx , (m∉y , ag))) ∣₁
        where
        m∉y : ⟨ m ∈ˢ y ⟩ → Empty.⊥
        m∉y my = PT.rec Empty.isProp⊥
          (λ { (inl (_ , nmy)) → nmy my ; (inr (nmx , _)) → nmx mx }) apartM
```

`m` より下での一致も、向きの交換がただで手に入る。`m` より下の各 `w` に対し `belowM` が `Apart w` を反駁するので `agree w` が適用でき、両方向の所属同値が得られる。組を逆向きに書き並べるだけで、元は `x` から `y` へ向いていた一致から `Agrees R A y x m` が作られる。`m∈A`、`mx`、`m∉y` と合わせて、これは `y` が `x` に先立つことの完全な `Witness` であり、`gt` が截断の中で渡す。

```agda
        ag : Agrees R A y x m
        ag w w∈A hw = agree w (belowM w w∈A hw) .snd , agree w (belowM w w∈A hw) .fst
      side (inr nmx) = lt ∣ m , (m∈A , (my , (nmx , ag))) ∣₁
        where
        my : ⟨ m ∈ˢ y ⟩
```

鏡像の分岐は、代わりに `m` が `x` に属さないと仮定し、`x` が `y` に先立つことの `lt` の証人を作る。`apartM` から `m ∈ˢ y` を取り出すのもまた截断の場合分けである。左の選言肢は `m ∈ˢ x` を主張することになり `nmx` が反駁するので、右の選言肢だけが生き残り、それは所属をそのまま帯びている。今回 `m` より下の一致は向きの交換を要しない。証人の向きが `agree` の作るものと一致しているからである。対称な二つの分岐がそろい、`precedes` の三分法が完成し、段階上の局所順序は整礎性を残して要素上の線順序となる。

```agda
        my = PT.rec (snd (m ∈ˢ y))
          (λ { (inl (mx , _)) → Empty.rec (nmx mx) ; (inr (_ , h)) → h }) apartM
        ag : Agrees R A x y m
        ag w w∈A hw = agree w (belowM w w∈A hw)
```

## 有限段階

数項上の再帰により、数え上げと最初の相違による整列順序を各有限段階から次の段階へ同時に運ぶ。

数項で添字づけられた段階こそ有限の段階であり、各段階上の順序は再帰によって構成される。段階零は空であり、`n` の後者の段階上の順序は、段階 `n` 自身の順序を基底として、段階 `n` の定義可能部分集合を最初の相違点で比較するものである。`before-irrefl` はすべての段階で成立し、帰納を要しない。この比較の非反射性は前提を要さず、段階零にはそもそも比較が存在しないからである。

定義は、三分の判断のための小さな道具から始まる。`Tri-map` は `Tri` の選言肢ごとに関数を一つ適用するものであり、三つの節がその計算規則である。これは、二つの集合について証明された三分法を、段階の二つの点について必要な三分法へ変換するのに使われる。両者は所属の証明を帯びるかどうかだけが違う。

```agda
Tri-map : {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level}
          {A₁ : Type ℓ₁} {B₁ : Type ℓ₂} {C₁ : Type ℓ₃}
          {A₂ : Type ℓ₄} {B₂ : Type ℓ₅} {C₂ : Type ℓ₆}
        → (A₁ → A₂) → (B₁ → B₂) → (C₁ → C₂) → Tri A₁ B₁ C₁ → Tri A₂ B₂ C₂
Tri-map f g h (lt a) = lt (f a)
```

数項で添字づけられた段階に名が与えられる。`finiteStage n` は段階 `Lset (# n)` である。関係 `before` は続いて添字上の再帰である。零では偽の真理値が取られ、いかなる対も関係されない。後者では `precedes` を一つ下の段階に適用したものである。所属を比較する基底集合は段階 `n` そのもの、最初の相違点を探す際にたどる基底順序は一段下で再帰が作った `before n` である。

```agda
Tri-map f g h (eq b) = eq (g b)
Tri-map f g h (gt c) = gt (h c)

finiteStage : ℕ → S
finiteStage n = Lset (# n)

before : ℕ → S → S → hProp (ℓ-suc ℓ)
```

`before` の非反射性はすべての数項で成立し、その証明は帰納を行わない。零では前提は偽の真理値の住人であり、`Empty.rec*` がそれを除去する。後者ではまさに `precedes-irrefl`、つまりこの比較を定義した際に前提なしで確立された非反射性である。だからこそ、非反射性は再帰が運ぶべきデータには入らない。

```agda
before zero    x y = ⊥
before (suc n) = precedes (before n) (finiteStage n)

before-irrefl : (n : ℕ) (x : S) → ⟨ before n x x ⟩ → Empty.⊥
before-irrefl zero    x h = Empty.rec* h
before-irrefl (suc n) x h = precedes-irrefl (before n) (finiteStage n) x h
```

基底の場合の空性は `zero-empty` として別に記録される。段階零の要素となる集合はない。`Lset (# zero)` から所属の証明書を読み出すと、単に、`δ` が数項零の要素で `x` が `Lset δ` の定義可能部分集合であるようなある段階 `δ` が得られるだけである。数項零に要素はなく、`∅-empty` がいかなる所属の主張も矛盾へ変える。目標 `Empty.⊥` が命題であるため、この截断の除去は正当である。

```agda
zero-empty : (x : S) → ⟨ x ∈ˢ finiteStage zero ⟩ → Empty.⊥
zero-empty x h = PT.rec Empty.isProp⊥ step (Lset-out (# zero) x h)
  where
  step : Σ[ δ ∈ S ] (⟨ δ ∈ˢ ∅ ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) → Empty.⊥
  step (δ , δ∈ , _) = ∅-empty δ (∈∈ₛ {a = δ} {b = ∅} .fst δ∈)
```

再帰が運ぶべきデータは、要素の数え上げ、三分法、推移性の三つだけであり、それ以外には何もない。非反射性はすべての段階で自動的に成立し、整礎性は使う箇所でその場で導出されるので、運ぶ必要はない。段階の点とは集合にその所属の証明を添えたものであり、所属は命題なので、二つの点は集合が等しければただちに等しい。「集合についての述定」と「台が型でなければならない束」との間を行き来するのに必要な作業は、これだけである。

前節の探索機構は型の上で働くので、段階の要素は `Point` として包まれる。すなわち、集合に `finiteStage n` への所属の証明書を添えたものである。関係 `Below` は根底の集合で `before n` を読む。所属は命題なので、同じ集合を持つ二つの点ははじめから等しい。この一事実が、「集合についての述定」と「点についての述定」との間の行き来のすべての作業を担う。

```agda
Point : ℕ → Type (ℓ-suc ℓ)
Point n = Σ[ x ∈ S ] ⟨ x ∈ˢ finiteStage n ⟩

Below : (n : ℕ) → Point n → Point n → Type (ℓ-suc ℓ)
Below n a b = ⟨ before n (a .fst) (b .fst) ⟩

record StageOrder (n : ℕ) : Type (ℓ-suc ℓ) where
```

段階 `n` の帰納は、後者の一歩に必要な事実だけを保つ。すなわち `finiteStage n` の数え上げ、その段階の要素に対する `before n` の三岐性、そして任意の集合に対する `before n` の推移性である。非反射性は最初の相違から一様に従い、局所順序の整礎性は必要なときに数え上げから得られる。

```agda
  field
    tally : Tally (finiteStage n)
    tri   : (x y : S) → ⟨ x ∈ˢ finiteStage n ⟩ → ⟨ y ∈ˢ finiteStage n ⟩
          → Tri ⟨ before n x y ⟩ (x ≡ y) ⟨ before n y x ⟩
    trans : (x y z : S) → ⟨ before n x y ⟩ → ⟨ before n y z ⟩ → ⟨ before n x z ⟩
```

`Ordered` の内部での最初の課題は、点についての三分法である。`triPoint` は集合についての三分法 `tri` を `Tri-map` に渡す。中央の選言肢は結論がパスなので変換が要り、`Σ≡Prop` がまさにそれを供給する。第二成分は命題の証明であるから、根底の集合の間のパスは点の間のパスへ延長できる。

```agda
module Ordered (n : ℕ) (r : StageOrder n) where
  open StageOrder r public
  open Tally tally

  triPoint : (a b : Point n) → Tri (Below n a b) (a ≡ b) (Below n b a)
  triPoint a b = Tri-map id (Σ≡Prop (λ z → snd (z ∈ˢ finiteStage n))) id
```

数え上げは、各項にそれ自身の所属の証明を対にすることで、集合から点へ引き上げられ `points` となる。被覆の述定 `covers` は、この対を通して `onto` を運んだものである。点が与えられれば、`onto` は同じ集合を持つ項の添字を単に提供し、`Σ≡Prop` が集合の等式を点の等式へ引き上げる。被覆は数え上げ自身と同様、截断されたままである。

```agda
    (tri (a .fst) (b .fst) (a .snd) (b .snd))

  points : Fin size → Point n
  points i = item i , inside i

  covers : (a : Point n) → ∥ Σ[ i ∈ Fin size ] (points i ≡ a) ∥₁
  covers a = PT.map (λ { (i , q) → i , Σ≡Prop (λ z → snd (z ∈ˢ finiteStage n)) q })
```

段階の点について、三岐性・非反射性・推移性を有限な数え上げと合わせると二つの帰結が得られる。有限走査は単に非空な任意の述語に最小の点を与え、同じ最小反例の議論が点の関係の整礎性を与える。

```agda
    (onto (a .fst) (a .snd))

  open Search (Below n) triPoint (λ a → before-irrefl n (a .fst))
              (λ a b c → trans (a .fst) (b .fst) (c .fst)) public
  open Over size points covers public

  order : SWO (Point n)
```

これらの事実は `finiteStage n` の点上の狭義整列順序を定める。関係は `Before n`、三つの順序法則は段階内の比較から、整礎性は有限走査から得られる。この構成では局所的な比較と、無限降下を排除する有限性の議論が明確に分かれている。

```agda
  order = record
    { _<∙_   = Below n
    ; tri∙   = triPoint
    ; irr∙   = λ a → before-irrefl n (a .fst)
    ; trans∙ = λ a b c → trans (a .fst) (b .fst) (c .fst)
```

最後の補題は、最小要素を次の段階が必要とする形に包む。`leastMem` は、段階のある要素に単に満たされる集合上の述語 `P` を受け取り、`P` を満たす明示的な要素 `m` を、`before n` 順序での最小性、すなわち `P` を満たす段階の要素 `b` で `m` より真に下にあるものが存在しないこととともに返す。前提を除けば、ここに截断はない。

```agda
    ; wf∙    = wellFounded }

  leastMem : (P : S → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ finiteStage n ⟩ × ⟨ P a ⟩) ∥₁
           → Σ[ m ∈ S ] (⟨ m ∈ˢ finiteStage n ⟩ × ⟨ P m ⟩
               × ((b : S) → ⟨ b ∈ˢ finiteStage n ⟩ → ⟨ P b ⟩
                          → ⟨ before n b m ⟩ → Empty.⊥))
```

証明は点の水準で探索を走らせ、結果をほどく。`least` を引き上げた述語と包装し直した截断的証人に適用すると、明示的な対、点 `m` とその `Least` の証明書が返る。点の三つの成分と証明書の二つの成分を集合水準の述定へ組み立て直し、最小性の節は証明書を対 `b , b∈` に適用することで作られる。

```agda
  leastMem P h = found .fst .fst
               , ( found .fst .snd
                 , ( found .snd .fst
                   , (λ b b∈ pb hb → found .snd .snd (b , b∈) pb hb) ) )
    where
```

残るのは接合だけである。`Q` は点の根底の集合で集合水準の述語を読み、`found` は三つ組から「点と証明の対」へ包装し直した截断的前提で `least` を呼ぶ。この `leastMem` こそ、後者の段階で再帰が `baseLeast` として `Difference` に渡すものであり、探索機構と最初の相違の順序との環を閉じる。

```agda
    Q : Point n → hProp (ℓ-suc ℓ)
    Q a = P (a .fst)
    found : Σ[ m ∈ Point n ] Least Q m
    found = least Q (PT.map (λ { (a , a∈ , pa) → (a , a∈) , pa }) h)
```

再帰は零段階の空の数え上げと、空性から従う順序法則から始まる。後者段階では、一つ前の数え上げを定義可能冪集合へ持ち上げる。最初の相違による比較は、二つの部分集合条件から三岐性を与え、前段階の順序から推移性を直接与える。後者段階の同一視を使うのは、段階とその定義可能冪集合の間で所属を移す箇所だけである。

基底の場合、三つの欄を一つのレコードに組み立てる。それらはまさに今示した三つの小さな事実である。数え上げ `empty` のサイズは零である。添字型 `Fin zero` は空なので、項と所属の欄は荒謬パターン、すなわち与えられない引数に対する関数で与えられる。段階零には列挙すべきものがなく、それがこの数え上げの内容のすべてである。

```agda
stageOrder : (n : ℕ) → StageOrder n
stageOrder zero = record { tally = empty ; tri = triZero ; trans = transZero }
  where
  empty : Tally (finiteStage zero)
  empty = record
```

零段階の数え上げの残る欄も、同じ事実から得られる。添字が存在しないため、列挙された項の所属証明は生じようがなく、段階の被覆は `zero-empty` から従う。`finiteStage zero` の要素を仮定すれば矛盾が得られるからである。したがって `empty` は両方向で空の段階を正確に列挙している。

```agda
    { size   = zero
    ; item   = λ ()
    ; inside = λ ()
    ; onto   = λ x x∈ → Empty.rec (zero-empty x x∈) }
  triZero : (x y : S) → ⟨ x ∈ˢ finiteStage zero ⟩ → ⟨ y ∈ˢ finiteStage zero ⟩
```

二つの順序の欄は空虚である。零での三分法は `x` と `y` の所属の証明書を受け取るが、そのような証明書は存在しないので、`zero-empty` が一つ目から矛盾を取り出して目標を処理する。零での推移性は型が `before zero x y` である前提を受け取るが、`before` の計算規則によりそれは偽の真理値であり、`Empty.rec*` が除去する。空の前提が空の結論を作る。この順序が空であること以外に、空の順序の性質は使われない。

```agda
          → Tri ⟨ before zero x y ⟩ (x ≡ y) ⟨ before zero y x ⟩
  triZero x y x∈ y∈ = Empty.rec (zero-empty x x∈)
  transZero : (x y z : S) → ⟨ before zero x y ⟩ → ⟨ before zero y z ⟩
            → ⟨ before zero x z ⟩
  transZero x y z h k = Empty.rec* h
```

後者の一歩が段階 `n` から必要とする数学的入力は、その最小要素原理、`before n` の三岐性と推移性、そして要素の数え上げである。前二者により最初の相違はその段階の部分集合上の狭義比較となり、数え上げはブールマスクを通してそれらの部分集合を列挙する。これらが段階 `suc n` に必要な数え上げと順序法則を与える。

```agda
stageOrder (suc n) = record { tally = raised ; tri = triSuc ; trans = transSuc }
  where
  module Prev = Ordered n (stageOrder n)
  module Diff = Difference (before n) (finiteStage n) Prev.tri Prev.trans Prev.leastMem
  module Power = PowerStep (# n) (numeral-ord n) Prev.tally
```

同一視 `step` はパス `Lset-suc (# n)` であり、`n` の後者の段階が段階 `n` の定義可能冪集合であると述べる。新しい数え上げ `raised` は冪数え上げのサイズと項をそのまま保つので、列挙するのは同じ定義可能部分集合である。変わるのは所属の証明書をどこから読むかだけであり、そこに `step` が現れる。

```agda
  step : finiteStage (suc n) ≡ 𝒟ₒ (finiteStage n)
  step = Lset-suc (# n)

  raised : Tally (finiteStage (suc n))
  raised = record
    { size   = Tally.size Power.powerTally
```

`inside` の欄は、各所属の証明書を `step` の逆向きに沿って定義可能冪集合から後者の段階へ輸送する。証明書が証明するのは冪集合への所属であり、数え上げが主張するのは `Lset (# suc n)` への所属だからである。対称的に、`onto` は後者の段階への所属の証明書を受け取り、`step` に沿って前向きに輸送してから冪数え上げの被覆を呼ぶ。どちらの向きでも輸送は一句の所属の述定にだけ働く。

```agda
    ; item   = Tally.item Power.powerTally
    ; inside = λ i → subst (λ w → ⟨ Tally.item Power.powerTally i ∈ˢ w ⟩) (sym step)
                       (Tally.inside Power.powerTally i)
    ; onto   = λ x x∈ → Tally.onto Power.powerTally x
                          (subst (λ w → ⟨ x ∈ˢ w ⟩) step x∈) }
```

補題 `members` は、`precedes-tri` が要求する包含の前提を取り出す。段階 `n` の定義可能部分集合の要素はすべて段階 `n` にある。それが `𝒟ₒ∋⊆` であり、定義可能冪集合への所属から逆向きに読むものである。まず `step` に沿って `x` の証明書を冪集合へ輸送すれば、得られるものは関数である。`x` の各要素 `w` に対し、`w` が段階 `n` にあることの証明書を与える。

```agda
  members : (x : S) → ⟨ x ∈ˢ finiteStage (suc n) ⟩
          → (w : S) → ⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ finiteStage n ⟩
  members x x∈ = 𝒟ₒ∋⊆ (finiteStage n) x (subst (λ v → ⟨ x ∈ˢ v ⟩) step x∈)

  triSuc : (x y : S) → ⟨ x ∈ˢ finiteStage (suc n) ⟩ → ⟨ y ∈ˢ finiteStage (suc n) ⟩
         → Tri ⟨ before (suc n) x y ⟩ (x ≡ y) ⟨ before (suc n) y x ⟩
```

後者の二つの欄は今や一行の適用である。`before (suc n)` は定義により `precedes (before n) (finiteStage n)` だから、`triSuc` は二つの包含の前提を `members` が供給する `Diff.precedes-tri` である。`transSuc` はそのまま `Diff.precedes-trans` であり、前提ははじめから正しい形をしている。再帰はここで閉じる。各段階の順序の事実は一つ下の段階の事実であり、最初の相違の理論がそれを消費する。

```agda
  triSuc x y x∈ y∈ = Diff.precedes-tri x y (members x x∈) (members y y∈)

  transSuc : (x y z : S) → ⟨ before (suc n) x y ⟩ → ⟨ before (suc n) y z ⟩
           → ⟨ before (suc n) x z ⟩
  transSuc = Diff.precedes-trans
```

## 極限段階

`Lset ω` の各要素に最小の有限レベルを与え、まずレベルを、次に局所的な段階順序を比較して、極限段階の整列順序を得る。

`Lset ω` の要素は、ある数項で添字づけられた有限段階に現れる。その出現段階の中から自然数の最小要素探索で最小のものを取り、それを要素の**レベル**と呼ぶ。異なるレベル間の降下を組み立てる際にも、自然数の整礎性を再び用いる。

極限の要素は `Limit` として包まれる。すなわち集合に `Lset ω` への所属の証明書を添えたものである。補題 `inSome` はそのような証明書を、その集合がある有限段階に現れるという截断された述定へ変換する。極限段階から証明書を読み出すと、`ω` に属しその集合が `Lset δ` の定義可能部分集合であるようなある `δ` が単に得られるだけである。外側の除去の目標は截断型であり、それは命題なので除去は正当である。

```agda
Limit : Type (ℓ-suc ℓ)
Limit = Σ[ x ∈ S ] ⟨ x ∈ˢ Lset ω ⟩

inSome : (x : S) → ⟨ x ∈ˢ Lset ω ⟩ → ∥ Σ[ n ∈ ℕ ] ⟨ x ∈ˢ finiteStage n ⟩ ∥₁
inSome x h = PT.rec PT.squash₁ atStage (Lset-out ω x h)
  where
```

残るのは `ω` より下の添字 `δ` を同定することである。所属 `δ ∈ ω` は、持ち上げられた自然数 `k` が存在して `δ` が数項 `# (lower k)` に等しいという切断された主張である。`PT.map` により切断の内部でこの数項の証人を用いると、パスが `𝒟ₒ (Lset δ)` に関する定義可能部分集合の証明を `Lset (# lower k)` 上のものへ書き換え、`Lset-suc` が `x` を `finiteStage (suc (lower k))` に置く。これにより、添字 `ω` と段階 `Lset ω` を混同せずに有限段階での出現が示される。

```agda
  atStage : Σ[ δ ∈ S ] (⟨ δ ∈ˢ ω ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
          → ∥ Σ[ n ∈ ℕ ] ⟨ x ∈ˢ finiteStage n ⟩ ∥₁
  atStage (δ , δ∈ω , x∈) = PT.map named δ∈ω
    where
    named : Σ[ k ∈ Lift ℕ ] (# (lower k) ≡ δ) → Σ[ n ∈ ℕ ] ⟨ x ∈ˢ finiteStage n ⟩
```

数項に名が付いたので、`named` が実際の出現段階を作る。`Lset-suc` が `Lset (# (suc k))` を `Lset (# k)` の定義可能冪集合と同一視するので、その集合が `Lset (# (lower k))` の定義可能部分集合であることの証明書は、`sym (Lset-suc ...)` に沿って輸送され、`finiteStage (suc (lower k))` への所属となる。したがって出現段階を添字づける数項は、`ω` の内部に現れる数項より一つ大きい。これは添字とその後者の段階の間の、いつもの一つずれである。

```agda
    named (k , q) = suc (lower k)
      , subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-suc (# (lower k))))
          (subst (λ w → ⟨ x ∈ˢ 𝒟ₒ (Lset w) ⟩) (sym q) x∈)

levelData : (a : Limit)
          → Σ[ n ∈ ℕ ] IsLeast natOrder (λ m → a .fst ∈ˢ finiteStage m) n
```

`levelData` が、截断された存在と最小要素の定理が出会う箇所である。述語 `m ↦ a .fst ∈ˢ finiteStage m` と截断された証人 `inSome` に対し、自然数順序についての `leastOf` と排中律を適用すると、明示的な数項と `IsLeast` のデータが返る。その数項の段階は集合を含み、より小さい数項ではその性質は成り立たない。したがってレベルは最小の出現段階であり、截断から任意に選ばれた段階ではない。

```agda
levelData a =
  leastOf natOrder lem (λ m → a .fst ∈ˢ finiteStage m) (inSome (a .fst) (a .snd))

level : Limit → ℕ
level a = levelData a .fst

level-in : (a : Limit) → ⟨ a .fst ∈ˢ finiteStage (level a) ⟩
```

二つの射影には扱いやすい名が付いている。`level a` は根底の集合が現れる最小の数項であり、`level-in a` はその段階での所属の証明書である。要素の「階」について整列順序が必要とするものはすべてデータとして手に入り、次の節はまさにこの二つの材料から順序を組み立てる。

```agda
level-in a = levelData a .snd .fst
```

極限上の順序はレベルを第一の鍵として比較する：レベルの低い要素が先に来て、同じレベルの二つの要素はそのレベル自身の順序で比較される。第二の選択肢はレベルの等しさを保持するが、その向きのおかげで第二の要素を第一の要素のレベルで読み取ることができ、定義に余計な輸送が現れない。

非反射性と推移性はこの選択肢についての場合分けであり、レベルの等式を使って段階順序の事実を必要なレベルへ移す。三分法はまずレベルを比較し、一致する場合にのみ段階の順序に委ねる。

関係 `a ≺ b` は、先に来る二つの仕方の非交和です。左の選択肢は `a` のレベルが厳密に小さいと言い、右の選択肢はレベルが一致し、段階 `level a` の中で基底の集合がその段階自身の `before` 順序に入ると言います。左辺の `Lift` は自然数上の比較を `Type ℓ-zero` から、右の選択肢が既に住む宇宙 `Type (ℓ-suc ℓ)` へ引き上げ、両者の枝が一つの型を共有するようにします。この関係は辞書式に読みます：レベルが決め手となり、同点のときにだけ段階に問い合わせます。

```agda
_≺_ : Limit → Limit → Type (ℓ-suc ℓ)
a ≺ b = Lift {ℓ-zero} {ℓ-suc ℓ} (level a < level b)
      ⊎ ((level b ≡ level a) × ⟨ before (level a) (a .fst) (b .fst) ⟩)

limit-irrefl : (a : Limit) → a ≺ a → Empty.⊥
limit-irrefl a (inl h)       = ¬m<m (lower h)
```

非反射性は、各枝について対応する成分の事実で処理されます：厳密な不等式 `level a < level a` は `¬m<m` が拒み、`a` 自身に対する `before (level a)` の証人は `before-irrefl` が拒みます。後者は全段階で帰納なしに成り立っていました。推移性は、二つの前提がそれぞれどちらの枝を使うかで場合分けします。両段階ともレベルで下降するなら `<-trans` が二つの不等式を合成し、片方だけが下降するなら、もう一方の前提にあるレベルの等式を `subst` とともに用いて厳密な不等式を正しい端点へ移し、やはり左の枝を得ます。

```agda
limit-irrefl a (inr (_ , h)) = before-irrefl (level a) (a .fst) h

limit-trans : (a b c : Limit) → a ≺ b → b ≺ c → a ≺ c
limit-trans a b c (inl h)       (inl k)       = inl (lift (<-trans (lower h) (lower k)))
limit-trans a b c (inl h)       (inr (q , _)) =
  inl (lift (subst (λ j → level a < j) (sym q) (lower h)))
```

二つの仮定がともに同レベルの分岐にあるとき、`a ≺ b` から `q : level b ≡ level a`、`b ≺ c` から `p : level c ≡ level b` を得る。合成 `p ∙ q : level c ≡ level a` が `a ≺ c` に必要な等式である。段階順序の事実 `hbc` は `level b` で述べられているので、`q` に沿って `level a` へ輸送し、そこで `StageOrder.trans` により `hab` と合成する。

```agda
limit-trans a b c (inr (q , _)) (inl k)       =
  inl (lift (subst (λ j → j < level c) q (lower k)))
limit-trans a b c (inr (q , hab)) (inr (p , hbc)) = inr (p ∙ q , joined)
  where
  moved : ⟨ before (level a) (b .fst) (c .fst) ⟩
```

`moved` の輸送は等式 `q` に沿って `hbc` を移し、`before` の主張がなされる段階を `level b` から `level a` へ変えるだけです。こうして二つの証人は同じ段階に住みます。`hab` はそこで `a` の集合が `b` の集合に先行し、`moved` は `b` の集合が `c` の集合に先行すると言うので、段階 `level a` での `StageOrder.trans` が両者を `joined` へとつなぎ、`a` が自レベル内で `c` に先行する証人となります。これで推移性は完成です。続く三分法は、二つのレベルを直接比較して判定します。

```agda
  moved = subst (λ j → ⟨ before j (b .fst) (c .fst) ⟩) q hbc
  joined : ⟨ before (level a) (a .fst) (c .fst) ⟩
  joined = StageOrder.trans (stageOrder (level a)) (a .fst) (b .fst) (c .fst) hab moved

limit-tri : (a b : Limit) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
limit-tri a b = byLevel (level a ≟ level b)
```

三岐性ではまず `level a ≟ level b` を判定する。レベルが異なれば、対応する狭義比較の分岐が直ちに得られる。等しい場合には `p : level a ≡ level b` が得られ、`level-in b` を `sym p` に沿って輸送すると `b` が `finiteStage (level a)` に入る。そこで `StageOrder.tri` が一つの段階内で二つの基底集合を比較できる。

```agda
  where
  byLevel : NatOrder.Trichotomy (level a) (level b) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
  byLevel (NatOrder.lt h) = lt (inl (lift h))
  byLevel (NatOrder.gt h) = gt (inl (lift h))
  byLevel (NatOrder.eq p) = same
```

局所的な三岐性を、極限関係が要求する等式の向きで包み直す。局所結果が `a before b` なら、`a ≺ b` の同レベル分岐に `sym p : level b ≡ level a` を返す。`b before a` なら、`b ≺ a` の同レベル分岐に `p` を返し、before の証明を段階 `level b` へ輸送する。基底集合の等式は、所属証明の成分が命題なので `Limit` の等式へ持ち上がる。

```agda
    (StageOrder.tri (stageOrder (level a)) (a .fst) (b .fst) (level-in a) b∈)
    where
    b∈ : ⟨ b .fst ∈ˢ finiteStage (level a) ⟩
    b∈ = subst (λ j → ⟨ b .fst ∈ˢ finiteStage j ⟩) (sym p) (level-in b)
    same : Tri ⟨ before (level a) (a .fst) (b .fst) ⟩ (a .fst ≡ b .fst)
```

組み替えは段階の判定によって三通りに分かれます。`a` の集合が `b` の集合に先行するなら、結果は `≺` の右の枝で、等式は定義が要求する向きどおりに `sym p` で供給されます。二つの集合が等しいなら、`Σ≡Prop` がそれを対 `a` と `b` の間の経路に引き上げます。`Limit` の第二成分が命題であるためこれが正当化され、これが `eq` の場合です。`b` の集合が `a` の集合に先行するなら、その `before` の事実を `p` に沿って述べられるべきレベルへ輸送し、結果は引数を入れ替えた右の枝となります。どの場合も、すでに組み上げた材料以外のものは何も要りませんでした。

```agda
               ⟨ before (level a) (b .fst) (a .fst) ⟩
         → Tri (a ≺ b) (a ≡ b) (b ≺ a)
    same (lt h) = lt (inr (sym p , h))
    same (eq q) = eq (Σ≡Prop (λ z → snd (z ∈ˢ Lset ω)) q)
    same (gt h) = gt (inr (p , subst (λ j → ⟨ before j (b .fst) (a .fst) ⟩) p h))
```

整礎性の証明は二重の入れ子になった帰納であり、意図的に二つを分けています。外側はレベルについての帰納で、ライブラリの既成の形を用い、より低いすべてのレベルを網羅する帰納仮定を手渡します。内側は、有限段階がすでに持つ accessibility に沿う通常の下降であり、その正当性はまさにその段階の有限性に由来します。レベルをまたぐ下降の一歩は外側の仮定に訴え、レベル内の一歩は内側に訴えます。内側の関数は自分自身の accessibility の実引数以外には再帰しないため、二つを比べる必要は一度も生じません。

レベル `k` の目標 `b` と、同じ基底集合をもつ段階 `k` の点 `u` を固定する。内側の議論は、局所関係 `Below k` に関する `u` の到達可能性を、極限関係に関する `b` の到達可能性へ移す。`Acc` を一段展開すると、任意の前駆を `c` とする。`c` のレベルが低ければ外側の帰納仮定を使い、同じレベルなら `u` の局所前駆にして内側の到達可能性を使う。

```agda
accInside : (k : ℕ)
          → ((m : ℕ) → m < k → (b : Limit) → level b ≡ m → Acc _≺_ b)
          → (u : Point k) → Acc (Below k) u
          → (b : Limit) → level b ≡ k → b .fst ≡ u .fst → Acc _≺_ b
accInside k ih u (acc ru) b q e = acc step
```

`step` の遂行は、前提 `c ≺ b` が取る枝で場合分けします。左の枝では `c` のレベルは `b` より厳密に小さく、したがって `k` よりも小さい。この不等式を `subst` で等式 `q` の下に動かし、レベル `level c` で `ih` を適用します。これがレベルをまたぐ場合です。右の枝では `c` は `b` とレベルを共有するので、両者は段階 `k` の内側に住み、下降は内側の accessibility に引き渡されます。`ru` は `u` の accessibility の `acc` 構成子が供給する関数で、`c` に対応する点 `pc` と、`pc` が `u` より下であることの証明に適用されます。

```agda
  where
  step : (c : Limit) → c ≺ b → Acc _≺_ c
  step c (inl h) = ih (level c) (subst (λ j → level c < j) q (lower h)) c refl
  step c (inr (qb , hc)) = accInside k ih pc (ru pc below) c qc refl
    where
```

右の枝の簿記は明示的に書き出す必要があります。まず `qc` は二つのレベルの等式 `sym qb` と `q` を合成し、`level c ≡ k` を証明します。`c` を段階 `k` で見られるようにするのはまさにこの等式です。次に `pc` は `c` の基底集合と、段階 `k` での所属を一つにまとめます。所属は `level-in c` を `qc` に沿って輸送して得ます。`Point k` とは集合にこうした証書を添えたものなので、この一つの構成が議論を極限から、内側の順序の住む有限段階へと引き戻します。

```agda
    qc : level c ≡ k
    qc = sym qb ∙ q
    pc : Point k
    pc = c .fst , subst (λ j → ⟨ c .fst ∈ˢ finiteStage j ⟩) qc (level-in c)
    below : Below k pc u
```

レベルが等しい場合、`u` の各極限前駆 `b` は同じ有限段階 `k` に属し、その段階の順序で `u` より小さい。この場合に伴う等式は両端点を固定した `k` にそろえるだけであり、`Below k` に関する `u` の到達可能性が `b` の到達可能性を与える。したがって内側の再帰は一つの有限段階の順序の中だけを下降する。

```agda
    below = subst (λ v → ⟨ before k (c .fst) v ⟩) e
              (subst (λ j → ⟨ before j (c .fst) (b .fst) ⟩) qc hc)

accByLevel : (k : ℕ) → (b : Limit) → level b ≡ k → Acc _≺_ b
accByLevel = WFI.induction <-wellfounded outer
  where
```

外側は自然数のレベルに関する整礎帰納であり、その帰納仮定はレベルが `k` より真に小さい前駆を扱う。内側の到達可能性はレベル `k` にとどまる前駆を扱う。この二場合が辞書式の証明をなし、異なる有限段階の順序どうしの整合性を仮定する必要はない。

```agda
  outer : (k : ℕ) → ((m : ℕ) → m < k → (b : Limit) → level b ≡ m → Acc _≺_ b)
        → (b : Limit) → level b ≡ k → Acc _≺_ b
  outer k ih b q = accInside k ih here
    (Ordered.wellFounded k (stageOrder k) here) b q refl
    where
```

`outer` の本体は目標を内側の補題へ帰着させます。まず `b` に対応する段階 `k` の点 `here` を作ります。その作り方は上の `pc` とまったく同じです。次に `Ordered.wellFounded k (stageOrder k) here` がその点の段階 `k` の順序における accessibility を供給し、`accInside` がそこから引き受けます。残る二つの実引数はレベルの等式 `q` と、`b` の基底集合を `here` のそれと同一視する自反射的な等式です。最後の主張 `limit-wf` は極限のすべての要素が accessible であることを言い、レベルの帰納を `level a` で自明な等式 `refl` とともに具体化して得られます。

```agda
    here : Point k
    here = b .fst , subst (λ j → ⟨ b .fst ∈ˢ finiteStage j ⟩) q (level-in b)

limit-wf : WellFounded _≺_
limit-wf a = accByLevel (level a) a refl

limitOrder : SWO Limit
```

したがって `≺` は `Limit` 上の狭義整列順序である。三岐性・非反射性・推移性を満たし、二段階の帰納が整礎性を証明する。初出レベルが異なる要素はレベルで順序づけ、レベルが等しい要素だけを一つの有限段階の順序で比較する。

```agda
limitOrder = record
  { _<∙_   = _≺_
  ; tri∙   = limit-tri
  ; irr∙   = limit-irrefl
  ; trans∙ = limit-trans
```

したがって `limitOrder` は `Lset ω` の要素上の狭義整列順序である。レベルを第一のキーとし、最小レベルが等しい要素はその有限段階の順序で比較する。その最小要素演算により、極限段階上の単に非空な命題値族から選択できる。

```agda
  ; wf∙    = limit-wf }
```

## まとめ

有限な数え上げは定義可能冪集合を通じて上昇し、各数項段階で整礎な最初の相違の順序を支え、最後に `Lset ω` 上の `limitOrder` を与えます。

`Tally` がこの章の持つ有限性のすべてです：すべての要素を命中させる有限族であり、単射性も決定可能な等しさも要求しません。`PowerStep.powerTally` は、数え上げの上のビットベクトルを列挙し、数え上げられた段階のすべての部分集合が定義可能であることを指摘することで、それを定義可能冪集合へ運びます。`stageOrder` はその一歩を数項に沿って進めるので、すべての有限段階が数え上げを持ちます。

`precedes` は二つの部分集合を最初に相違する点で比較します。非反射性は定義から直接従い、推移性は二つの証人の比較から、三分法は排中律と基底の最小要素とから得られます。整礎性はそもそもこの比較の性質ではありません：それは数え上げから `Search` を通じて来るものであり、無限の基底の上では成立しなくなるでしょう。だからこそ有限性を先に確立しておく必要があったのです。

`limitOrder` は `Lset ω` の要素上の狭義の整列順序であり、レベルを第一の鍵とし、レベルの内側では各有限段階自身の順序を用います。これが選択公理が取る interface です：これがあれば、`leastOf` は極限段階の要素上の任意の inhabited な性質から一つの要素を取り出し、毎回同じものを取り出します。