---
title: "順序数の添字、Gödel 対順序、有限添字"
module: L.Ordinal.SquareLaw
lang: ja
site: "Bedrock"
description: "順序数の添字、Gödel 対順序、有限添字"
stage: "順序数，単射，基数"
reading_order: 87
canonical: https://bedrock.institute/ja/L.Ordinal.SquareLaw.html
html: L.Ordinal.SquareLaw.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Ordinal/SquareLaw.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Model, V.Presentation, L.Constructible, L.Ordinal, V.Coding, L.Ordinal.Linear, L.WellOrder.Base]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.Ordinal.SquareLaw.md, https://bedrock.institute/zh/L.Ordinal.SquareLaw.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 順序数の添字、Gödel 対順序、有限添字

本章では後の計数に使う三つの具体的な道具を与える。順序数の添字上の所属整列順序、添字の対上の Gödel 順序、有限順序数の要素と `Fin` の対応である。

第一の構成は、添字が指す順序数要素どうしの所属によって二つの添字を比較し、順序数の三分性と正則性によってその比較を添字型上の狭義整列順序にします。第二の構成は、その順序での座標の最大値によって添字の対を階級づけし、最大値を共有する対は辞書式に並べます。三分性・非反射性・推移性は直接に証明され、整礎性は降下を辞書式積の二段階に入れ子にすることで得られます。第三の構成は、無限順序数 ω の各要素を数項として読み、有限順序数 # n の添字と `Fin n` の間を双方向に変換します。次に、正確な不可能性を有限鳩の巣原理へ帰着します。任意の大きさの有限型の単射像を含む型は、ある固定された有限型の平方へ単射できません。

本章は固定された宇宙レベル ℓ で働き、一つの古典的仮定をモジュールパラメータとして取ります。それはレベル ℓ-suc ℓ のすべての命題に対する判定です。後に確立される比較にはこれが必要です。順序数の三分法も最小要素の探索も、単なる存在の問いを排中律で決着させるからです。この仮定を明示的なパラメータとして残すことで、各構成がどの古典的入力を消費するかが正確に記録されます。

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

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

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

数学的な舞台は累積階層 V です。そこでは集合が型 S をなし、所属は「ある添字の存在」という切り詰められた言明として表されます。各集合 a には選ばれた小さな提示が伴います。添字型 ⟪ a ⟫ と埋め込み ⟪ a ⟫↪ であり、その像こそが a です。したがって a の要素について論じることは添字について論じることになり、埋め込みの単射性が同じ要素を指す添字を同一視します。以下の構成は、IsOrd α の証明書をもつ任意の順序数 α を扱います。これは von Neumann の意味で、推移的であり、その要素もすべて推移的である集合のことです。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import V.Model {ℓ} using ( ω-specV; numeralV; numeralV≡# )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import L.Constructible {ℓ} using ( IsOrd )
```

狭義整列順序は、一つの関係について四つの性質をまとめます。任意の二点が三分法で比較でき、どの点も自分自身より真に小さくなく、狭義比較が推移的で、すべての降下が整礎です。自然数がその基本例です。leastOf はこの構造と排中律を使い、単に要素が存在する命題値族から最小の証人を選びます。後では、順序数の三分法が順序数の要素に同じ三方向の比較を与えます。

```agda
open import L.Ordinal {ℓ} using ( mem-ord; ∈#-elim )
open import V.Coding {ℓ} using ( #-inj′; #mono )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( SWO; Tri; lt; eq; gt; leastOf; natOrder; module SWO )
```

論理の語彙は、証明すべき言明の形に合わせて選ばれています。反証は空型への関数であり、所属の証明は切り詰められた命題の住人であり、三路の比較はその場合の直和で、inl と inr で印づけられます。対やレコードの間のパスは標準補題 Σ≡Prop と ΣPathP で扱います。関係する成分の型が命題であるとき、成分のパスから依存対へのパスを組み立てるものです。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Sigma using ( Σ≡Prop; ΣPathP )
```

有限計数の部分には算術と標準的な有限型が必要です。自然数の乗法 _·_ は有限型の平方の大きさを定め、ライブラリの等価 factorEquiv は `Fin n × Fin n` を `Fin (n · n)` と同一視します。鳩の巣定理は、本章の最後の議論の要となる不可能性を供給します。`Fin (suc n)` から `Fin n` への単射は存在しない、というものです。自然数上の順序には「≤ が命題である」という事実が伴い、これにより `Fin` への比較がその上限の証明非依存性と調和します。

```agda
open import Cubical.Data.Nat using ( _·_ )
import Cubical.Data.Fin.Base as FB
open import Cubical.Data.Fin.Properties using ( factorEquiv; pigeonhole )
open import Cubical.Data.Nat.Order using ( _<_; isProp≤; ≤-refl )
open import Cubical.Foundations.Equiv using ( equivFun; invEq; retEq )
```

各集合 a について、提示写像 ⟪ a ⟫↪ は添字を、それが指す要素へ送ります。したがって # k 上の繊維は、まさにその数項を指す添字からなります。k < n なら数項の単調性により # k は # n の中に入り、対応する繊維の点を選ぶことで Fin n から有限順序数の添字型への変換が定まります。逆向きには最小要素の探索を使います。任意の添字には数項のラベルが初めから付いていないからです。

```agda
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
```

整礎性は到達可能性の述語によって運ばれます。x のすべての R-先行者が再び到達可能なとき Acc R x が成り立ち、acc がこのデータを包み、WellFounded R はすべての要素の到達可能性を要求します。本章の降下の議論は、この到達可能性の証明書を下へ下へと受け渡してゆきます。最後に、レベル `ℓ-suc ℓ` の `hProp` 上の直接の演算を利用し、命題上の連言などの論理演算を、順序数の節で使う構造の仕組みから利用できるようにします。

```agda
open InfinitySet using ( #_; ω )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )

open hPropStructure 𝒮ᵥ
```

本章の後半では、Gödel 対順序の整礎性を、その降下を入れ子になった辞書式降下に埋め込むことで得ます。そのために必要な材料は一般的な構成です。X 上の狭義整列順序と Y 上の任意の整礎な関係が与えられれば、積 X × Y には自然な狭義順序が伴い、その順序は整礎です。この節はまさにそれだけを組み立てます。

二つの小さな点がこの構成を形づくります。第一に、積の順序はまず整列順序で第一座標を比較し、両方向の狭義比較がともに成り立たないとき、すなわち第一座標が等しいときにのみ第二の関係を参照します。二つの失敗した比較から等式を復元するのが、connex (連結性) の補題の働きです。第二に、証明は第一座標と第二座標のそれぞれに対する到達可能性の証明書を同時に運び、この順序の二段階の優先順位に対応します。

狭義整列順序は任意の二要素を三分します。比較データ Tri は「a が b より下」の証明、パス a ≡ b、あるいは「b が a より下」の証明のいずれかを返します。したがって両方向の狭義比較がともに反証されていれば、残るのは中間の場合だけであり、それがまさに求める等式を運んでいます。この connex の補題はその場合分けをまとめたもので、新しい順序の法則ではなく、二つの反証のもとでの三分法データの読み方です。

```agda
connex : {ℓc : Level} {A : Type ℓc} (w : SWO A) (a b : A)
       → (SWO._<∙_ w a b → Empty.⊥) → (SWO._<∙_ w b a → Empty.⊥) → a ≡ b
connex w a b ¬ab ¬ba with SWO.tri∙ w a b
... | lt h = Empty.rec (¬ab h)
... | eq p = p
```

積は一般的に設定されます。第一因子には X 上の狭義整列順序 u が伴い、その関係・三分法・整礎性が使えます。第二因子には Y 上の任意の整礎な関係 _<ᵥ_ が伴います。三分割法や推移性は要求されません。積がこの関係に求めるのは降下だけだからです。両方の関係はレベル ℓ-suc ℓ で値をとります。これは後の順序数の比較が住むレベルです。

```agda
... | gt h = Empty.rec (¬ba h)

module _ {ℓx ℓy : Level} {X : Type ℓx} {Y : Type ℓy} (u : SWO X)
         (_<ᵥ_ : Y → Y → Type (ℓ-suc ℓ)) (wfv : WellFounded _<ᵥ_) where

  private
    module U = SWO u
```

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

```agda
  _≺×_ : X × Y → X × Y → Type (ℓ-suc ℓ)
  (a , x) ≺× (b , y) =
    (a U.<∙ b) ⊎ (((a U.<∙ b) → Empty.⊥) × ((b U.<∙ a) → Empty.⊥) × (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) の証明書を組み立てます。

```agda
    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 であり、本章の残りの部分がこの積について消費する唯一の主張です。

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

## 順序数の添字上の所属順序

順序数 α は推移的であり、その要素もすべて推移的で、要素は所属によって線形に順序づけられます。古典的な入力 `ord-tri` がこの順序を三分的にします。しかし後の章の計数の議論に必要なのは、要素そのもの上の順序ではなく、α の固定された提示の添字上の順序です。小さな型 ⟪ α ⟫ と、その像が α である埋め込み ⟪ α ⟫↪ です。この節は所属順序を要素から添字へと運びます。

二つの区別がこの移し替えを忠実にします。第一に、添字 m それ自体は階層の集合ではありません。それが指す要素は ⟪ α ⟫↪ m であり、比較はすべてこの指名された要素のレベルで行われ、埋め込みの単射性が要素の等式から添字の等式を復元します。第二に、指名された各要素もまた順序数です。これは α の推移性からの帰結であり、各添字で推移性と古典的な三分法を使うことを許すものです。結果として得られるのは ⟪ α ⟫ 上の狭義整列順序 ordSWO で、次の節の Gödel 対順序が階級づけの基礎とする実例です。

添字上の関係 ≺₁ は、指名された要素どうしの所属によって定義されます。m ≺₁ n が成り立つのは、構造の所属命題において ⟪ α ⟫↪ m が ⟪ α ⟫↪ n の要素であるとき、そのときに限ります。この節の残りはすべてこの定義を読みます。最初の支えとなる事実は、指名された各要素もまた順序数であることです。α が推移的で添字 m が α の要素を指すので、所属の証明 member α m に証明書 mem-ord を適用すれば、指名された要素の IsOrd が得られます。この証明書 ord-inord はこの後さらに三回使われます。

```agda
module _ (α : S) (oα : IsOrd α) where

  _≺₁_ : ⟪ α ⟫ → ⟪ α ⟫ → 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 になります。≺₁ は指名された要素どうしの所属として定義されているからです。

```agda
  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 になります。

```agda
       → 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 → Empty.⊥)
```

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

```agda
  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 にまとめます。狭義整列順序の章の自然数の実例が供給するのと同じ五つのフィールドです。

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

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

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

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

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

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

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

```agda
  _≤₁_ : ⟪ α ⟫ → ⟪ α ⟫ → 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 ブロックがそれを実行します。

```agda
  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 が一致する場合は、パスの対称性が二つ目の等式を与えます。

```agda
    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 は、二つの入力がともに反射的な順序 ≤₁ で計算された最大値以下にあることを述べています。

```agda
    go (gt h) = inr refl , inl h
```

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

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

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

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

```agda
    (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 の狭義比較があれば、対応する方向で対は真に順序づけられ、二つの等式は外の段が本当に並んでいることの証人として一緒に運ばれます。逆方向は対称です。

```agda
    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 へ降ります。

```agda
    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≺ の証明全体を、一つ下の段の比較データを消費しながら段ごとに進む一つの三重の場合分けとして読めます。

```agda
    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≺ が手に入れば、順序 ≺ はデータとして三分的であり、これが後の一意性の議論が消費する性質です。

```agda
           → 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 → Empty.⊥)
```

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

```agda
  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 は第二座標に ≺₁ の推移性を適用したにすぎず、後の最も内側の場合の合成の議論になります。

```agda
    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 が得られるからです。両方とも等式の場合が残り、第二座標の組に委ねられます。

```agda
    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 の写しです。

```agda
    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 に委ねる。

```agda
        → ((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 snd` が対の一致をそのまま回復する。

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

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

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

```agda
  _≺²_ = _≺×_ ordSWO _≺₁_ wf₁

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

  _≺³_ : (⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)) → (⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)) → Type (ℓ-suc ℓ)
  _≺³_ = _≺×_ ordSWO _≺²_ wf²
```

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

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

  ¬<₁ : (m : ⟪ α ⟫) {n : ⟪ α ⟫} → m ≡ n → (m ≺₁ n → Empty.⊥)
  ¬<₁ 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` が第一座標の狭いステップを第二段に置く。

```agda
  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 は、到達可能性の証明の添字がその証明が対象とする対を定めるように述べられており、下の再帰が自分自身に再び入れるようになっている。

```agda
    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 が適用される。したがって対の任意の降下列は級付き三つ組の降下列へ写されるが、`_≺³_` の整礎性は後者を禁じるから、対の順序に無限降下はない。

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

## 有限順序数と `Fin` の間を移る

`ω` の各要素は数項ですが、`ω` の要素であることは切り捨てられた命題であり、数項のラベルが「単に存在する」ことしか与えません。有限順序数 `# n` の内部では事情が良くなります。「この添字が `k < n` なる `# k` を表す」という命題は `hProp` なので排中律が適用でき、最小要素の探索は選ばれた最小ラベルを返します。このラベルが変換 `toFin : ⟪ # n ⟫ → Fin n` であり、`#mono` の与える繊維が逆方向の道を与えます。

探索の命題 P は、`# n` の各添字 m と各自然数 k に対して、`k < n` と「m が数項 `# k` を表す」という主張の連言をまとめたものです。その命題性は二つの事実から組み立てられます。順序 `k < n` が命題であることと、表された要素の等式が集合の中に住んでおり、その等式型も命題であることです。この連言を `hProp` に包むことが、後で排中律を適用できる根拠になります。

```agda
module FiniteBase where

  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` を得ます。結果は `∥_∥₁` の中に留まるので、この定理が与えるのは数項ラベルの単なる存在であり、選ばれたラベルではありません。証人を得るには切り捨てを非命題的な対象へ消去する必要があります。

```agda
  ω-mem→numeral β β∈ω = PT.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 を満たすことを含意します。この切り捨てられた証人を `leastOf natOrder lem` に渡すと、自然数の順序について排中律を用いて、単なる存在が選ばれた最小の対 s に変わります。その第一成分がラベル k であり、証明書の第一成分が上界 `k < n` で、これこそ `Fin n` がまとめたデータです。

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

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

```agda
    k = fst s
    k<n : k < n
    k<n = fst (fst (snd s))

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

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

```agda
    where
    s = 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 fst e) ∙ sym (toFin-spec n m₂))
```

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

```agda
  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) ≡ # (fst i)
  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)` の順方向であり、位置の対を一つの位置で数え上げます。

```agda
  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` の連結です。これは先に指摘したパターン、つまり逆の形をした写像は逆法則が供給されるまでは逆ではない、ということの実例で、ここではライブラリの同値が逆法則を供給します。

```agda
             → 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 とその証明書が得られ、単射性の仮定をその等式と合成すれば空の型の要素が得られます。

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

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

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

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

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

この設定のもとで、内側のモジュール NoInj は型 A を固定します。A はすべての `E m` から単射 `into m` を受け入れ、その単射は各レベルで単射です。その定理 no-inj は、任意の n に対して単射 `A → E n × E n` は存在しないと言います。帰結は直接的で、示された証明は構成した有限関数 g とその単射性を `no-inj-Fin (n · n)` に渡すだけだからです。すべての仕事は g の定義と g-inj の証明にあります。

```agda
    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) → Empty.⊥
      no-inj n f finj = no-inj-Fin (n · n) g g-inj
```

写像 g は、禁じられている単射 `Fin (suc (n · n)) → Fin (n · n)` であり、合成として構成されます。`n · n` より 1 大きい集合の位置 i から出発し、復号器 fromFinE が `E (suc (n · n))` の要素を作り、単射 into がそれを A へ持ち上げ、仮定された写像 f がそれを `E n` の要素の対へ送り、符号器 toFinE が各成分を `Fin n` の位置へ変えます。最後に factor がこの位置の対を `Fin (n · n)` の一つの位置へ圧縮します。

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

g の単射性は、矛盾をその構成の各層を通って後ろへ伝播させます。`g x ≡ g y` と仮定します。factor が単射なので、符号化された位置の対は一致し、toFinE が単射なのでその対の二つの成分は `E n` の要素として一致し、f が単射なので A の二つの要素は一致し、into が単射なので `E (suc (n · n))` の二つの要素は一致し、最後に fromFinE が単射なので `x ≡ y` が得られます。示された項はまさにこの連鎖に沿って内側から外側へ読めます。

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

where ブロックは中間値に名前を付け、連鎖を読みやすくします。Xx と Xy は、位置 x と y を復号してから注入して得られる A の二つの要素であり、f による像の一致を示すべき入力そのものです。命題 p-eq は中間目標、すなわち符号化された位置の対が一致することを記録します。

```agda
          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 (fst (f Xx)) , toFinE n (snd (f Xx)))
```

中間目標 p-eq はまさに factor の単射性が与えるものです。圧縮された位置の間の仮定の等式 e に factor-inj を適用すれば、それを `Fin n` の位置の対の一致へと戻せます。ここでの対は、`f Xx` と `f Xy` の二つの成分の toFinE 像からなる対です。

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

対の一致を `cong fst` と `cong snd` で射影すると、第一と第二の符号化位置のそれぞれの一致に分解されます。その後、符号器の単射性 toFinE-inj によって、それぞれが `f Xx` と `f Xy` の対応する成分の一致へと変換され、fst-eq′ が、そして一行後に第二座標の対応物が得られます。

```agda
          fst-eq = cong fst p-eq
          snd-eq : toFinE n (snd (f Xx)) ≡ toFinE n (snd (f Xy))
          snd-eq = cong snd p-eq
          fst-eq′ : fst (f Xx) ≡ fst (f Xy)
          fst-eq′ = toFinE-inj n (fst (f Xx)) (fst (f Xy)) fst-eq
```

二つの成分の一致は ΣPathP によって対の一致へと再構成されます。これは第一成分の経路と第二成分の経路を依存対の間の経路へとまとめるものです。この pair-eq こそ、最も外側の単射性の仮定 finj が消費するものであり、g-inj から始まった後ろ向きの連鎖を完了します。

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