順序数の添字、Gödel 対順序、有限添字

private module U = SWO u

積の順序 _≺×_ が (a , x) を (b , y) より下に置く道は二つある。整列順序で a が b より真に下にあるか、あるいは第一座標が等しいこと (両方向の狭義比較への反証の組がそれを証明する) と、第二の関係で x が y より下にあることである。これは辞書式の優先順位を直和として述べたものである。整列順序をまず参照し、引き分けのときのみ第二の関係を見る。順序と並んで、証明はそのデータを計画する。accProd は各座標の到達可能性の証明書から対の証明書を組み立てる。

_≺×_ : X × Y → X × Y → Type (ℓ-suc ℓ)
(a , x) ≺× (b , y) =
  (a U.<∙ b) ⊎ (((a U.<∙ b) → ⊥₀) × ((b U.<∙ a) → ⊥₀) × (x <ᵥ y))

private
  accProd : (a : X) → Acc U._<∙_ a → (x : Y) → Acc _<ᵥ_ x → Acc _≺×_ (a , x)

降下は二段階の優先順位に従う。a が整列順序で到達可能であり x が第二の関係で到達可能だとすると、任意の ≺×-先行者 (b , y) は直和の二つの枝のどちらかに落ちる。第一座標が真に下がっていた場合は、b は整列順序における a の先行者なので、その到達可能性の証明書 ru b h が使え、y は自前の証明書 wfv y を提供する。これらの真に小さい二つの証明書への再帰が (b , y) の証明書を組み立てる。

  accProd a (acc ru) = inner
    where
    inner : (x : Y) → Acc _<ᵥ_ x → Acc _≺×_ (a , x)
    inner x (acc rv) = acc λ where
      (b , y) (inl h) → accProd b (ru b h) y (wfv y)

引き分けの場合こそ connex の出番である。第二の枝は両方向の狭義比較が失敗したと主張するので、connex がパス b ≡ a を生み出し、その対はこのパスに沿って第一座標の等しい対へ輸送できる。降下は第二の関係だけの問題に帰着し、そこでは証明書 rv y h が適用される。この二つの節を重ねれば、すべての対が到達可能である。整列順序が各第一座標を到達可能にし、仮定が各第二座標を到達可能にするからである。これが prodWF であり、本章の残りの部分がこの積について消費する唯一の主張である。

      (b , y) (inr (¬ba , ¬ab , h)) →
        subst (λ z → Acc _≺×_ (z , y)) (sym (connex u b a ¬ba ¬ab))
          (inner y (rv y h))

prodWF : WellFounded _≺×_
prodWF (a , x) = accProd a (U.wf∙ a) x (wfv x)

_≺₁_ : ⟪ α ⟫ → ⟪ α ⟫ → Type (ℓ-suc ℓ)
m ≺₁ n = ⟪ α ⟫↪ m ∈ᵗ ⟪ α ⟫↪ n

ord-inord : (m : ⟪ α ⟫) → IsOrd (⟪ α ⟫↪ m)
ord-inord m = mem-ord {A = α} oα (⟪ α ⟫↪ m) (member α m)

添字の三分法は、指名された要素の三分法から来る。古典的な定理 ord-tri は二つの順序数要素を比較し、直和を返す。第一が第二の要素であることの証明、要素の等式のパス、あるいは逆方向の証明である。補助の go はこの三つの場合を対応づける。所属の二つの枝はそのまま lt と gt になる。≺₁ は指名された要素どうしの所属として定義されているからである。

tri₁ : (m n : ⟪ α ⟫) → Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m)
tri₁ m n = go (ord-tri (⟪ α ⟫↪ m) (ord-inord m) (⟪ α ⟫↪ n) (ord-inord n))
  where
  go : (⟨ ⟪ α ⟫↪ m ∈ˢ ⟪ α ⟫↪ n ⟩
        ⊎ ((⟪ α ⟫↪ m ≡ ⟪ α ⟫↪ n) ⊎ ⟨ ⟪ α ⟫↪ n ∈ˢ ⟪ α ⟫↪ m ⟩))

等号の枝だけが、提示を本質的に使う箇所である。順序数の三分法が返すのは指名された要素の等式であるが、目標は添字の等式であり、両者は異なる型である。埋め込みの単射性 ↪-inj が要素のパスを添字の間のパスへと反映する。この枝を処理すれば、tri₁ は ⟪ α ⟫ 上の三場合の比較データ Tri になる。

     → Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m)
  go (inl h)       = lt h
  go (inr (inl p)) = eq (↪-inj {a = α} p)
  go (inr (inr h)) = gt h

irr₁ : (m : ⟪ α ⟫) → (m ≺₁ m → ⊥₀)

非反射性と推移性は、指名された要素から引き継がれる。自分自身に属する集合はないので、m ≺₁ m は自己反証する。推移性については、m ≺₁ n と n ≺₁ k はどちらも ⟪ α ⟫↪ k についての所属の事実であり、ord-inord によりこれは順序数である。IsOrd の証明書の最初の成分は、順序数の要素どうしの所属の推移性を主張するので、二つの事実を直接つなぐ。到達可能性も同じように運ばれる。指名された要素 ⟪ α ⟫↪ m の各要素が所属のもとで到達可能なら、m の各 ≺×-ではなく ≺₁-先行者 n はある要素を指すので、添字 n に対する所属の事実をその証明書に渡せば、acc₁ が ≺₁ のもとでの m の到達可能性を返す。

irr₁ m h = ∈-irrefl (⟪ α ⟫↪ m) h

trans₁ : (m n k : ⟪ α ⟫) → m ≺₁ n → n ≺₁ k → m ≺₁ k
trans₁ m n k h h' = ord-inord k .fst h h'

acc₁ : (m : ⟪ α ⟫) → Acc _∈ᵗ_ (⟪ α ⟫↪ m) → Acc _≺₁_ m
acc₁ m (acc r) = acc (λ n n≺m → acc₁ n (r (⟪ α ⟫↪ n) n≺m))

≺₁ の整礎性まであと一歩である。周囲の階層での正則性が、所属のもとでの到達可能性の証明書をすべての集合に渡すので、指名された要素 ⟪ α ⟫↪ m はそれぞれ到達可能であり、acc₁ がそれを添字 m の到達可能性へと持ち上げる。これが wf₁ であり、有限の節の探索が再利用する整礎性である。そしてレコード ordSWO が関係とその四つの法則をインターフェース SWO にまとめる。狭義整列順序の章の自然数の実例が供給するのと同じ五つのフィールドである。

wf₁ : WellFounded _≺₁_
wf₁ m = acc₁ m (regularityV (⟪ α ⟫↪ m))

ordSWO : SWO ⟪ α ⟫
ordSWO = record
  { _<∙_   = _≺₁_

ordSWO の組み立てこそがこの節の要点である。これは実例であって新しい数学ではない。SWO を入力とする以後の構成はどれも、任意の順序数の添字の上で動くようになり、次の節の対順序が消費するのはまさにこの実例である。ここで ω や有限順序数が特別扱いされることはない。議論に使ったのは α の推移性、埋め込み、古典的な三分法、そして正則性だけである。

  ; tri∙   = tri₁
  ; irr∙   = irr₁
  ; trans∙ = trans₁
  ; wf∙    = wf₁ }

古典的な Gödel の対の考え方は、指字の対に順序を与え、対の上の降下を座標ごとに分析できるようにするものである。ここで使う順序は普通の辞書式順序ではない。まず二つの座標の ≺₁-最大値で階級づけを行うので、座標がどちらも小さい対は、並び方にかかわらず大きい座標をもつ対の下に沈み、最大の階級を共有する対だけが第一座標、次に第二座標で比較される。この節はその順序を定義し、≺₁ の対応する法則から三分法・非反射性・推移性を直接証明する。整礎性には前の節の辞書式積が必要で、次のコードのまとまりで与えられる。

最大値には一つの準備が要る。≺₁ の反射的な伴い手 ≤₁ で、狭義の関係と等式の直和として定義する。三分法データは明示的な三場合のデータなので、二つの添字の最大値は比較を検査して二つの入力のどちらかを返すことで計算され、証明書 max-spec は返された値が真の最大値であることを支える二つの ≤₁ の事実を記録する。

非狭義の伴い手 ≤₁ は、ある添字が別の添字より真には上にない二つの場合を集める。m ≤₁ n が成り立つのは、m ≺₁ n のときか、m が n と等しいときである。これを使って最大値は比較データから定義される。maxGo は m と n の三場合の比較を引数に取り、大きい方を返す。m が真に下のときは n を、残る二つの場合は m を返す。

_≤₁_ : ⟪ α ⟫ → ⟪ α ⟫ → Type (ℓ-suc ℓ)
m ≤₁ n = (m ≺₁ n) ⊎ (m ≡ n)

maxGo : (m n : ⟪ α ⟫) → Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m) → ⟪ α ⟫
maxGo m n (lt _) = n
maxGo m n (eq _) = m

関数 maxOrd は最大値を全域化したものである。まず比較 tri₁ m n を計算し、そのデータに maxGo を適用する。tri₁ が古典的な入力であるため、maxOrd は値がそのデータに依存する定義された関数であり、独立に証明された全域性の主張ではない。仕様 max-spec は、結果を最大値たらしめるものを述べる。各入力が出力に対して ≤₁ であることであり、その証明も同じ場合分けによる。次の where ブロックがそれを実行する。

maxGo m n (gt _) = m

maxOrd : ⟪ α ⟫ → ⟪ α ⟫ → ⟪ α ⟫
maxOrd m n = maxGo m n (tri₁ m n)

max-spec : (m n : ⟪ α ⟫) → (m ≤₁ maxOrd m n) × (n ≤₁ maxOrd m n)
max-spec m n = go (tri₁ m n)

最初の二つの比較の場合は、二つの ≤₁ の事実を直接に証明する。m ≺₁ n なら m ≤₁ n は狭義の枝を、n ≤₁ n は等号の枝を使う。m と n が一致する場合は、パスの対称性が二つ目の等式を与える。

  where
  go : (t : Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m))
     → (m ≤₁ maxGo m n t) × (n ≤₁ maxGo m n t)
  go (lt h) = inl h , inr refl
  go (eq p) = inr refl , inr (sym p)

残る場合は対称である。n ≺₁ m なら、選ばれる最大値は m である。したがって max-spec は、二つの入力がともに反射的な順序 ≤₁ で計算された最大値以下にあることを述べている。

  go (gt h) = inr refl , inl h

型 Pair は添字の平方を集める。要素は α の添字の対 (a , b) である。Pair 上の順序 ≺ は、その三段階の優先順位を入れ子の直和として定義する。第一の枝は階級を比較する。maxOrd a b が maxOrd c d より真に下にあることである。階級が並んだときは、第二の枝が階級の等式を要求したうえで座標を比較する。a が c より真に下にあるか、a が c に等しければ b が d より真に下にあることである。

Pair : Type ℓ
Pair = ⟪ α ⟫ × ⟪ α ⟫

_≺_ : Pair → Pair → Type (ℓ-suc ℓ)
(a , b) ≺ (c , d) =

三分法の証明は、定義の入れ子を外から内へと写す。外側の分析 M-case は tri₁ で二つの階級を比較する。階級が真に順序づけられていれば、対全体がどちらの方向でも第一の枝により真に順序づけられる。引き分けの場合だけが内側の段を必要とし、tri≺ は任意の二つの対について三場合のデータを返す一つの関数として組み立てられる。

  (maxOrd a b ≺₁ maxOrd c d)
    ⊎ ((maxOrd a b ≡ maxOrd c d) × ((a ≺₁ c) ⊎ ((a ≡ c) × (b ≺₁ d))))

tri≺ : (p q : Pair) → Tri (p ≺ q) (p ≡ q) (q ≺ p)
tri≺ (a , b) (c , d) = M-case (tri₁ (maxOrd a b) (maxOrd c d))
  where

最も深い場合 Y-case は、階級と第一座標がともに一致する対を扱い、第二座標を比較する。b と d の狭義比較があれば、対応する方向で対は真に順序づけられ、二つの等式は外の段が本当に並んでいることの証人として一緒に運ばれる。逆方向は対称である。

  Y-case : (e : maxOrd a b ≡ maxOrd c d) (f : a ≡ c)
         → Tri (b ≺₁ d) (b ≡ d) (d ≺₁ b)
         → Tri ((a , b) ≺ (c , d)) ((a , b) ≡ (c , d)) ((c , d) ≺ (a , b))
  Y-case e f (lt h) = lt (inr (e , inr (f , h)))
  Y-case e f (gt h) = gt (inr (sym e , inr (sym f , h)))

第二座標まで一致するときは、二つの対は等しく、対の構成子への cong₂ が二つの座標のパスを対の間のパスに変える。比較データの等号の枝が裸のタグではなく実際のパスを運ぶのはこのためである。一段上では、X-case が第一座標を比較する。狭義の比較がその段で順序を決め、引き分けの場合は b と d の比較を連れて Y-case へ降りる。

  Y-case e f (eq g) = eq (cong₂ _,_ f g)

  X-case : (e : maxOrd a b ≡ maxOrd c d)
         → Tri (a ≺₁ c) (a ≡ c) (c ≺₁ a)
         → Tri ((a , b) ≺ (c , d)) ((a , b) ≡ (c , d)) ((c , d) ≺ (a , b))
  X-case e (lt h) = lt (inr (e , inl h))

最後に最上段である。M-case が階級そのものを比較する。二つの狭義の場合は ≺ の第一の枝をそのまま適用する。M-case のシグネチャは、入力がまさに二つの階級に対する三分法データであることを明示するので、tri≺ の証明全体を、一つ下の段の比較データを消費しながら段ごとに進む一つの三重の場合分けとして読める。

  X-case e (gt h) = gt (inr (sym e , inl h))
  X-case e (eq f) = Y-case e f (tri₁ b d)

  M-case : Tri (maxOrd a b ≺₁ maxOrd c d)
               (maxOrd a b ≡ maxOrd c d)
               (maxOrd c d ≺₁ maxOrd a b)

M-case の三つの場合が分析を閉じる。階級で狭義に、あるいは引き分けから第一座標を経て第二座標へと降りる場合である。tri≺ が手に入れば、順序 ≺ はデータとして三分的であり、これが後の一意性の議論が消費する性質である。

         → Tri ((a , b) ≺ (c , d)) ((a , b) ≡ (c , d)) ((c , d) ≺ (a , b))
  M-case (lt h) = lt (inl h)
  M-case (gt h) = gt (inl h)
  M-case (eq e) = X-case e (tri₁ a c)

irr≺ : (p : Pair) → (p ≺ p → ⊥₀)

対の順序の非反射性は短く済む。それぞれの段がすでに自分の狭義比較の反証の仕方を知っているからである。(a , b) ≺ (a , b) なら、その証明は入れ子の定義の三つの枝のどれかに落ちる。いずれも座標か階級についての狭義の ≺₁ の事実であり、対応する irr₁ が矛盾に導く。階級の場合は maxOrd a b で、第一座標の場合は a で、第二座標の場合は b で irr₁ を使う。

irr≺ (a , b) (inl h)              = irr₁ (maxOrd a b) h
irr≺ (a , b) (inr (e , inl h))    = irr₁ a h
irr≺ (a , b) (inr (e , inr (f , h))) = irr₁ b h

trans≺ : (p q r : Pair) → p ≺ q → q ≺ r → p ≺ r
trans≺ (a , b) (c , d) (e , f) = goM

推移性が本質的な法則で、その証明は三つの階級を軸に組織される。M₁ は (a , b) の階級、M₂ は (c , d) の、M₃ は (e , f) の階級である。補題 goY と goX がまず内側の段を扱う。goY は第二座標に ≺₁ の推移性を適用したにすぎず、後の最も内側の場合の合成の議論になる。

  where
  M₁ = maxOrd a b
  M₂ = maxOrd c d
  M₃ = maxOrd e f

  goY : (b ≺₁ d) → (d ≺₁ f) → (b ≺₁ f)

補題 goX は、二つの狭義のステップの座標レベルでの判定を合成する。両ステップが第一座標で狭義のときは、≺₁ の推移性がそれらを合成する。片方が狭義でもう片方が第一座標の等式のときは、そのパスに沿って狭義の事実が輸送される。a ≺₁ c と c ≡ e から代入により a ≺₁ e が得られるからである。両方とも等式の場合が残り、第二座標の組に委ねられる。

  goY = trans₁ b d f

  goX : ((a ≺₁ c) ⊎ ((a ≡ c) × (b ≺₁ d)))
      → ((c ≺₁ e) ⊎ ((c ≡ e) × (d ≺₁ f)))
      → ((a ≺₁ e) ⊎ ((a ≡ e) × (b ≺₁ f)))
  goX (inl h) (inl h') = inl (trans₁ a c e h h')

残った場合は goX から第二座標の組へ渡され、それらの等式のパスは連結されて、両端の階級が一致することの証人となる。この二つの補題をそろえて、goM のシグネチャは最上段での合成の問題を述べる。M₁ と M₂ の間の狭義のステップか引き分け、および M₂ と M₃ の間の対応する判定から、M₁ と M₃ の間の対応する判定を作ることである。その構造はちょうど一段上の goX の写しである。

  goX (inl h) (inr (e₂ , _)) = inl (subst (λ w → a ≺₁ w) e₂ h)
  goX (inr (e₁ , _)) (inl h') = inl (subst (λ w → w ≺₁ e) (sym e₁) h')
  goX (inr (e₁ , s₁)) (inr (e₂ , s₂)) = inr (e₁ ∙ e₂ , goY s₁ s₂)

  goM : ((M₁ ≺₁ M₂) ⊎ ((M₁ ≡ M₂) × ((a ≺₁ c) ⊎ ((a ≡ c) × (b ≺₁ d)))))
      → ((M₂ ≺₁ M₃) ⊎ ((M₂ ≡ M₃) × ((c ≺₁ e) ⊎ ((c ≡ e) × (d ≺₁ f)))))

goM の 4 つの節は、goX を一段上に移した形をしている。両方のステップが最大値の間で真に狭いなら、≺₁ の推移性で M₁ ≺₁ M₂ と M₂ ≺₁ M₃ を合成する。片方だけが狭く、他方が最大値での一致であるときは、等しいことを示す経路に沿って狭い事実を輸送する。すなわち M₁ ≺₁ M₂ と M₂ ≡ M₃ から置換により M₁ ≺₁ M₃ が出て、一致が先に来る場合は対称に sym e₁ を使う。両方とも最大値での一致のときだけ同じ段に留まり、級の一致を連結した経路 e₁ ∙ e₂ を記録し、第二座標を goX に委ねる。

      → ((M₁ ≺₁ M₃) ⊎ ((M₁ ≡ M₃) × ((a ≺₁ e) ⊎ ((a ≡ e) × (b ≺₁ f)))))
  goM (inl h) (inl h') = inl (trans₁ M₁ M₂ M₃ h h')
  goM (inl h) (inr (e₂ , _)) = inl (subst (λ w → M₁ ≺₁ w) e₂ h)
  goM (inr (e₁ , _)) (inl h') = inl (subst (λ w → w ≺₁ M₃) (sym e₁) h')
  goM (inr (e₁ , s₁)) (inr (e₂ , s₂)) = inr (e₁ ∙ e₂ , goX s₁ s₂)

辞書式積の整礎性を借りるために、各対を三つ組として改めて提示する。f は級である maxOrd a b を対 (a , b) の手前に記録する。この射の単射性はほとんど自明で、三つ組の間の経路を第二成分に格納された対へ射影すればよく、その射影 cong (λ p → p .snd) が対の一致をそのまま回復する。

f : Pair → ⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)
f (a , b) = maxOrd a b , (a , b)

f-inj : {p q : Pair} → f p ≡ f q → p ≡ q
f-inj {a , b} {c , d} e = cong (λ p → p .snd) e

_≺²_ : (⟪ α ⟫ × ⟪ α ⟫) → (⟪ α ⟫ × ⟪ α ⟫) → Type (ℓ-suc ℓ)

ここで順序数順序を外側の成分として、辞書式積を二度具体化する。関係 _≺²_ は添字の対を比較する。まず左座標の ≺₁ で比べ、どちらの向きも成り立たないときに右座標の ≺₁ で比べる。この形に対しては prodWF がちょうど整礎性を与える。もう一段重ねた _≺³_ は f の着地点である級付き三つ組を比較するから、_≺³_ の下での下降は級、第一座標、第二座標という三段の辞書式下降になる。

_≺²_ = PairOrder._≺×_
  where module PairOrder = Lexicographic ordSWO _≺₁_ wf₁

wf² : WellFounded _≺²_
wf² = prodWF ordSWO _≺₁_ wf₁

_≺³_ : (⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)) → (⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)) → Type (ℓ-suc ℓ)
_≺³_ = TripleOrder._≺×_
  where module TripleOrder = Lexicographic ordSWO _≺²_ wf²

wf³ は prodWF の二度目の適用にすぎず、_≺³_ は追加の作業なしに整礎である。補助事実 ¬<₁ は反反射性の小さな帰結を記録する。添字 m と n が等しければ、ステップ m ≺₁ n は存在しえない。そのステップを等式に沿って後ろへ輸送すれば m ≺₁ m が得られるからである。これは積の関係が求めるまさにその準備である。_≺×_ は外側のどちらの向きも成り立たないときに限って次の段へ降りるからだ。これを踏まえると、subrel は対の順序の各ステップ p ≺ q を級付き三つ組の間のステップ f p ≺³ f q へ変換するものとして型が与えられている。

wf³ : WellFounded _≺³_
wf³ = prodWF ordSWO _≺²_ wf²

¬<₁ : (m : ⟪ α ⟫) {n : ⟪ α ⟫} → m ≡ n → (m ≺₁ n → ⊥₀)
¬<₁ m {n} q h = irr₁ m (subst (λ w → m ≺₁ w) (sym q) h)

subrel : {p q : Pair} → p ≺ q → f p ≺³ f q

subrel の最初の二つの場合は直接的である。級がすでに真に順序づけられているなら、ステップ inl h はそれ自体が _≺³_ の最上段のステップである。両関係が外側の成分 ≺₁ を共有するからだ。級が一致し第一座標が真に狭い場合、目標の関係は一段降りる前に級のどちらの向きも成り立たないことの証明を要求する。一致の経路とその対称にそれぞれ ¬<₁ を適用すれば、まさにその二つの反駁が得られ、その後に inl h が第一座標の狭いステップを第二段に置く。

subrel {a , b} {c , d} (inl h) =
  inl h
subrel {a , b} {c , d} (inr (e , inl h)) =
  inr (¬<₁ (maxOrd a b) e , ¬<₁ (maxOrd c d) (sym e) , inl h)
subrel {a , b} {c , d} (inr (e , inr (f , h))) =

完全に一致する場合はさらに一段深く入れ子になる。級が一致し、第一座標も一致し、第二座標が真に狭い。そこで subrel は、h を最内段に置く前に、級の二つの向きと第一座標の二つの向きを反駁しなければならない。対の順序の整礎性は、f に沿って到達可能性を引き戻すことで従う。wf≺ p は f p の _≺³_ における到達可能性から出発するが、それを wf³ が与える。非公開の補助関数 go は、到達可能性の証明の添字がその証明が対象とする対を定めるように述べられており、下の再帰が自分自身に再び入れるようになっている。

  inr (¬<₁ (maxOrd a b) e , ¬<₁ (maxOrd c d) (sym e)
     , inr (¬<₁ a f , ¬<₁ c (sym f) , h))

wf≺ : WellFounded _≺_
wf≺ p = go (wf³ (f p))
  where

go の計算規則は到達可能性のデータを展開する。acc r から出発する。ここで r は f q の各 _≺³_ 前駆を到達可能性へ写す。これにより対の側で acc が作られる。q' ≺ q を満たす前駆 q' が与えられると、ステップは subrel によって f q' ≺³ f q へと押し出され、r に渡され、そこへ再び go が適用される。したがって対の任意の降下列は級付き三つ組の降下列へ写されるが、_≺³_ の整礎性は後者を禁じるから、対の順序に無限降下はない。

  go : {q : Pair} → Acc _≺³_ (f q) → Acc _≺_ q
  go {q} (acc r) = acc (λ q' q'≺q → go (r (f q') (subrel {q'} {q} q'≺q)))

P : (n : ℕ) (m : ⟪ # n ⟫) → ℕ → hProp (ℓ-suc ℓ)
P n m k = ((k < n) × (⟪ # n ⟫↪ m ≡ # k))
        , isProp× isProp≤ (isSetS (⟪ # n ⟫↪ m) (# k))

ω-mem→numeral : (β : S) → ⟨ β ∈ˢ ω ⟩ → ∥ Σ[ n ∶ ℕ ] (β ≡ # n) ∥₁

β が ω に属することそのものは、β が数項であることを切り捨てられた形でしか言わない。ω の仕様は、持ち上げられた自然数と近似の証明書の切り捨てられた対を与える。補助関数 hit はこのデータを経路へと精製し、近似 β ≈ˢ numeralV n と numeralV≡# n の合成から β ≡ # n を得る。結果は ∥_∥₁ の中に留まるので、この定理が与えるのは数項ラベルの単なる存在であり、選ばれたラベルではない。証人を得るには切り捨てを非命題的な対象へ消去する必要がある。

ω-mem→numeral β β∈ω = map₁ hit (subst ⟨_⟩ (ω-specV β) β∈ω)
  where
  hit : Σ[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] ⟨ β ≈ˢ numeralV (lower n) ⟩
      → Σ[ n ∶ ℕ ] (β ≡ # n)
  hit (n , p) = lower n , p ∙ numeralV≡# (lower n)

有限順序数 # n の添字には具体的な出発点がある。表された要素が ⟪ # n ⟫ に属するという事実は、∈#-elim を通じて、k < n なる k が P を満たすことを含意する。ここで作るのは小さな表示と Fin n の外的な同一視なので、この切り捨てられた証人を HostLeast.leastOf natOrder lem に渡すことは、意図的にホスト専用探索を使うことである。単なる存在は選ばれた最小の対 s に変わる。その第一成分がラベル k であり、証明書の第一成分が上界 k < n で、これこそ Fin n がまとめたデータである。

toFin : (n : ℕ) → ⟪ # n ⟫ → FB.Fin n
toFin n m = k , k<n
  where
  s = HostLeast.leastOf natOrder lem (P n m)
    (∈#-elim n (⟪ # n ⟫↪ m) (member (# n) m))
  k : ℕ

toFin の仕様は型の上界よりも多くを言う。最小ラベル k は P の第二の連言支、すなわち添字 m が # k を表すという部分を満たすのである。これは最小要素の探索が返す証明書の第二成分であり、下の単射性の証明が消費する経路そのものである。

  k = s .fst
  k<n : k < n
  k<n = ((s .snd) .fst) .fst

toFin-spec : (n : ℕ) (m : ⟪ # n ⟫) → ⟪ # n ⟫↪ m ≡ # ((toFin n m) .fst)
toFin-spec n m = ((s .snd) .fst) .snd

toFin の単射性は、ラベルの一致という仮定に沿って二つの仕様の経路を輸送することで従う。toFin n m₁ と toFin n m₂ が一致すればその第一成分は一致し、したがって # ((toFin n m₁) .fst) と # ((toFin n m₂) .fst) の間に経路がある。二つの仕様と連結すれば表された要素の間の経路が得られ、↪-inj が順序数の順序のときと同様に、表された要素の一致を添字の一致へと反映する。

  where
  s = HostLeast.leastOf natOrder lem (P n m)
    (∈#-elim n (⟪ # n ⟫↪ m) (member (# n) m))

toFin-inj : (n : ℕ) (m₁ m₂ : ⟪ # n ⟫) → toFin n m₁ ≡ toFin n m₂ → m₁ ≡ m₂
toFin-inj n m₁ m₂ e = ↪-inj {a = # n}
  (toFin-spec n m₁ ∙ cong (λ k → # k) (cong (λ p → p .fst) e) ∙ sym (toFin-spec n m₂))

逆方向は #mono から始まる。k < n ならば # k が # n の要素であることを #mono が証明する。添字型 ⟪ # n ⟫ は # n の要素を提示するので、この所属には繊維が付随する。すなわち、表された要素が # k である添字と、fromFin-spec が記録するのとまったく同じ形の証明書である。したがって fromFin n (k , k<n) はこの繊維の第一成分であり、最小探索ではなく提示の仕方によって選ばれる。

fromFin : (n : ℕ) → FB.Fin n → ⟪ # n ⟫
fromFin n (k , k<n) = fiber (# n) (#mono k n k<n) .fst

fromFin-spec : (n : ℕ) (i : FB.Fin n) → ⟪ # n ⟫↪ (fromFin n i) ≡ # (i .fst)
fromFin-spec n (k , k<n) = fiber (# n) (#mono k n k<n) .snd

fromFin-inj : (n : ℕ) (i₁ i₂ : FB.Fin n) → fromFin n i₁ ≡ fromFin n i₂ → i₁ ≡ i₂

fromFin の単射性は、Fin n が部分型であることを用いる。その第二成分は有界な自然数、つまり命題値の族なので、対の一致は第一成分の一致に帰着する。二つの仕様と e から得た、表された要素の間の経路は #-inj′ によって自然数の間の経路に変換され、Σ≡Prop がそれを Fin n の経路へ持ち上げる。続いてこの節は factor を導入する。これは標準的な同値 factorEquiv : Fin n × Fin n ≃ Fin (n · n) の順方向であり、位置の対を一つの位置で数え上げる。

fromFin-inj n i₁ i₂ e = Σ≡Prop (λ _ → isProp≤)
  (#-inj′ (sym (fromFin-spec n i₁) ∙ cong (⟪ # n ⟫↪) e ∙ fromFin-spec n i₂))

factor : (n : ℕ) → FB.Fin n × FB.Fin n → FB.Fin (n · n)
factor n = equivFun (factorEquiv {n = n} {m = n})

factor-inj : (n : ℕ) (x y : FB.Fin n × FB.Fin n)

factor は単なる関数ではなく同値であるため、その単射性に新しい場合分けは不要である。factor n x と factor n y が一致すれば、両側に逆写像を適用し往復則 retEq を使えば、x と y そのものに戻る。証明は sym (retEq ...) x、輸送された等式、retEq ... y の連結である。これは先に指摘したパターン、つまり逆の形をした写像は往復則が供給されるまでは逆ではない、ということの実例で、ここではライブラリの同値が往復則を供給する。

           → factor n x ≡ factor n y → x ≡ y
factor-inj n x y e =
  sym (retEq (factorEquiv {n = n} {m = n}) x)
    ∙ cong (invEq (factorEquiv {n = n} {m = n})) e
    ∙ retEq (factorEquiv {n = n} {m = n}) y

鳩の巣の命題は、後の矛盾の有限の中核である。関数 Fin (suc n) → Fin n は単射になりえない。ライブラリの結果 pigeonhole を反射性の証明 ≤-refl {m = suc n} とともに f に適用すると、相異なるのに f i ≡ f j を満たす二つの位置 i と j とその証明書が得られ、単射性の仮定をその等式と合成すれば空の型の要素が得られる。

no-inj-Fin : (n : ℕ) → (f : FB.Fin (suc n) → FB.Fin n)
           → ((x y : FB.Fin (suc n)) → f x ≡ f y → x ≡ y) → ⊥₀
no-inj-Fin n f finj = i#j (finj i j feq)
  where
  i = (pigeonhole (≤-refl {m = suc n}) f) .fst

この展開は、鳩の巣の証明書を最終行で必要な部分に分ける。i と j は衝突する二つの位置、i#j はその相異性、feq は像の一致である。計算 i#j (finj i j feq) は単射性の仮定から i ≡ j を得て、それを相異性に渡して矛盾を生み出す。

  j = ((pigeonhole (≤-refl {m = suc n}) f) .snd) .fst
  prf = ((pigeonhole (≤-refl {m = suc n}) f) .snd) .snd
  i#j = prf .fst
  feq : f i ≡ f j
  feq = prf .snd

最後のブロックは ω から抽象化する。これは族 E : ℕ → Type ℓ でパラメータ化され、単射な符号器 toFinE : E n → Fin n と単射な復号器 fromFinE : Fin n → E n を伴う。何が仮定され、何が仮定されないかに注意してほしい。各方向はそれぞれ自身の単射性の証明を伴うが、両者が互いに逆であることは要求されず、E n と Fin n の間の同値も主張されない。議論に入るのはこの二つの単射性だけである。

module AbstractChase (E : ℕ → Type ℓ)
                     (toFinE : (n : ℕ) → E n → FB.Fin n)
                     (toFinE-inj : (n : ℕ) (m₁ m₂ : E n) → toFinE n m₁ ≡ toFinE n m₂ → m₁ ≡ m₂)
                     (fromFinE : (n : ℕ) → FB.Fin n → E n)
                     (fromFinE-inj : (n : ℕ) (i₁ i₂ : FB.Fin n) → fromFinE n i₁ ≡ fromFinE n i₂ → i₁ ≡ i₂) where

module NoInj (A : Type ℓ) (into : (m : ℕ) → E m → A)
             (into-inj : (m : ℕ) (i₁ i₂ : E m) → into m i₁ ≡ into m i₂ → i₁ ≡ i₂) where

  no-inj : (n : ℕ) → (f : A → E n × E n)
         → ((x y : A) → f x ≡ f y → x ≡ y) → ⊥₀
  no-inj n f finj = no-inj-Fin (n · n) g g-inj

    where
    g : FB.Fin (suc (n · n)) → FB.Fin (n · n)
    g i = factor n ( toFinE n ((f (into (suc (n · n)) (fromFinE (suc (n · n)) i))) .fst)
                   , toFinE n ((f (into (suc (n · n)) (fromFinE (suc (n · n)) i))) .snd))
    g-inj : (x y : FB.Fin (suc (n · n))) → g x ≡ g y → x ≡ y

    g-inj x y e = fromFinE-inj (suc (n · n)) x y
      (into-inj (suc (n · n))
        (fromFinE (suc (n · n)) x) (fromFinE (suc (n · n)) y)
        (finj Xx Xy pair-eq))
      where

      Xx : A
      Xx = into (suc (n · n)) (fromFinE (suc (n · n)) x)
      Xy : A
      Xy = into (suc (n · n)) (fromFinE (suc (n · n)) y)
      p-eq : (toFinE n ((f Xx) .fst) , toFinE n ((f Xx) .snd))

           ≡ (toFinE n ((f Xy) .fst) , toFinE n ((f Xy) .snd))
      p-eq = factor-inj n
               (toFinE n ((f Xx) .fst) , toFinE n ((f Xx) .snd))
               (toFinE n ((f Xy) .fst) , toFinE n ((f Xy) .snd)) e
      fst-eq : toFinE n ((f Xx) .fst) ≡ toFinE n ((f Xy) .fst)

      fst-eq = cong (λ p → p .fst) p-eq
      snd-eq : toFinE n ((f Xx) .snd) ≡ toFinE n ((f Xy) .snd)
      snd-eq = cong (λ p → p .snd) p-eq
      fst-eq′ : (f Xx) .fst ≡ (f Xy) .fst
      fst-eq′ = toFinE-inj n ((f Xx) .fst) ((f Xy) .fst) fst-eq

      snd-eq′ : (f Xx) .snd ≡ (f Xy) .snd
      snd-eq′ = toFinE-inj n ((f Xx) .snd) ((f Xy) .snd) snd-eq
      pair-eq : f Xx ≡ f Xy
      pair-eq = ΣPathP (fst-eq′ , snd-eq′)