---
title: "Ordinal indices, the Gödel pair order, and finite indices"
module: L.Ordinal.SquareLaw
lang: en
site: "Bedrock"
description: "Ordinal indices, the Gödel pair order, and finite indices"
stage: "Ordinals, injections and cardinals"
reading_order: 87
canonical: https://bedrock.institute/en/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/zh/L.Ordinal.SquareLaw.md, https://bedrock.institute/ja/L.Ordinal.SquareLaw.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Ordinal indices, the Gödel pair order, and finite indices

This chapter supplies three concrete orders and conversions used by later counting arguments: the membership well-order on an ordinal's index, the Gödel order on pairs of indices, and the correspondence between members of a finite ordinal and `Fin`.

The first construction compares two indices of an ordinal by membership of the ordinal elements they name; ordinal trichotomy and regularity turn that comparison into a strict well-order on the index type. The second grades a pair of indices by the maximum of its coordinates under that order and orders pairs sharing a maximum coordinate lexicographically; trichotomy, irreflexivity and transitivity are proved directly, and well-foundedness comes from nesting the descent inside two levels of the lexicographic product. The third reads each member of the infinite ordinal ω as a numeral and converts indices of the finite ordinal # n to and from `Fin n`. It then reduces a precise obstruction to the finite pigeonhole principle: a type that contains injective images of finite types of every size cannot itself inject into the square of a fixed finite type.

The chapter works at a fixed universe level ℓ, and it takes one classical assumption as a module parameter: a decision of every proposition at level ℓ-suc ℓ. The comparisons established later need this, because ordinal trichotomy and least-element search each settle a mere-existence question by excluded middle. Keeping the assumption as an explicit parameter records exactly which classical input each construction consumes.

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

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

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

The mathematical setting is the cumulative hierarchy V, whose sets form a type S and whose membership is truncated existence of an index. Each set a carries a chosen small presentation: an index type ⟪ a ⟫ and an embedding ⟪ a ⟫↪ whose image is a. Reasoning about members of a thus becomes reasoning about indices, and the injectivity of the embedding identifies indices naming the same element. The constructions below treat an arbitrary ordinal α with the certificate IsOrd α: a transitive set all of whose members are transitive, in the von Neumann sense.

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

A strict well-order combines four properties of one relation: any two points are trichotomically comparable, no point lies strictly below itself, strict comparison is transitive, and every descending chain is well founded. Natural numbers provide the model example. The operation leastOf uses this structure and excluded middle to select a least witness from a merely inhabited proposition-valued family; later, ordinal trichotomy supplies the same three-way comparison for members of an ordinal.

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

The logical vocabulary matches the shape of the statements to be proved. Refutations are functions into the empty type; membership proofs are inhabitants of truncated propositions; a three-way comparison is a sum of its cases, rendered by inl and inr. Paths between pairs and between records are handled by the standard lemmas Σ≡Prop and ΣPathP, which build a path into a dependent pair from paths of the components when the relevant component types are propositions.

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

The finite counting part needs arithmetic and the standard finite types. Multiplication _·_ on natural numbers sizes the square of a finite type, and the library equivalence factorEquiv identifies `Fin n × Fin n` with `Fin (n · n)`. The pigeonhole theorem supplies the impossibility that anchors the chapter's last argument: no injection from `Fin (suc n)` to `Fin n` exists. Order on the natural numbers comes with the fact that ≤ is a proposition, which makes comparisons into `Fin` respect the proof-irrelevance of their bound.

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

For each set a, the presentation map ⟪ a ⟫↪ turns an index into the member it names. Its fiber over # k therefore contains exactly the indices naming that numeral. When k < n, numeral monotonicity places # k inside # n, and choosing the corresponding fiber point defines the conversion from Fin n into the index type of the finite ordinal. The reverse conversion will use least search, because an arbitrary index does not arrive with its numeral label.

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

Well-foundedness is carried by the accessibility predicate: Acc R x holds when every R-predecessor of x is again accessible, acc packages this data, and WellFounded R asks for accessibility of every element. Accessibility certificates are handed downward in the descent arguments of this chapter. Finally, the direct operations on `hProp (ℓ-suc ℓ)` are available, making conjunction and the other logical operations on propositions available to the structure machinery used in the ordinal section.

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

open hPropStructure 𝒮ᵥ
```

Later in this chapter, well-foundedness of the Gödel pair order is obtained by embedding its descent into nested lexicographic descents. The ingredient needed for that is a general construction: given a strict well-order on X and any well-founded relation on Y, the product X × Y carries a natural strict order, and that order is well founded. This section builds exactly that, and nothing more.

Two small points shape the construction. First, the product order compares the first coordinates with the well-order, and only when neither direction of strict comparison holds, that is, when the first coordinates are equal, does it consult the second relation; recovering the equality from the two failed comparisons is what the connexity lemma does. Second, the proof carries an accessibility certificate for the first coordinate and one for the second coordinate simultaneously, mirroring the two-level priority of the order.

A strict well-order trichotomizes any two elements: the comparison data Tri returns either a proof that a is below b, a path a ≡ b, or a proof that b is below a. So if both strict directions have been refuted, only the middle case can remain, and it carries exactly the equality we want. This connexity lemma packages that case analysis; it is not a new order law but a reading of trichotomy data under two refutations.

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

The product is set up generically. The first factor carries a strict well-order u on X, giving access to its relation, its trichotomy and its well-foundedness. The second factor carries any relation _<ᵥ_ on Y that is well founded; no trichotomy or transitivity is demanded of it, since the product will only ever need to descend along it. Both relations are valued at level ℓ-suc ℓ, the level at which the later ordinal comparisons live.

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

The product order _≺×_ has two ways to compare (a , x) below (b , y). Either a is strictly below b in the well-order, or the first coordinates are equal, witnessed by the pair of refutations of both strict directions, and x is below y in the second relation. This is the lexicographic priority stated as a sum: the well-order is consulted first, the second relation only at ties. Alongside the order, the proof plans its data: accProd will build an accessibility certificate for a pair from one for each coordinate.

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

The descent follows the two-tier priority. Given that a is accessible in the well-order and x is accessible in the second relation, any ≺×-predecessor (b , y) falls into one of the two summands. If the first coordinate strictly dropped, then b is a well-order predecessor of a, so its accessibility certificate ru b h applies, and y contributes its own certificate wfv y; recursion on these two strictly smaller certificates builds the certificate for (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)
```

The tie case is where connex earns its place: the second summand asserts both strict comparisons fail, so connex produces a path b ≡ a and the pair may be transported to one with equal first coordinates, reducing descent to the second relation alone, where the certificate rv y h applies. Stacking these two clauses, every pair is accessible, since the well-order makes each first coordinate accessible and the hypothesis makes each second coordinate accessible; this is prodWF, the only statement about the product that the rest of the chapter consumes.

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

## The membership order on an ordinal's index

An ordinal α is a transitive set whose members are all transitive, and its members are linearly ordered by membership; the classical input `ord-tri` makes that order trichotomic. But the counting arguments of later chapters need the order on the indices rather than on the members themselves of the fixed presentation of α: the small type ⟪ α ⟫ whose embedding ⟪ α ⟫↪ has image α. This section transports the membership order from members to indices.

Two distinctions make the transport honest. First, an index m is not itself a set of the hierarchy; the element it names is ⟪ α ⟫↪ m, and all comparisons happen at the level of these named elements, with injectivity of the embedding recovering index equality from element equality. Second, each named element is itself an ordinal, a consequence of transitivity of α, and this is what licenses transitivity and the classical trichotomy at every index. The result is the strict well-order ordSWO on ⟪ α ⟫, the base instance on which the Gödel pair order of the next section is graded.

The relation ≺₁ on indices is defined by membership of the named elements: m ≺₁ n holds exactly when ⟪ α ⟫↪ m is a member of ⟪ α ⟫↪ n in the structure's membership proposition. Everything else in the section reads this definition. The first supporting fact is that each named element is itself an ordinal: since α is transitive and the index m names a member of α, the certificate mem-ord applied to the membership proof member α m yields IsOrd of the named element. This certificate ord-inord is used three more times below.

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

Trichotomy on indices comes from trichotomy of the named elements. The classical theorem ord-tri compares two ordinal members, returning either a proof that the first is a member of the second, a path of element equality, or a proof in the other direction, packed as a sum. The auxiliary go matches these three cases: the two membership branches become lt and gt directly, since ≺₁ was defined as membership of named elements.

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

The equality branch is the only place the presentation is used essentially. Ordinal trichotomy returns equality of the named elements, but the goal is equality of indices, and these are different types. Injectivity of the embedding, recorded as ↪-inj, reflects the element path to a path between indices. With that branch handled, tri₁ is the three-case comparison data Tri on ⟪ α ⟫.

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

Irreflexivity and transitivity are inherited from the named elements. No set is a member of itself, so m ≺₁ m refutes itself. For transitivity, m ≺₁ n and n ≺₁ k are both membership facts about ⟪ α ⟫↪ k, an ordinal by ord-inord, and the first component of the IsOrd certificate asserts transitivity of membership among the members of an ordinal, so it chains the two facts directly. Accessibility transfers the same way: if every member of the named element ⟪ α ⟫↪ m is accessible under membership, then every ≺₁-predecessor n of m names a member, so its certificate can be fed the membership fact for the index n, and acc₁ returns the accessibility of m under ≺₁.

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

Well-foundedness of ≺₁ is now one step away: regularity on the ambient hierarchy hands an accessibility certificate for membership to every set, so every named element ⟪ α ⟫↪ m is accessible, and acc₁ lifts that to accessibility of the index m. This is wf₁, the well-foundedness the search in the finite section will reuse. The record ordSWO then packages the relation with its four laws into the interface SWO, the same five fields the natural-number instance of the strict well-order chapter supplies.

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

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

Assembling ordSWO is the point of the section: an instance, not new mathematics. Every later construction that takes a SWO can now run on the index of any ordinal, and the pair order of the next section consumes exactly this instance. Nothing about ω or finite ordinals is special here; the argument used only transitivity of α, the embedding, classical trichotomy and regularity.

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

The classical Gödel pairing idea orders pairs of indices so that descent on pairs can be analyzed coordinate by coordinate. The order used here is not the plain lexicographic order: it is graded first by the ≺₁-maximum of the two coordinates, so that pairs of small coordinates sink below pairs with a large coordinate regardless of arrangement, and only pairs sharing a maximum grade are compared by first coordinate and then by second coordinate. This section defines that order and proves trichotomy, irreflexivity and transitivity directly from the corresponding laws of ≺₁; its well-foundedness, which needs the lexicographic product of the earlier section, follows in the next block of code.

The maximum requires one preliminary: a reflexive companion ≤₁ of ≺₁, defined as a sum of the strict relation and equality. Since trichotomy data is explicit three-case data, the maximum of two indices is computed by inspecting the comparison and returning one of the two inputs, and the certificate max-spec records the two ≤₁-facts that make the returned value a genuine maximum.

The non-strict companion ≤₁ collects the two ways one index can fail to be strictly above another: m ≤₁ n holds either because m ≺₁ n or because m equals n. With it, the maximum is defined from comparison data: maxGo takes the three-case comparison of m and n as an argument and returns the larger one, n when m is strictly below, and m in the two remaining cases.

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

The function maxOrd is the maximum made total: it first computes the comparison tri₁ m n and then applies maxGo to that data. Because tri₁ is classical input, maxOrd is a defined function whose values depend on that data, not on an independently proved totality claim. The specification max-spec states what makes the result a maximum: each input is ≤₁ the output, and it is proved by the same case analysis, which the following where block carries out.

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

The first two comparison cases certify both ≤₁-facts directly. If m ≺₁ n, then m ≤₁ n uses the strict branch and n ≤₁ n uses the equality branch; when m and n agree, symmetry of the path supplies the second equality.

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

The remaining case is symmetric: when n ≺₁ m, the chosen maximum is m. Thus max-spec says precisely that both inputs lie below the computed maximum in the reflexive order ≤₁.

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

The type Pair collects the square of the index: an element is a pair (a , b) of indices of α. The order ≺ on Pair is defined by its three-tier priority as a nested sum. The first summand compares grades: maxOrd a b is strictly below maxOrd c d. If the grades tie, the second summand requires the grade equality and then compares coordinates: a strictly below c, or, if a equals c, b strictly below d.

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

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

The proof of trichotomy mirrors the definition's nesting from the outside in. The outer analysis M-case compares the two grades with tri₁; when the grades are strictly ordered, the whole pairs are strictly ordered by the first summand, in either direction. Only the tie case needs the inner tiers, and tri≺ is assembled as one function returning the three-case data for any two pairs.

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

The deepest case Y-case handles pairs whose grades and first coordinates both agree, comparing the second coordinates. A strict comparison of b and d puts the pairs strictly in order in the matching direction, with the two equalities carried along as witnesses that the outer tiers really tie; the reverse direction is symmetric.

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

When the second coordinates also agree, the two pairs are equal, and cong₂ on the pairing constructor turns the two coordinate paths into a path between pairs; this is why the equality branch of the comparison data carries actual paths rather than bare tags. One tier up, X-case compares the first coordinates: a strict comparison settles the order at that tier, and the tie case descends to Y-case with the comparison of b and d.

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

Finally the top tier: M-case compares the grades themselves. The two strict cases are the first summand of ≺ applied directly. The signature of M-case spells out that its input is exactly the trichotomy data for the two grades, so the reader can see the whole proof of tri≺ as one three-fold case analysis, tier by tier, each tier consuming the comparison data of the one below.

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

The three cases of M-case close the analysis: strict in the grades, or a tie descending through the first and then the second coordinate. With tri≺ in hand, the order ≺ is trichotomic as data, which is what later uniqueness arguments will consume.

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

Irreflexivity of the pair order is short because each tier already knows how to refute its own strict comparison. If (a , b) ≺ (a , b), the witness falls into one of the three summands of the nested definition; each is a strict ≺₁-fact about a coordinate or a grade, and the corresponding irr₁ turns it into a contradiction. The grade case uses irr₁ at maxOrd a b, the first-coordinate case at a, the second-coordinate case at b.

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

Transitivity is the substantial law, and its proof is organized around the three grades: M₁ the grade of (a , b), M₂ of (c , d), M₃ of (e , f). The lemmas goY and goX handle the inner tiers first. goY is nothing but transitivity of ≺₁ applied to the second coordinates; it is the composite argument of the innermost case below.

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

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

The lemma goX composes the coordinate-level verdicts of the two strict steps. When both steps are strict in the first coordinate, transitivity of ≺₁ composes them. When one step is strict and the other is a first-coordinate equality, the strict fact is transported along that path, since a ≺₁ c and c ≡ e give a ≺₁ e by substitution. Both equalities is the remaining case, deferred to the pair of second coordinates.

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

The remaining case passes from goX to the pair of second coordinates, and their equality paths are concatenated to witness that the grades of the endpoints coincide. With these two lemmas prepared, the signature of goM states the composition problem at the top tier: from a strict step or tie between M₁ and M₂, and one between M₂ and M₃, produce the corresponding verdict between M₁ and M₃. The structure exactly mirrors goX, one level up.

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

The four clauses of `goM` are `goX` shifted one tier up. If both steps are strict between the maxima, transitivity of ≺₁ composes `M₁ ≺₁ M₂` and `M₂ ≺₁ M₃`. If one step is strict and the other is a tie at the maximum, the strict fact is transported along the equality path: `M₁ ≺₁ M₂` together with `M₂ ≡ M₃` yields `M₁ ≺₁ M₃` by substitution, and symmetrically with `sym e₁` when the tie comes first. Only when both steps are ties at the maximum do we remain there, recording `e₁ ∙ e₂` as the concatenated path of grades and delegating the second coordinates to `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₂)
```

To borrow the well-foundedness of the lexicographic product, each pair is re-exposed as a triple: `f` stores the grade `maxOrd a b` in front of the pair `(a , b)`. This map is injective for a trivial reason: a path between the triples can be projected onto the pair stored in the second component, and that projection `cong snd` recovers the pair equality outright.

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

Two lexicographic products are now instantiated with the ordinal order as the outer component. The relation `_≺²_` compares pairs of indices: first by ≺₁ on the left coordinate, and, when neither direction holds there, by ≺₁ on the right coordinate; `prodWF` supplied well-foundedness for exactly this shape. Stacking once more, `_≺³_` compares the graded triples on which `f` lands, so descent under `_≺³_` is a three-tier lexicographic descent: grade, first coordinate, second coordinate.

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

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

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

`wf³` is just the second application of `prodWF`, so `_≺³_` is well-founded without further work. The helper `¬<₁` records a small consequence of irreflexivity: if `m` and `n` are equal indices, no step `m ≺₁ n` can exist, since transporting the step backwards along the equality gives `m ≺₁ m`. This is exactly the bookkeeping the product relation needs, because `_≺×_` descends to its second tier only when neither outer direction holds. With that in place, `subrel` is typed to convert every step `p ≺ q` of the pair order into a step `f p ≺³ f q` between the graded triples.

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

The first two cases of `subrel` are direct. When the grades are already strictly ordered, the step `inl h` is itself a top-tier step of `_≺³_`, since both relations share the outer component ≺₁. When the grades tie and the first coordinates are strictly ordered, the target relation requires proof that neither grade direction holds before descending a tier; `¬<₁` on each side, applied to the tie path and its symmetry, supplies exactly those two refutations, after which `inl h` places the strict first-coordinate step on the second tier.

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

The fully tied case nests one level deeper: the grades tie, the first coordinates tie, and the second coordinates are strictly ordered, so `subrel` must refute both grade directions and then both first-coordinate directions before placing `h` on the innermost tier. Well-foundedness of the pair order then follows by pulling accessibility back along `f`: `wf≺ p` starts from accessibility of `f p` in `_≺³_`, which `wf³` provides. The private helper `go` is stated so that the index of the accessibility proof determines the pair it is about, letting the recursion below reenter itself.

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

The computation rule of `go` unpacks the accessibility data: from `acc r`, where `r` maps every `_≺³_`-predecessor of `f q` to accessibility, it produces `acc` on the pair side. Given a predecessor `q'` with `q' ≺ q`, the step is pushed forward through `subrel` to a step `f q' ≺³ f q`, fed to `r`, and `go` is applied again. Hence every descending chain of pairs maps to a descending chain of graded triples, which well-foundedness of `_≺³_` forbids, so the pair order admits no infinite descent.

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

## Moving between finite ordinals and `Fin`

Every member of `ω` is a numeral, but membership in `ω` is a truncated statement and yields only a mere existence of a numeral label. Inside the finite ordinal `# n` the situation is better: the proposition "this index represents `# k` with `k < n`" is an `hProp`, so excluded middle applies and least-element search returns a chosen least label. That label is the conversion `toFin : ⟪ # n ⟫ → Fin n`, and the fiber supplied by `#mono` gives the way back.

The search proposition `P` packages, for each index `m` of `# n` and each natural number `k`, the conjunction of `k < n` and the assertion that `m` represents the numeral `# k`. Its propositionhood is assembled from two facts: the order `k < n` is a proposition, and the equality of represented elements lives in a set, so its equality type is a proposition as well. Wrapping the conjunction into an `hProp` is what later licenses an application of excluded middle to it.

```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) ∥₁
```

Membership of `β` in `ω` itself only says that β is a numeral in the truncated sense: the specification of `ω` delivers a truncated pair of a lifted natural number and an approximation certificate. The helper `hit` refines this data into a path: the approximation `β ≈ˢ numeralV n` composed with `numeralV≡# n` yields `β ≡ # n`. The result stays inside `∥_∥₁`, so this theorem gives a mere existence of a numeral label and not a chosen one; a witness would require eliminating the truncation into a non-propositional target.

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

For an index of the finite ordinal `# n` there is a concrete inhabitant to start from: the membership of the represented element in `⟪ # n ⟫` implies, via `∈#-elim`, that some `k < n` satisfies `P`. Feeding this truncated witness to `leastOf natOrder lem` uses excluded middle at the natural-number order to turn mere existence into a chosen least pair `s`. Its first component is the label `k` and the first component of its certificate is the bound `k < n`, which is exactly the data `Fin n` packages.

```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 : ℕ
```

The specification of `toFin` says more than the type bound: the least label `k` satisfies the full second conjunct of `P`, namely that the index `m` represents `# k`. This is the second component of the certificate returned by the least-element search, and it is the path that the injectivity proof below will consume.

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

Injectivity of `toFin` follows by transporting the two specification paths along the assumed equality of labels. If `toFin n m₁` and `toFin n m₂` agree, their first components agree, so `# (fst (toFin n m₁))` and `# (fst (toFin n m₂))` are connected by a path; concatenating with the two specifications gives a path between the represented elements, and `↪-inj` reflects equality of represented elements back to equality of indices, as it did for the ordinal order.

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

The reverse direction starts from `#mono`, which witnesses that `# k` is a member of `# n` whenever `k < n`. Since the index type `⟪ # n ⟫` presents the members of `# n`, that membership comes with a fiber: an index whose represented element is `# k`, together with a certificate of exactly the shape that `fromFin-spec` records. So `fromFin n (k , k<n)` is the first component of this fiber, chosen by the presentation rather than by least search.

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

Injectivity of `fromFin` uses that `Fin n` is a subtype: its second components are bounded naturals, a proposition-valued family, so an equality of pairs reduces to an equality of first components. The path between represented elements obtained from the two specifications and `e` is converted by `#-inj′` into a path of natural numbers, and `Σ≡Prop` lifts that to a path in `Fin n`. The section then introduces `factor`, defined as the forward direction of the standard equivalence `factorEquiv : Fin n × Fin n ≃ Fin (n · n)`, which enumerates pairs of positions by a single position.

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

Because `factor` is an equivalence and not merely a function, its injectivity needs no new case analysis: if `factor n x` and `factor n y` agree, applying the inverse and using the round-trip law `retEq` on each side returns `x` and `y` themselves. The proof is the concatenation of `sym (retEq ...) x`, the transported equality, and `retEq ... y`. This is the pattern noted earlier: a map shaped like an inverse is not an inverse until the inverse laws are supplied, and here the library's equivalence supplies them.

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

The pigeonhole statement is the finite core of the later contradiction: no function `Fin (suc n) → Fin n` can be injective. The library result `pigeonhole`, applied with the reflexivity witness `≤-refl {m = suc n}`, produces two positions `i` and `j` together with a certificate that they are distinct yet `f i ≡ f j`; composing the injectivity hypothesis with that equality yields an element of the empty type.

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

The unpacking separates the pigeonhole certificate into the parts the final line needs: `i` and `j` are the two colliding positions, `i#j` is their distinctness, and `feq` is the equality of their images. The computation `i#j (finj i j feq)` then applies the injectivity hypothesis to obtain `i ≡ j` and feeds it to the distinctness, producing the contradiction.

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

The final block abstracts away from omega. It is parameterized by a family `E : ℕ → Type ℓ` together with an injective encoder `toFinE : E n → Fin n` and an injective decoder `fromFinE : Fin n → E n`. Note what is and is not assumed: each direction comes with its own injectivity proof, but the two are not required to be mutually inverse, and no equivalence between `E n` and `Fin n` is claimed. Only the two injectivities enter the argument.

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

Inside this setup, the inner module `NoInj` fixes a type `A` that receives an injection `into m` from every `E m`, itself injective at each level. Its theorem `no-inj` says that no injection `A → E n × E n` can exist for any `n`: the reduction is immediate, because the displayed proof simply hands the constructed finite function `g` to `no-inj-Fin (n · n)` together with its injectivity. All the work lies in defining `g` and proving `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
```

The map `g` is the forbidden injection `Fin (suc (n · n)) → Fin (n · n)`, built as a composition. Starting from a position `i` of a set one larger than `n · n`, the decoder `fromFinE` produces an element of `E (suc (n · n))`, the injection `into` lifts it into `A`, the assumed map `f` sends it to a pair of elements of `E n`, and the encoder `toFinE` turns each component into a position of `Fin n`. The pair of positions is finally compressed by `factor` into a single position of `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
```

Injectivity of `g` propagates the contradiction backwards through each layer of its construction. Assume `g x ≡ g y`. Since `factor` is injective, the pair of encoded positions is equal; since `toFinE` is injective, the two components of the pair are equal as elements of `E n`; since `f` is injective, the two elements of `A` are equal; since `into` is injective, the two elements of `E (suc (n · n))` are equal; and since `fromFinE` is injective, `x ≡ y`. The displayed term reads inside out exactly along this chain.

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

The `where` block names the intermediate values to keep the chain readable. `Xx` and `Xy` are the two elements of `A` obtained by decoding the positions `x` and `y` and then injecting them; they are the inputs whose images under `f` must be shown equal. The statement `p-eq` records the intermediate goal: the pairs of encoded positions agree.

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

The intermediate goal `p-eq` is exactly what the injectivity of `factor` delivers: applying `factor-inj` to the assumed equality `e` between the compressed positions converts it back to an equality of the pairs of positions in `Fin n`, here the pairs of `toFinE`-images of the two components of `f Xx` and `f Xy`.

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

Projecting the pair equality with `cong fst` and `cong snd` splits it into equalities of the first and second encoded positions. Each is then converted back into an equality of the corresponding components of `f Xx` and `f Xy` by the encoder's injectivity `toFinE-inj`, giving `fst-eq′` and, one line later, its second-coordinate counterpart.

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

The two component equalities are reassembled into an equality of pairs by `ΣPathP`, which packages a path of first components and a path of second components into a path between dependent pairs. This `pair-eq` is precisely what the outermost injectivity hypothesis `finj` consumes, completing the backward chain begun at `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′)
```