有限段階上の整列順序

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

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

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

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

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

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

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

{-# 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 の仕組みも取り込み、段階とその内部の有限集合とを結びつけます。

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 に適用でき、自然数の実例が数項を順序づけるものになります。

  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 によりループを排除し、_≟_ で判定可能です。これらは、ある性質を証拠立てる最小の添字を見つけるため、また走査の中で各歩の判定を下すために、まさに必要となる性質です。

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 は整礎な関係を消費する帰納原理を提供します。

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 とその極限 ω が有限段階と極限の添字になる。

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 に属する証拠の型であり、数え上げはこの形を、各項の所属の証明と全要素が表現されるという主張の双方に用いる。

open InfinitySet using ( #_; ω )

open hPropStructure 𝒮ᵥ

有限な数え上げ

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

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

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

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

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 の命題的切断を返す。したがって添字は単に存在するだけで、選ばれた位置は外へ現れない。後では、この切断された証人を目標が命題である場合にだけ除去する。

    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 は再帰がパターン照合できるよう明示されている点にも注意してください。

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 で剥がされた型を復元します。

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 がそのずらしを通して帰納仮定を運びます。逆向きの合成は主張されず、ここでは合が単射であるという主張も一切ありません。

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 が合わさって、すべてのビットベクトルが届くことを示します。

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 が期待する形に正確に一致します。

maskCount : ℕ → ℕ
maskCount zero    = 
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 より小さい添字が半分に分けられ、落ちた半分が先頭ビットを、内側の添字が尾を名指します。この読みは定理ではなく定義であり、ただ計算するだけのものです。

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 への経路とをともに作り出します。基底の場合、空ベクトルは零番の添字から来ます。列挙の中で単なる存在ではなくデータを渡さねばならないのはここだけですが、再帰がベクトルそのものに沿って進むため、それが可能になります。

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 の欄が期待する形です。

     ∙ 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 を報告します。その結果の型は族と長さを依存対としてまとめるため、再帰はマスクに算術を一切用いずに長さを伸ばせます。

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) が記録しているものです。

  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 です。この主張は単なる存在ではなくデータです。実際の証人が作り出され、ビットも等式も明示的に与えられます。

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 がこの簿記を、証人三つ組に対してまさに行います。

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 で成立します。そうでなければ再帰が尾の位置に答え、同じずらしがそのまま当てはまります。

       → Σ[ 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 が必要なのです。

  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 と経路です。どちらの向きも切断を含まないことが、後の所属の議論で選択の両側に実際の証人を渡せる理由です。

  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 の場合は頭が零番の位置で答え、より深い位置は再帰します。

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 となり、項目の等式はそのまま保たれます。二つの仕様を合わせると、選択はマスクが印づけたものより大きくも小さくもないことが分かりますが、位置の対応の二つの仕方が互いに逆であるという主張はありません。

  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 を尋ね、ずらした族に再帰します。

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 が書き出したマスクが与えられた部分集合を再現することを証明できるのです。

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 自体は計算に関係せず、照合されるのは判定だけです。だからこそこの定義は一組の等式であって証明ではありません。

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 ⟩ の成立を忠実に答えることを示します。

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 は、このファイバー要素の二つの射影です。重複を許す有限な数え上げの任意のファイバーから添字を選ぶこととは異なり、そちらのファイバーは命題とは限りません。

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 が構成したものです。

  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 に等しい数え上げの位置が、単に存在するということです。

  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 を回復します。どちらの段階でもデータは截断の中で生み出されるので、単なる存在主張から選ばれた証人が取り出されることはありません。

  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 に到達します。この三つの合成が、証明に表示されたパス列そのものです。

    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 がその埋め込み形の所属を証明します。

      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 に等しい位置です。

    (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 そのものであると述べています。

    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 に属することを示します。

  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 へと輸送します。

      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 として単に列挙します。

                 (λ 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 に強制します。

      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 で張った集合です。残りの欄が記録を完成させます。各項目は定義可能性の証明書を伴い、被覆の条項はこの次に与えられます。

               (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 に等しい添字を単に示せばよいことになります。

    ; 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 の被覆が要求するすべてであり、すべての定義可能部分集合が命中するものの、一意なマスクによるとは限りません。

    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 を満たすことと、より小さい充足者がすべて矛盾を導くことを記録する。

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 を満たす他の項目はありません。右の選択肢では、すべての項目が述語を満たしません。どちらの選択肢も截断された存在ではなく完全なデータを運ぶので、後の構成が実際の要素を返せます。

  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 は尾の結果と頭部の判定を族全体の結果へと統合します。

  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 がその比較の三通りの結果を分析します。

            → (⟨ 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 に渡します。

      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 が扱う。

      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 に渡されます。優位者の証明書はどの枝でも古い証明書から組み立て直されるのです。

      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 に渡されます。

    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 と矛盾します。

    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 に回されます。これで導入部に予告した四つの組み合わせがそろいました。

    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 の組です。

  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 を満たさないと仮定したとき、与えられた截断された証人を反駁せねばなりません。この消去が正当なのは、目標が命題である空の型だからで、証人の截断は何も選ばずにほどけます。

      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 がそれを矛盾に変えます。続く行がまさにこの輸送を行います。

          (λ { (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 は完全に矛盾します。証人が必ず族の中に充足者を引き込むことが示されたからです。

        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 の反駁は、非到達可能という述語が非空であることを示すためだけに用いる。

    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 の截断された組であり、仮定は単に到達不能な要素の集まりが空でないと言っているにすぎません。

        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 が肯定の枝で証明書を返します。

        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 は正当で、仮定された到達可能性の反駁に与えることで矛盾が閉じます。無限下降列が構成されたり排除されたりしたのではなく、議論は完全にこの矛盾によるものです。

          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 には属さず、その下で一致が成り立つ、ということです。所属条項の向きこそが、比較でどちらが勝つかを決めます。

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 を同時に持つ証人が現れ、第二の条項を第一に施せば矛盾です。

  ⟨ 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 の要素がどれも満たさない要素を返します。結論の形に注意してください。呼び出し側が実際の最小要素を必要とするので、截断ではなく明示的なデータです。

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 の截断された証人を返します。したがって証明は、最初の截断を消去し、次に第二の截断を消去することから始まります。どちらの目標も再び截断であり、したがって命題です。

                 × ((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 がその三通りの結果を分析します。

    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 への所属を合成された比較を通して輸送するのです。

      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 に沿って所属を輸送すれば矛盾が得られます。

        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 がこの反駁をまとめます。

      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 へと下ろします。二つの非対称な場合が処理され、等しい場合は反駁されたので、推移性が完成します。

        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 に渡せる。

  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 の反駁を矛盾への除去を正当化する。

    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 における所属同値の二つの包含節である。証明が否定形の命題から所属蕴含を作り出す必要があるのはここだけで、それは実質的に二重否定の除去となる。

    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 をそこへ除去するのは正当である。

      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 で一致する、ということになる。

      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 の所属同値が各点で適用できる。

        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⊆ が同様に扱う。除去の向きに注意。命題値の所属関係への除去であり、これこそ命題的截断が許すことである。

      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 の分岐が閉じる。

      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 順序の下ではそれより下に相違点がない。この明示性こそが、最小の相違点を後に証人として使える理由である。

    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 である。それぞれに名を付けておくことで、以下の対称な二つの分岐が読みやすくなる。両者ともこれらの欄のいくつかを引用するからである。

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

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

      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.⊥ が命題であるため、この截断の除去は許される。

      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 が截断の中で渡す。

        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 の三分法が完成し、段階上の局所順序は整礎性を残して要素上の線順序となる。

        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 の選言肢ごとに関数を一つ適用するものであり、三つの節がその計算規則である。これは、二つの集合について証明された三分法を、段階の二つの点について必要な三分法へ変換するのに使われる。両者は所属の証明を帯びるかどうかだけが違う。

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 である。

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、つまりこの比較を定義した際に前提なしで確立された非反射性である。だからこそ、非反射性は再帰が運ぶべきデータには入らない。

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.⊥ が命題であるため、この截断の除去は正当である。

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 を読む。所属は命題なので、同じ集合を持つ二つの点ははじめから等しい。この一事実が、「集合についての述定」と「点についての述定」との間の行き来のすべての作業を担う。

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 の推移性である。非反射性は最初の相違から一様に従い、局所順序の整礎性は必要なときに数え上げから得られる。

  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 がまさにそれを供給する。第二成分は命題の証明であるから、根底の集合の間のパスは点の間のパスへ延長できる。

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 が集合の等式を点の等式へ引き上げる。被覆は数え上げ自身と同様、截断されたままである。

    (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 })

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

    (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、三つの順序法則は段階内の比較から、整礎性は有限走査から得られる。この構成では局所的な比較と、無限降下を排除する有限性の議論が明確に分かれている。

  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 より真に下にあるものが存在しないこととともに返す。前提を除けば、ここに截断はない。

    ; 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∈ に適用することで作られる。

  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 に渡すものであり、探索機構と最初の相違の順序との環を閉じる。