---
title: "Well-orders on finite stages"
module: L.Choice.FiniteStageOrders
lang: en
site: "Bedrock"
description: "Well-orders on finite stages"
stage: "The canonical well-order and Choice"
reading_order: 74
canonical: https://bedrock.institute/en/L.Choice.FiniteStageOrders.html
html: L.Choice.FiniteStageOrders.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/FiniteStageOrders.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal, L.Axioms.Basic, L.WellOrder.Base]
routes: [canonical-order]
translations: [https://bedrock.institute/zh/L.Choice.FiniteStageOrders.md, https://bedrock.institute/ja/L.Choice.FiniteStageOrders.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Well-orders on finite stages

This chapter proves that every numeral-indexed stage is finite and equips it with the earliest-disagreement well-order, then combines stage number and local order to well-order the limit stage.

The earlier choice construction locates, for each cell of a family, the stage at which the cell first has a member, and showed that this stage is a successor. Every member of the cell that appears exactly there is therefore a definable subset of one and the same set: a name written over a single stage. What is still missing is a way to **compare** those names, and comparison is what this chapter builds, at the bottom of the tower.

The chapter rests on two claims. The first is that each stage indexed by a numeral is finite, in the precise sense given below: it comes with a finite list of sets that includes all of its members. The second is that a finite stage carries a well-order, obtained by comparing two of its members at the earliest point where they disagree, and giving the larger place to whichever of the two contains that point.

The second claim is the mathematical content, and it is a claim about **finite** sets in an essential way. Order the subsets of the natural numbers by that same recipe and there is an infinite descent: the set of all numbers, then all numbers from one on, then all from two on, and so forth, each step deleting the earliest surviving point and so landing strictly lower. Nothing about the recipe forbids this; what forbids it over a finite base is that a finite base has only finitely many subsets, so a search for a smallest one terminates. The well-foundedness proof below goes exactly this way: a finite list plus a linear order yields a smallest member of any inhabited property, by scanning the list and keeping, at each step, the smallest candidate so far; and "every inhabited property has a smallest member" is, classically, well-foundedness.

Finiteness propagates up the tower because the definable subsets of a finite set are all of its subsets, and a set with a list has only finitely many subsets, one for each vector of bits over that list. So a list of the stage yields a list of the next stage, and the recursion is enough to carry the whole construction through.

The limit-stage construction does not require a compatibility theorem for the finite-stage orders. It uses the first stage at which an element appears as the primary key. Two members of the limit that first appear at different finite stages are compared by those stage numbers alone; two that first appear at the same stage are compared by that stage's own order. No compatibility between the finite-stage orders is needed, and none is asserted.

The setting is the constructible universe built over the ambient cumulative hierarchy $V$. Excluded middle enters here as an explicit hypothesis: the module is parameterized by a decision `lem` for every proposition at level `ℓ-suc ℓ`. This one level is all the chapter asks for, and every construction below is allowed to call this single fixed decision; nothing is claimed for propositions at other levels beyond what the displayed theorems actually prove.

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

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

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

The names used throughout are those of the constructible hierarchy: a stage `Lset α` of the tower, the operator `𝒟ₒ` producing the definable subsets of a stage, and the fact `numeral-ord` that the numeral `# n` is an ordinal. In particular each finite stage `Lset (# n)` is a genuine stage, which is what lets the recursion of later sections climb the numerals. Also imported is `Lset-suc` and the `FinOf` machinery, which ties a stage to the finite sets inside it.

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

Comparison needs a base order with trichotomy. The order `natOrder` on natural numbers is a strict, strongly well-founded linear order packaged as `SWO`, with a three-case comparison `Tri` split into `lt`, `eq`, `gt`. The search routines of later sections are written against this interface, so they work for any `SWO`, and the natural number instance is the one that orders the numerals.

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

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

Booleans enter as masks: to enumerate the subsets of a tallied set, each entry is either kept or dropped, recorded by `true` or `false` on `Bool`, where `false≢true` distinguishes the two. On the index side, natural numbers are compared with the strict order `_<_`, which is transitive and well-founded, admits no loops by `¬m<m`, and is decidable via `_≟_`. These are precisely the properties needed to find the least index witnessing a property, and to make head-on decisions inside a scan.

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

Well-foundedness here is the accessibility predicate `Acc`: a point is accessible when every predecessor is accessible, packaged by the constructor `acc`. A relation is well-founded, of type `WellFounded`, when all its points are accessible. The proof obligations from `Acc` are propositions, which is recorded by `isPropAcc` and used when eliminating merely existential data into an accessibility statement. The module `WFI` supplies the recursion principle that consumes a well-founded relation.

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

For a set `x` in the cumulative hierarchy, `⟪ x ⟫` is its small presentation type and `⟪ x ⟫↪` embeds that type into the hierarchy. The equivalence `∈∈ₛ` relates presentation membership to hierarchy membership, while `∈-asFiber` recovers an index and its identifying path from a membership proof. The empty set supplies stage zero, and the von Neumann numerals `# n` with their limit `ω` index the finite stages and their limit.

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

Membership statements below are proposition-valued. Thus `⟨ x ∈ˢ A ⟩` is the type of evidence that `x` belongs to `A`; tallies use this form both to certify each listed entry and to state that every member is represented.

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

open hPropStructure 𝒮ᵥ
```

## Tallies

A `Tally` presents every member of a set by a finite indexed family, allowing repetitions and requiring neither injectivity nor decidable equality.

Finiteness enters as a **tally**: a number, a family of that many sets all belonging to `A`, and the statement that every member of `A` is merely one of them. `onto` records that every member is merely represented in the family.

Repetitions and undecidable equality cause no difficulty. A scan may revisit the same element, and a bit vector records choices by position even when two positions name the same set. This deliberately weak finiteness notion is therefore stable under the construction of the next stage.

A tally of a set `A` has three data fields. The number `size` fixes how many entries are listed, and `item` turns each valid position, an element of `Fin size`, into a set `item i`. The field `inside` certifies that every listed entry genuinely belongs to `A`; without it, a longer list would trivially cover a small set. Note that the same element may well appear at several positions: the record does not prevent this, and no field asks whether two positions hold the same set.

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

The fourth field states coverage. Given `x` together with a proof that it belongs to `A`, `onto` returns the propositional truncation of an index `i` and a path `item i ≡ x`. Thus an index exists merely, without exposing a chosen position. Later eliminations use this truncated witness only when their targets are propositions.

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

## Splitting a finite index

The maps `splitFin` and `joinFin` identify an index below a sum with an index in one summand, supplying the arithmetic used to enumerate masks.

Tallying a power set means enumerating bit vectors, and there are twice as many vectors of length `n + 1` as of length `n`. So one piece of index arithmetic is needed: an index below `a + b` is either an index below `a` or an index below `b`, and conversely. Only one of the two round trips is ever used, so only that one is proved; `bumpLeft` is the shift that makes the recursion on `a` type-check.

A concrete picture helps. If `a = 2` and `b = 3`, an index below `5` is exactly either an index below `2` or one below `3`: `joinFin` sends the left summand to the first two slots and the right summand to the last three, while `splitFin` asks which zone an index fell into. Repetitions are irrelevant here, since these maps concern positions, not the entries that later sit at them.

The first map concerns sums whose left side grows by one. `bumpLeft` takes an index in either `a` or `b` and produces an index in `suc a` or `b`: a left index is pushed one slot further out, a right index is left alone. It has no content of its own; it exists so that the recursive step of `splitFin`, which peels one slot off the left summand, can restore a left index to the right type. Note `joinFin` is stated only in the direction from `Fin a ⊎ Fin b` to `Fin (a + b)`, with `a` explicit so the recursion can pattern-match on it.

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

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

`joinFin` and `splitFin` are mutual inverses in shape, though only one round trip will be proved. `joinFin` is recursive in `a`: at `zero` an index below `0 + b` is just an index below `b`, and at a successor the first slot belongs to the left summand, so a left index at position zero maps to slot zero and everything else shifts up by one. `splitFin` runs the same recursion backwards: an index below `a + b` first asks whether it is below `a`, and the `suc` case uses `bumpLeft` to restore the peeled type.

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

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

The round trip `split-join` says that splitting an index that was just joined returns the original left-or-right index. Every clause is either `refl` or a application of `cong` to the recursive path: the computation of `splitFin (joinFin x)` already reduces to `bumpLeft` applied to the recursive answer, and `cong bumpLeft` carries the induction hypothesis through that shift. The opposite composite is never claimed, and nothing here asserts that joining is injective.

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

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

What this buys for the mask section is exact bookkeeping of sizes. When the enumeration of masks at length `suc n` splits its index in half at `maskCount n`, `splitFin` decides whether the leading bit is `false` or `true` and hands the remaining index to the recursion at `n`, where `mask-onto` and `split-join` together show that every bit vector is reached.

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

## Enumerating the masks

`maskAt` enumerates every Boolean vector of a fixed length, and `mask-onto` proves that every selection pattern occurs.

A **mask** of length `n` is a vector of `n` bits; it will say, of a tallied set, which entries to keep. There are `maskCount n` of them, that number being two to the `n` written as an iterated doubling, and `maskAt` reads an index as a mask: split the index in half, and the half it lands in supplies the leading bit while the rest supplies the tail. Every mask is read off some index, which is `mask-onto`, and that is the only property of the enumeration that is needed. No pointwise injectivity property is required.

For `n = 2`, the four indices give the four masks from `false ∷ false ∷ []` through `true ∷ true ∷ []`. The construction in fact enumerates them without repetition, although the later tally argument needs only the proved coverage `mask-onto` and does not rely on injectivity.

The count of masks is defined by the recursion it will be enumerated with: length zero admits exactly one mask, and a mask of length `suc n` is a leading bit together with a mask of length `n`, giving the sum `maskCount n + maskCount n`. This is two to the `n` written as iterated doubling, which is exactly the shape `splitFin` expects, since both numbers being added are the same.

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

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

`maskCons` glues a leading bit onto a tail read from the appropriate half of the index, choosing `false` for the left summand and `true` for the right. `maskAt` then reads an index as a mask: at length zero the only mask is the empty vector, and at length `suc n` the index below `maskCount (suc n) = maskCount n + maskCount n` is split in half, the half naming the leading bit and the inner index naming the tail. The reading is a definition, not a theorem: it simply computes.

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

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

Coverage is the content of `mask-onto`, and it is deliberately untruncated: given a vector `v`, the statement produces an actual index together with a path from the mask read there to `v`. At the base the empty vector comes from the zeroth index. The recursion follows the vector itself, so the enumeration can deliver this explicit index rather than only its mere existence.

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

At a successor the vector decides the branch. For a leading `false` the tail's index is joined into the left half by `joinFin`, and the path is assembled in two steps: first `split-join` shows that splitting the joined index recovers the left half as claimed, and then the recursive path is carried under the leading bit by `cong (false ∷_)`. The `true` case is verbatim the same with the right half. Together with the count, this says the masks of a tallied set are covered by `Fin (maskCount size)`, which is exactly the shape a `Tally` field expects.

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

## Selecting a sub-family

`select` filters a finite family by a Boolean mask, while its membership lemmas connect selected entries with the positions marked true.

`select` applies a mask to a family: it keeps the entries whose bit is `true` and returns them as a family again, together with its own length. The length is **produced by the recursion**, which is the point: nothing has to be counted, and no arithmetic relates the answer to the mask.

Two specifications say what the result contains, and both are untruncated, because each is read straight off the same recursion. `marks` runs in the other direction, turning a decision on the entries into the mask that records it.

A small example shows the interaction with repetitions. Take a family with a repeated entry and the mask that keeps both copies: the selection then contains that entry twice, and both copies are answered by the lemmas, each with its own original position. Nothing is lost or merged, because nothing is ever required to be unique.

The helper `selectStep` performs one step of the filter: given an entry `x` and an already-selected family, it prepends `x` and reports the new length `suc k`. Its result type packages the family with its length in a dependent pair, so the recursion can grow the length without ever consulting the mask arithmetically.

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

`select` is a recursion on the mask. The empty mask selects nothing, signaled by an absurd pattern: there is no position in a family of length zero. A leading `false` drops the head and recurses on the shifted family; a leading `true` keeps the head with `selectStep`. At each step the family is shifted by one, which is what the `λ i → f (suc i)` throughout records.

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

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

The first specification, `select-out`, reads the selection forwards: every position `j` of the selected family comes from some original position `i` whose bit is `true`, and the entry there really is the original entry `f i`. The claim is data, not a mere existence: an actual witness `i` is produced, with both the bit and the equality given explicitly.

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

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

The proof walks the same recursion as the definition. In the `false` case the head is gone, so the original position answering `j` in the tail is shifted up to `suc i` in the full vector; the local `step` performs exactly this bookkeeping on the witness triple.

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

In the `true` case there are two subcases. If the selected position is the first, the answer is the head itself, with both equations holding by `refl` because `select` returned the head untouched as slot zero. Otherwise the recursion answers the tail positions, and the same shift applies.

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

The second subcase repeats the shift bookkeeping, now with the head present: the selected family of `true ∷ v` is the head followed by the selection of the tail, so a position beyond the head answers in the tail and maps back to `suc i`. The two branches differ only in this relocation, which is why both need their own `step`.

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

The converse specification, `select-in`, says every marked entry is selected: an original position `i` whose bit is `true` has a selected position `j` whose entry is `f i`. Again the claim is explicit data, an actual `j` together with a path. Nothing is truncated in either direction, which is what lets the later membership arguments pass real witnesses across the selection.

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

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

Its proof mirrors the recursion from the other end. A position in an empty family is absurd. In a `false` case the head cannot be marked true, so the hypothesis `e` contradicts `false≢true`; a shifted position recurses. In a `true` case the head answers with position zero, and deeper positions recurse.

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

The final clause performs the prepend bookkeeping: the position found in the tail becomes `suc j` in the family that now has the head in front, with the entry equality carried through unchanged. Both specifications together say that the selection is neither larger nor smaller than what the mask marked, though nothing asserts the two ways of matching positions are mutually inverse.

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

`marks` runs the filter in reverse: instead of reading a mask and keeping entries, it takes a Boolean verdict `d` on entries and writes down the mask recording it, one bit per position. The base is the empty vector, and the step asks `d` at the head and recurses on the shifted family.

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

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

`marks-lookup` certifies that the recorded mask really answers the verdict at each position: looking up position `i` in `marks n f d` gives `d (f i)`. The head case is `refl` by the computation rule of `marks`, and deeper positions recurse. This lemma is what lets `maskOf` later prove that the mask it writes down reproduces a given subset.

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

## A truth value, decided into a bit

Excluded middle turns each proposition into the Boolean bit used by a mask, and the two specifications recover truth and falsity from that bit.

The excluded middle hands over a disjunction, while a mask requires a bit, so the two have to be connected. The verdict is taken as an argument rather than looked up inside the definition: that is what lets the two round-trip lemmas be proved by matching on it, with the truth value itself supplied explicitly so that the round-trip statement has the intended proposition as its parameter.

This conversion is one concrete use of excluded middle in the tally construction: it decides a membership proposition and records the answer as a bit.

`decideOf` turns a verdict into a bit: the left alternative, a proof of `⟨ P ⟩`, is recorded as `true`, and the right, a refutation of `⟨ P ⟩`, as `false`. The proposition `P` itself is irrelevant to the computation; only the verdict is matched, which is why the definition is a pair of equations rather than a proof.

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

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

The two round trips connect the bit back to the truth value. `decide-true` says a proof of `⟨ P ⟩` forces the bit to be `true`: in the refutation branch the proof itself would be refuted, which is a contradiction. `decide-sound` reads the other way: a bit of `true` yields a proof of `⟨ P ⟩`, taken directly from the left branch or obtained because the right branch would force `false ≡ true`. Together they say the bit faithfully answers whether `⟨ P ⟩` holds, for the verdict that was passed in.

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

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

## The definable subsets of a tallied stage

Finiteness travels up the tower through this section. Fix an ordinal `σ` and a tally of the stage `Lset σ`; the goal is a tally of `𝒟ₒ (Lset σ)`, the definable subsets of that stage. Each entry of the given tally is a member of the stage, hence has a name in the stage's small member type; a mask over the tally selects which names to keep, and `part` spans the kept names into a finite set. By the basic-axioms chapter's `finSet∈𝒟ₒ`, such a spanned set is a definable subset of the stage, defined by the finite disjunction of "equals one of these entries". Conversely, any definable subset `x` of the stage can be recovered: mark each tally entry according to decidable membership in `x`, and the spanned set of that mask is exactly `x`, where the inclusion `𝒟ₒ∋⊆` guarantees that every member of `x` is listed by the tally in the first place. So masks, of which there are `maskCount size`, merely cover all definable subsets, and that is precisely what a `Tally` demands.

A member of `Lset σ` lives in the stage as a set, but `finSet` needs a name in the small member type `⟪ Lset σ ⟫`. The embedding `⟪ Lset σ ⟫↪` reads such a name as a set. Membership is presented as a truncated fiber, but this embedding has proposition-valued fibers, so `∈-asFiber` may eliminate the truncation and return an explicit name together with its path to `item i`. The definitions `index i` and `index-eq i` are the two projections of that fiber element. This does not choose an index from an arbitrary finite tally fiber, whose repetitions need not be proposition-valued.

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

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

The second component of the same fiber is the path `index-eq i`, recording that the embedded name returns to `item i` along a path, not by a definitional equation. Every later transfer between the set `item i` and the name `index i` will go through this path by transport. With the names in place, a mask `v` over the tally is turned into a selection: `chosen v` is a length together with a function listing exactly the selected names, as built by the earlier `select`.

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

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

  part : Vec Bool size → S
```

`part` is the spanned set: it reads each selected name through the embedding and forms the finite set of the results, landing in the type `S` of sets. Because a finite family of members of `Lset σ` spans a definable subset of that stage, `part-def` obtains the certificate `⟨ part v ∈ˢ 𝒟ₒ (Lset σ) ⟩` directly from `finSet∈𝒟ₒ`, with no further work. The first specification then reads membership backwards: if `y` lies in `part v`, then merely there is a tally position whose bit is `true` and whose entry equals `y`.

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

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

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

The proof composes two steps. First, `finSet-out` unwraps membership in the spanned finite set: it merely produces a position `j` in the selection with the embedded name equal to `y`. Second, `select-out` traces that position back to its origin in the full tally, recovering the index `i` with `lookup i v ≡ true` and the agreement `chosen v .snd j ≡ index i`. Both steps produce their data inside the truncation, so no chosen witness is extracted from a mere existence claim.

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

The final equality has the source direction `item i ≡ y`. First `sym (index-eq i)` goes from `item i` to the embedded name `index i`. Next, `select-out` gives `chosen v .snd j ≡ index i`, so its symmetry is mapped through the embedding to reach the selected embedded name. Finally the path `q` supplied by finite-set membership reaches `y`. Their concatenation is exactly the three paths displayed in the proof.

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

The opposite specification runs forward. If the bit at position `i` is `true`, the entry `item i` does belong to `part v`. The reason is that the selection really contains that name: `select-in` finds, for every marked position, a slot in the chosen family holding the same name, and `finSet-in` then certifies membership of the embedded form.

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

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

Since membership in the spanned set is stated for the embedded name while the goal concerns the entry `item i`, the two are connected by the path `path` below, and `subst` moves the membership certificate along it. The auxiliary `ins` holds the slot that `select-in` produces: a position in the chosen family whose entry equals `index i`.

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

The remaining path `path` concatenates the slot's equality with `index-eq i`, so the transported membership is exactly membership of `item i`. With both directions in place, the construction can now be run in reverse. `maskOf` assigns to any set `x` the verdict mask obtained by deciding, for each tally entry, whether it belongs to `x`; excluded middle `lem` supplies the disjunction, and `decideOf` turns it into a bit. The goal `part-mask` states that for a definable subset `x` of the stage, the spanned set of this mask is `x` itself.

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

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

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

Membership in a set of the hierarchy is a proposition, so extensionality `extensionalV` reduces the claimed equality `part (maskOf x) ≡ x` to a pointwise equivalence of membership statements; `⇔toPath` assembles the two directions into the path. The forward direction shows every member of the spanned set lies in `x`.

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

The hypothesis of the forward direction is itself merely an existence: some marked position with entry equal to `y`. Because the target `⟨ y ∈ˢ x ⟩` is a proposition, the truncation may be eliminated into it. The recorded witness is a position `i` whose bit is `true` and whose entry is `y`; since the bit was computed by deciding membership of that very entry in `x`, reading the bit back with `decide-sound` yields membership in `x` for `item i`, and the equality `item i ≡ y` transfers it to `y`.

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

The backward direction starts from membership of `y` in `x` and must produce membership in the spanned set. Since that target is again a proposition, its truncated hypothesis can be eliminated. Here the hypothesis comes from the tally's coverage: `x` is a definable subset of the stage, and `𝒟ₒ∋⊆` says every member of a definable subset of `Lset σ` is a member of `Lset σ` itself, so the tally's `onto` merely lists `y` as some entry `item i`.

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

Given the entry `i` equal to `y`, it suffices to show `item i` belongs to the spanned set and transport along `item i ≡ y`. By `part-mem`, membership needs the bit at `i` to be `true`. And it is: the mask recorded the decision for `item i ∈ˢ x`, and since `y` belongs to `x`, the path `item i ≡ y` transports that proof so `decide-true` forces the bit to be `true`.

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

Both directions of `part-mask` are now assembled, and the section's payoff is at hand. Since every mask arises from some index via `mask-onto`, the masks enumerate, merely and with repetitions allowed, all definable subsets of `Lset σ`. There are `maskCount size` of them, so `powerTally` records a tally with that size, whose entry at index `j` is the spanned set of the mask `maskAt size j`. The remaining fields complete the record: each entry carries its definability certificate, and the coverage clause is supplied next.

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

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

The record's `inside` field reuses the certificate `part-def` at each enumerated mask, so every entry of `powerTally` is genuinely a definable subset of the stage. It remains to check `onto`, the truncated coverage. Given any definable subset `x` of `Lset σ`, we must merely exhibit an index whose enumerated entry equals `x`.

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

The witness index is the one that `mask-onto` produces for the verdict mask `maskOf x`. The enumerated entry at that index is `part (maskAt size j)`, which equals `part (maskOf x)` after rewriting the mask along the produced path, and `part-mask` then identifies that with `x`. The whole statement lands in a truncation, which is all a `Tally`'s coverage requires: every definable subset is hit, though not necessarily by a unique mask.

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

## Smallest elements, and well-foundedness

This section spends the tally built earlier rather than making one. Fix a type with a relation that is trichotomous, irreflexive and transitive: everything a strict well-order asks for except well-foundedness. The procedure `scan` walks a finite family and returns, without any truncation, either an entry that satisfies the predicate and is smallest among the entries that do, or a refutation showing no entry satisfies it. It is a plain recursion on the length: at each step excluded middle decides the predicate at the head, and trichotomy compares the head with the best found so far; the four combinations are the four clauses. The absence of truncation matters, because the caller wants an actual element, not a mere existence. Assuming the family merely covers the whole type, `Search.Over.least` upgrades this to a smallest element of any merely inhabited predicate over the whole type: the no-entry-satisfies-it branch is refuted by the witness, whose fiber in the family the predicate would have to hit. Well-foundedness then follows by the minimal-counterexample argument, described when its code is reached.

Fix a strict relation `≺` on `A` with trichotomy, irreflexivity and transitivity. The aim is to derive well-foundedness from a finite covering family rather than assume it. For a predicate `P`, `Least P m` records both that `m` satisfies `P` and that every strictly smaller satisfier leads to contradiction.

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

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

The scan's output type `Found P n f` is a disjunction of two explicit alternatives. In the left one, some position `i` holds an entry satisfying `P` and no other entry satisfying `P` lies below it within the family. In the right one, every entry fails the predicate. Both alternatives carry full data rather than truncated existence, which is what lets the later constructions return actual elements.

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

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

`scan` is defined by recursion on the family's length. The empty family returns the right alternative vacuously. For a family with a head, the recursion first handles the tail, shifting positions by one, and the verdict of excluded middle on `P` at the head is handed to `combine`, which merges the tail's outcome with the head's verdict into an outcome for the whole family.

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

The first clause of `combine` handles the case where the tail already yielded a smallest satisfier `f (suc i)` and the head also satisfies the predicate. Then two candidates compete, and trichotomy decides which of `f zero` and `f (suc i)` is smaller; the auxiliary `decide` analyses the three outcomes of that comparison.

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

If the head is strictly below the tail's champion, the head becomes the new champion. Its minimality is verified position by position: at the head itself, a claim `f zero ≺ f zero` contradicts irreflexivity outright; at a tail position, transitivity chains `f j ≺ f zero ≺ f (suc i)` and hands the result to the tail's already-established minimality `mi`.

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

If the head equals the tail's current least candidate, that candidate remains least. A hypothetical comparison placing the head below the candidate is transported along their equality into a self-comparison of the candidate and contradicted by irreflexivity; tail positions are still handled by `mi`.

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

If the tail's champion is strictly below the head, it survives. A hypothetical entry below the champion now has two ways down: transitivity through the head `f (suc i) ≺ f zero ≺ f (suc i)` produces a self-comparison refuted by irreflexivity, while the tail's own positions go to `mi`. The champion's certificate is thus rebuilt from the old one in every branch.

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

The second clause keeps the tail's champion when the head fails the predicate. No comparison is needed at all: the head cannot challenge the champion because it does not satisfy `P`, so a supposed counterexample at the head is refuted directly by the verdict `n₀`, and tail positions again go to `mi`.

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

Symmetrically, when the tail had no satisfier at all and the head does satisfy the predicate, the head is the new champion. Its minimality is immediate: the head itself is handled by irreflexivity, and any tail position satisfying the predicate would contradict the tail's refutation `none`.

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

The last clause is the agreement case: neither the tail nor the head supplies a satisfier, so the whole family is reported as satisfying nothing. The refutation is assembled positionwise, dispatching the head to `n₀` and each tail position to `none`. With this clause the four combinations announced in the lead are complete.

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

The sub-module `Over` adds the one premise that turns a finite family into a tally: `cov` says every element of `A` is merely hit by the family, a truncated coverage with repetitions allowed. Under this premise `least` upgrades the scan's answer to a least element for the whole type: its input is only a truncated witness that some element satisfies `P`, and its output is explicit data, an element together with `Least P m`.

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

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

Inside `least`, the auxiliary `nowhere` disposes of the scan's no-satisfier branch: assuming no entry satisfies `P`, it must refute the given truncated witness. The elimination is legitimate because the target is the empty type, a proposition, so the truncation of the witness may be taken apart without choosing anything.

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

Concretely, the witness supplies an element `a` with `⟨ P a ⟩`, and the coverage `cov a` merely names a family position `i` with `f i ≡ a`; again the target is a proposition, so the fiber may be read. Transporting the proof of `⟨ P a ⟩` backwards along `f i ≡ a` gives `⟨ P (f i) ⟩`, which the assumed refutation `none` turns into a contradiction. The next lines carry out exactly this transport.

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

The transport announced earlier is carried out here, in both components at once. Given a supposed entry `b` of the whole type below the champion, with `⟨ P b ⟩` and `b ≺ f i`, the coverage merely names a family position `j` with `f j ≡ b`; both the satisfaction and the comparison are transported backwards along that path, and the champion's family-level certificate `mi` refutes them together. Hence the scan's only remaining branch, the refutation `none`, is outright contradictory, since the witness was shown to force a satisfier into the family.

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

    wellFounded : WellFounded _≺_
```

To prove well-foundedness, first decide accessibility of an arbitrary `a`. The positive case returns its certificate. In the negative case, finite search produces a least element `m` whose accessibility is refuted. If every predecessor of `m` is accessible, `acc below` makes `m` accessible; applying the refutation stored in `found` to this certificate yields the contradiction. The original refutation of `a` is used only to witness that the predicate of non-accessibility is inhabited.

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

The property to be minimized is `NotAcc`, non-accessibility. Its underlying statement is a negation, and negations are propositions, so `NotAcc` is a legitimate truth value `Ω` and `least` may be applied to it. The input is the truncated pairing of `a` with the assumed refutation `nh`, so the hypothesis merely says that the set of non-accessible elements is nonempty.

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

Let `m` be the least non-accessible element just found. To show it accessible, one must show every predecessor `b` accessible, and accessibility of `b` is again a proposition, so it is decided once more by excluded middle; the auxiliary `pick` returns the certificate in the affirmative branch.

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

In the negative branch, `b` would be a non-accessible element strictly below the least non-accessible element `m`, and the minimality clause of `Least NotAcc m` refutes exactly that. Hence every predecessor is accessible, the certificate `acc below` is legitimate, and feeding it to the assumed refutation of accessibility closes the contradiction. Note that no infinite descending sequence was ever constructed or excluded; the argument is entirely this contradiction.

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

## The earliest disagreement

This section defines the order that finite stages will carry. Fix a set `A` and a relation `R` on sets, read as an order on the members of `A`. Two subsets of `A` are compared by looking at where they disagree. A witness that `x` comes before `y` is a member `z` of `A` that belongs to `y` and not to `x`, such that `x` and `y` **agree** below `z`, meaning that every member of `A` that `R` puts before `z` belongs to one exactly when it belongs to the other. Read backwards: `z` is the earliest point of disagreement, and `y` is the one that has it. The relation `precedes R A` is the truncated existence of such a witness, and irreflexivity is immediate and needs no hypothesis at all: a witness for `x` against itself would belong to `x` and not belong to `x`. The later proofs establish trichotomy and transitivity from hypotheses on the base order, and use finiteness for well-foundedness.

The two ingredients are stated separately. `Agrees R A x y z` says that membership in `x` and in `y` coincides for every member `w` of `A` that `R` places before `z`, in both directions. `Witness R A x y z` then assembles the full witness: `z` lies in `A`, it belongs to `y`, it does not belong to `x`, and agreement holds below it. The direction of the membership clauses is what decides which side wins the comparison.

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

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

`precedes R A x y` is the proposition that such a witness merely exists, packaged with `PT.squash₁` as a truth value. Because the witness is hidden behind a truncation, its existence is all that is asserted; nothing chooses `z`. Irreflexivity then costs one line: eliminating the truncation into the empty type, a proposition, exposes a witness with `z ∈ x` and `z ∉ x`, and the second clause applied to the first is the contradiction.

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

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

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

Transitivity and trichotomy of the earliest-disagreement order do need hypotheses on the base order, and the two need different ones, so both are collected in one module. Its parameters are trichotomy and transitivity of `R` on the members of `A`, and the smallest-element principle for `R` over those members; in the tower these come from the stage below.

Transitivity is a comparison of two witnesses. If `x` comes before `y` at `p` and `y` comes before `z` at `q`, then `p` and `q` cannot be equal, since `p` belongs to `y` and `q` does not; and whichever of the two is smaller witnesses that `x` comes before `z`. Both branches check the same two things: that the smaller point is on the right side, and that the agreement below it composes.

The module collects the three premises the earliest-disagreement order will inherit. `baseTri` and `baseTrans` say that `R` restricted to members of `A` is trichotomous and transitive, and `baseLeast` is the smallest-element principle over `A`: from a merely inhabited property of members of `A` it returns an element satisfying it that no smaller member of `A` satisfies. Note the shape of the conclusion: it is explicit data, not a truncation, since the caller needs the actual least element.

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

The statement of transitivity takes the two hypotheses exactly as `precedes` produces them: truncated witnesses for `x ≺ y` and for `y ≺ z`, and returns a truncated witness for `x ≺ z`. The proof therefore begins by eliminating the first truncation, then the second, both into a target that is again a truncation and hence a proposition.

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

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

With both witnesses exposed, `both` receives the full data: a point `p` witnessing `x` before `y`, with its membership clauses `agp`, and a point `q` witnessing `y` before `z`, with `agq`. The comparison of the two base points is delegated to the base trichotomy, and the auxiliary `decide` analyses its three outcomes.

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

If `p` is strictly below `q`, it keeps the role of witness for `x` before `z`. Its own clauses carry over unchanged, being about `x` and `y`; what must be verified is that `p` belongs to `z` and that agreement holds below `p` between `x` and `z`. Membership in `z` comes from `agq` at the point `p`, which transports `p`'s membership in `y` across the composite comparison.

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

Agreement below `p` is composed clause by clause. To show `w ∈ x` implies `w ∈ z`: `agp` lifts `w ∈ x` to `w ∈ y`, then `agq` lifts membership in `y` up to `z`, using base transitivity to know that `w` lies below `q` as well. The backward clause is symmetric, running `z` down to `y` and then to `x`. The equality case cannot occur: `p` belongs to `y` while `q` does not, so transporting membership along the path `p ≡ q` yields a contradiction.

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

If instead `q` is strictly below `p`, the roles swap: `q` witnesses `x` before `z`. Its clauses about `y` and `z` carry over, but membership in `x` and agreement must be established. For membership, `agp` read at the point `q` transports membership of `q` in `x` down to membership in `y`, contradicting `q ∉ y`; the auxiliary `q∉x` packages this refutation.

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

Agreement below `q` composes in the mirrored order: membership in `x` is pushed down to `y` by `agp`, using base transitivity with `q ≺ p` to place `w` below `p`, and `agq` then carries it up to `z`; the backward clause descends `z` to `y` first and then to `x`. With both asymmetric cases handled, and equality refuted, transitivity is complete.

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

Trichotomy is where the excluded middle and the smallest-element principle are used. Ask whether the two subsets disagree anywhere in `A`. If they do not, they agree everywhere in `A`; since both stay inside `A`, they already agree everywhere, and extensionality identifies them. If they do, there is an earliest point of disagreement, and one further decision, whether that point belongs to the first subset, says which way the comparison goes. Agreement below the point holds automatically in both branches: nothing below it disagrees, by the choice of the point.

The excluded middle is used a second time inside `agree`, to turn "not disagreeing" into "agreeing"; that step is exactly a double negation elimination.

The statement takes the two subsets `x` and `y` of `A` not as certificates of definability but as ordinary sets, together with the hypothesis that each stays inside `A`. The conclusion is a `Tri`, the three-way disjunction used throughout this chapter: `x` before `y`, equal as sets, or `y` before `x`. The proof begins by asking excluded middle about `Some`, and `Some` will be built as a proposition, namely a truncated existence statement, so `lem` may be fed `PT.squash₁` as its propositionhood certificate.

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

Two truncations organise the question. The predicate `Apart w` says, merely, that `w` distinguishes the two subsets, in either direction: it belongs to one and not the other. The truncated type `Some` says, merely, that some member of `A` is apart. Both are wrapped with `PT.squash₁`, so both are propositions rather than data; that is exactly what licenses deciding them by excluded middle, and later, eliminating a refutation of `Some` into contradiction.

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

The helper `agree` converts absence of disagreement into agreement, one direction at a time. Its hypothesis `na` refutes `Apart w`, and its conclusion is the two inclusion clauses of membership equivalence at `w`. The conversion from a negative statement to the required membership implication is a double-negation-elimination step.

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

For the forward clause, suppose `w ∈ˢ x` and ask excluded middle about `w ∈ˢ y`. If it holds, we are done. If its refutation `nh` is produced, then `w` is apart after all, witnessed by the left disjunct `wx , nh`; packaging that witness into the truncation and handing it to `na` yields a contradiction, from which `Empty.rec` produces any desired element, here the missing membership proof. The target `Empty.⊥` is a proposition, so eliminating the truncated `Apart w` into it is legitimate.

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

The backward clause is the mirror image. Assuming `w ∈ˢ y`, excluded middle decides `w ∈ˢ x`; a refutation would make `w` apart through the right disjunct `nh , wy`, and `na` refutes that. Together the two clauses say: if no point of difference exists at `w`, membership in `x` and membership in `y` coincide at `w`.

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

Now suppose `Some` is refuted, so no member of `A` is apart. The helper `nApart` packages this as a pointwise refutation of `Apart`, and `same` will use it at every `w` to prove the sets equal. The premise that the refuted witness lies in `A` is discharged next, and the membership equivalence of `agree` then applies at each point.

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

An apart point always lies in `A`, provided the two subsets do. Indeed, the truncated disjunction `ha` is eliminated into the proposition `w ∈ˢ A`: if the left disjunct holds, `w` belongs to `x`, and `x⊆` moves it into `A`; if the right holds, `y⊆` does the same. Note the direction of the elimination: into a proposition-valued membership, which is exactly what propositional truncation permits.

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

At each `w`, the two clauses of `agree w (nApart w)` assert membership in `x` if and only if membership in `y`. The combinator `⇔toPath` promotes this iff between the two propositions `w ∈ˢ x` and `w ∈ˢ y` to a path between them as types, which is the form extensionality for the cumulative hierarchy consumes. Feeding the pointwise paths to `extensionalV` yields the path `x ≡ y`, so the `eq` branch of the trichotomy is closed.

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

In the other branch, `Some` holds: some member of `A` is apart. The smallest-element principle `baseLeast`, available for the base order `R` on the members of `A`, is applied to the predicate `Apart`, and it returns an explicit record `found`, not a truncated existence: a point `m` in `A`, apart, with nothing apart below it in the `R` order. This explicitness is what lets the least apart point be used as a witness later.

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

The components of `found` are unpacked once and named: the point `m`, its membership `m∈A` in `A`, the apartness `apartM`, and the leastness `belowM`. Giving each a name keeps the two symmetric branches below readable, since each will cite several of these fields.

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

The leastness field `belowM` refutes any apart point strictly below `m`; its argument order is rearranged here to put the comparison hypothesis last, which suits the coming uses. With the least apart point in hand, excluded middle decides whether `m` belongs to `x`, and `side` turns each answer into a branch of the trichotomy.

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

If `m` does belong to `x`, then `m` witnesses that `y` comes before `x`: it lies in the second set and not the first. The sublemma `m∉y` refutes `m ∈ˢ y` by case analysis on the truncated `apartM`: in the left disjunct the witness itself carries a refutation of `m ∈ˢ y`, and in the right disjunct the refutation of `m ∈ˢ x` clashes with `mx`. Eliminating the truncation is allowed because the target `Empty.⊥` is a proposition.

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

Agreement below `m` also swaps sides for free. For each `w` below `m`, `belowM` refutes `Apart w`, so `agree w` applies and gives membership equivalence in both directions; the pair is merely written in the reversed order, producing `Agrees R A y x m` from an agreement originally oriented from `x` to `y`. Together with `m∈A`, `mx` and `m∉y`, this is a complete `Witness` that `y` precedes `x`, delivered inside the truncation by `gt`.

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

The mirrored branch assumes instead that `m` does not belong to `x`, and produces the `lt` witness that `x` precedes `y`. Extracting `m ∈ˢ y` from `apartM` is another truncated case analysis: the left disjunct would assert `m ∈ˢ x`, refuted by `nmx`, so only the right disjunct survives and it carries the membership outright. Agreement below `m` needs no reversal this time, since the witness is oriented from `x` to `y` exactly as `agree` produces it. With both symmetric branches in place, the trichotomy of `precedes` is complete, and the local order on a stage is a linear order on its members, pending well-foundedness.

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

## The finite stages

Recursion over numerals carries both a tally and an earliest-disagreement
well-order from each finite stage to the next.

The stages indexed by numerals are the finite ones, and the order on each is
built by recursion: stage zero is empty, and the order on the stage after `n` is
comparison at the earliest disagreement over stage `n`, with stage `n`'s own
order as the base. `before-irrefl` holds at every stage and needs no induction,
since irreflexivity of the comparison needed no hypothesis and stage zero carries
no comparison at all.

The definition begins with a small piece of plumbing for the three-way judgment. `Tri-map` acts on a `Tri` by applying one function in each alternative; the three clauses are its computation rules. It will convert the trichotomy proved about two sets into the trichotomy needed about two points of a stage, which differ only by carrying membership proofs.

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

The stages indexed by numerals are named: `finiteStage n` is the stage `Lset (# n)`. The relation `before` is then a recursion on the index. At zero it is the falsity truth value, so no pair is ever related. At a successor it is `precedes` applied to the previous stage: the base set over which membership is compared is the stage `n` itself, and the base order along which the earliest disagreement is sought is `before n`, the order the recursion built one step down.

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

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

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

Irreflexivity of `before` holds at every numeral, and its proof does no induction. At zero the hypothesis is a proof of falsity, which `Empty.rec*` eliminates. At a successor it is exactly `precedes-irrefl`, the hypothesis-free irreflexivity established when the comparison was defined. This is why irreflexivity is not one of the data the recursion has to carry.

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

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

The base case's emptiness is recorded separately as `zero-empty`: no set is a member of the stage zero. Reading a membership certificate out of `Lset (# zero)` produces, merely, some stage `δ` with `δ` a member of the numeral zero and `x` a definable subset of `Lset δ`; the numeral zero has no members, and `∅-empty` turns any alleged member into a contradiction. The elimination of the truncation is legitimate because the target `Empty.⊥` is a proposition.

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

What the recursion has to carry is a tally, trichotomy and transitivity, and
nothing else: irreflexivity holds automatically at every stage, and
well-foundedness is derived where it is used rather than transported.
A point of a stage is a set together with its membership, which is a
proposition, so two points are equal as soon as their sets are; that is all the
work involved in passing between the statements about sets and the bundle, whose
carrier must be a type.

The search machinery of the earlier section works over a type, so a member of a stage is packaged as a `Point`: a set together with its membership certificate in `finiteStage n`. The relation `Below` reads `before n` at the underlying sets. Since membership is a proposition, two points with the same set are already equal; this one fact does all the work of moving between statements about sets and statements about points.

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

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

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

The induction at stage `n` retains exactly the facts needed for the successor: a tally of `finiteStage n`, trichotomy of `before n` for members of that stage, and transitivity of `before n` on arbitrary sets. Irreflexivity follows uniformly from earliest disagreement, while well-foundedness is recovered from the tally whenever the local order is used.

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

Inside `Ordered`, the first task is trichotomy about points. `triPoint` applies `Tri-map` to the trichotomy `tri` about sets; the middle component, where the conclusion is a path, needs converting, and `Σ≡Prop` supplies exactly that: a path between the underlying sets extends to a path between the points, because the second components are proofs of a proposition.

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

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

The tally is lifted from sets to points by pairing each entry with its own membership proof, giving `points`. The coverage statement `covers` is then `onto` transported through this pairing: given a point, `onto` merely provides an index whose entry has the same set, and `Σ≡Prop` upgrades the equality of sets to an equality of points. Coverage remains truncated, as it was for the tally itself.

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

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

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

For points of the stage, trichotomy, irreflexivity and transitivity combine with the finite tally to give two consequences. Finite search yields a least point satisfying any merely inhabited predicate, and the same least-counterexample argument yields well-foundedness of the point relation.

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

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

  order : SWO (Point n)
```

These facts determine a strict well-order on the points of `finiteStage n`: the relation is `Before n`, its three order laws come from the stage comparison, and its well-foundedness comes from finite search. The construction therefore separates the local comparison from the finiteness argument that rules out infinite descent.

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

The last lemma packages least elements in the shape the next stage needs. `leastMem` takes a predicate `P` on sets that is merely satisfied by some member of the stage, and returns an explicit member `m` satisfying `P`, together with leastness in the `before n` order: no member `b` of the stage satisfying `P` lies strictly below `m`. Nothing here is truncated except the hypothesis.

```agda
    ; wf∙    = wellFounded }

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

The proof runs the search at the point level and unpacks the result. `least` is applied to the lifted predicate and the repackaged truncated witness, returning an explicit pair: a point `m` and its `Least` certificate. The three components of the point and the two of the certificate are then reassembled into the set-level statement, with the leastness clause composed by applying the certificate to the pair `b , b∈`.

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

Only the glue remains visible: `Q` reads the set-level predicate at the underlying set of a point, and `found` invokes `least` with the truncated hypothesis repackaged from a triple into a pair of a point and a proof. This `leastMem` is exactly what the recursion feeds to `Difference` as `baseLeast` at the successor stage, closing the loop between the search machinery and the earliest-disagreement order.

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

The recursion starts with the empty tally and vacuous order laws at stage zero. At a successor, the previous tally is lifted across the definable power set. Earliest disagreement supplies trichotomy from the two subset hypotheses and supplies transitivity directly from the preceding stage's order; the successor-stage identity is used only where membership must be moved between the stage and that definable power set.

The base case assembles a record whose three fields are the three small facts just displayed. The tally `empty` has size zero: the index type `Fin zero` is empty, so the entry and membership fields are given by the absurd pattern, functions from no possible arguments. There is nothing to list at stage zero, and that is the whole content of the tally.

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

The remaining fields of the zero-stage tally have the same source. Its membership certificate for any listed item is impossible because there is no index, while coverage of the stage follows from `zero-empty`: a supposed member of `finiteStage zero` yields a contradiction. Thus `empty` really enumerates the empty stage in both directions.

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

The two order fields are vacuous. Trichotomy at zero receives membership certificates for `x` and `y`, but no such certificates exist, so `zero-empty` extracts a contradiction from the first and discharges the goal. Transitivity at zero receives a hypothesis of type `before zero x y`, which by the computation rule of `before` is the falsity truth value, and `Empty.rec*` eliminates it. Empty premises make empty conclusions; no property of the empty order is used beyond its being empty.

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

The successor step needs three mathematical inputs from stage `n`: its least-element principle, the trichotomy and transitivity of `before n`, and a tally of its members. The first two make earliest disagreement a strict comparison on subsets of that stage, while the tally enumerates those subsets through Boolean masks. Together they provide exactly the tally and order laws required at stage `suc n`.

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

The identification `step` is the path `Lset-suc (# n)`, stating that the stage after `n` is the definable power set of stage `n`. The new tally `raised` keeps the size and the items of the power tally, so it enumerates the same definable subsets; what changes is only where the membership certificates are read, which is where `step` enters.

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

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

The `inside` field transports each membership certificate from the definable power set to the successor stage along the reverse of `step`, since the certificate proves membership in the power set but the tally claims membership in `Lset (# suc n)`. Symmetrically, `onto` takes a membership certificate in the successor stage and transports it forward along `step` before calling the power tally's coverage. In both directions the transport acts on a membership statement and nothing else.

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

The auxiliary `members` extracts the inclusion hypothesis that `precedes-tri` asks for. A definable subset of stage `n` has all of its members in stage `n`; this is `𝒟ₒ∋⊆`, read backwards from a membership in the definable power set. The transport along `step` moves the certificate for `x` into the power set first, and what results is a function: for every member `w` of `x`, a certificate that `w` lies in stage `n`.

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

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

Both successor fields are now one-line applications. `triSuc` is `Diff.precedes-tri` with the two inclusion hypotheses supplied by `members`, since `before (suc n)` is by definition `precedes (before n) (finiteStage n)`. `transSuc` is `Diff.precedes-trans` verbatim, its hypotheses already having the right shape. The recursion closes: each stage's order facts are the previous stage's, consumed by the earliest-disagreement theory.

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

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

## The limit stage

Every member of `Lset ω` receives its least finite level; comparing levels
first and the local stage order second gives the limit-stage well-order.

A member of `Lset ω` appears at some numeral-indexed finite stage. Among its stages of appearance, natural-number least-element search gives a smallest one, called its **level**. Natural-number well-foundedness is used again later to organize descent between different levels.

The limit's members are packaged as `Limit`, a set together with a membership certificate in `Lset ω`. The lemma `inSome` converts such a certificate into a truncated statement that the set appears at some finite stage. Reading the certificate out of the limit stage produces, merely, some `δ` in `ω` with the set a definable subset of `Lset δ`; the outer elimination is into a truncated type, which is a proposition, so it is legitimate.

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

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

It remains to identify the index `δ` below `ω`. Membership `δ ∈ ω` is the truncated assertion that `δ` equals a numeral `# (lower k)` for some lifted natural number `k`. After opening that truncated numeral witness with `PT.map`, the path rewrites the definable-subset certificate for `𝒟ₒ (Lset δ)` to one over `Lset (# lower k)`; `Lset-suc` then places `x` in `finiteStage (suc (lower k))`. This proves appearance at a finite stage without confusing the index `ω` with the stage `Lset ω`.

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

With the numeral named, `named` produces the actual stage of appearance. Since `Lset-suc` identifies `Lset (# (suc k))` with the definable power set of `Lset (# k)`, the certificate that the set is a definable subset of `Lset (# (lower k))` transports, along `sym (Lset-suc ...)`, into a membership in `finiteStage (suc (lower k))`. So the numeral indexing the stage of appearance is one more than the numeral appearing inside `ω`, which is the familiar off-by-one between an index and its successor stage.

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

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

`levelData` is where the truncated existence meets the least-element theorem. It applies `leastOf` for the natural-number order and excluded middle to the predicate `m ↦ a .fst ∈ˢ finiteStage m` and the truncated witness `inSome`, returning an explicit numeral together with `IsLeast` data: the stage at that numeral contains the set, and no smaller numeral has that property. The level is therefore the least stage of appearance, not an arbitrary stage selected from the truncation.

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

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

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

The two projections have convenient names: `level a` is the least numeral at which the underlying set appears, and `level-in a` is the membership certificate at that stage. Everything the limit order needs about a member's floor is now available as data, and the next section builds the order out of exactly these two ingredients.

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

The order on the limit takes the level as the primary key: a member of a lower level comes first, and two members of the same level are compared by that level's own order. The equation between levels is carried in the second alternative, and carried in the direction that lets the second member be read at the first's level, which is what keeps the definition free of any transport.

Irreflexivity and transitivity are case analyses on that alternative, with the level equations moving the stage-order facts to the level where they are needed. Trichotomy compares levels first and defers to the stage only when they agree.

The relation `a ≺ b` is a disjoint sum of two ways to come first. The left alternative says `a`'s level is strictly smaller; the right alternative says the levels coincide and, inside stage `level a`, the underlying sets stand in that stage's own `before` order. The `Lift` on the left raises the natural-number comparison from `Type ℓ-zero` to `Type (ℓ-suc ℓ)`, the universe where the right alternative already lives, so both branches share one type. Reading the relation is lexicographic: level decides unless it ties, and only a tie consults the stage.

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

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

Irreflexivity disposes of each branch with the corresponding fact about the ingredients: a strict inequality `level a < level a` is refused by `¬m<m`, and a witness of `before (level a)` against `a` itself is refused by `before-irrefl`, which held at every stage without induction. Transitivity then splits by which branch each hypothesis uses. When both steps descend in level, `<-trans` composes the two inequalities; when only one step does, the equality of levels in the other hypothesis is used with `subst` to move the one strict inequality to the right endpoint, still yielding the left branch.

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

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

When both hypotheses use their equal-level branches, `q : level b ≡ level a` comes from `a ≺ b` and `p : level c ≡ level b` comes from `b ≺ c`. Their composite `p ∙ q : level c ≡ level a` is the equation required for `a ≺ c`. The stage-order fact `hbc` is stated at `level b`; transport along `q` moves it to `level a`, where it composes with `hab` by StageOrder.trans.

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

The transport in `moved` moves `hbc` along the equation `q`, changing only the stage at which the `before` statement is made, from `level b` to `level a`. At that point both witnesses live in one stage: `hab` says `a`'s set precedes `b`'s there, and `moved` says `b`'s precedes `c`'s, so `StageOrder.trans` at stage `level a` joins them into `joined`, the witness that `a` precedes `c` inside its own level. This finishes transitivity; trichotomy is stated next and is decided by comparing the two levels outright.

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

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

Trichotomy first decides `level a ≟ level b`. Unequal levels immediately give the corresponding strict branch. In the equality case the decision supplies `p : level a ≡ level b`; transporting `level-in b` along `sym p` places `b` in `finiteStage (level a)`, so StageOrder.tri can compare both underlying sets in that one stage.

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

The local trichotomy is repackaged into the limit relation with the equality in the required direction. A local result `a before b` returns the right branch of `a ≺ b` with `sym p : level b ≡ level a`; a local result `b before a` returns the right branch of `b ≺ a` with `p`, transporting the before-proof to stage `level b`. Equality of underlying sets lifts to equality in `Limit` because its membership component is propositional.

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

Repackaging splits by the stage's verdict. If `a`'s set precedes `b`'s, the result is the right branch of `≺`, fed with the equation `sym p` in exactly the direction the definition asks for. If the sets are equal, `Σ≡Prop` promotes that to a path between the pairs `a` and `b`, legitimate because the second component of `Limit` is a proposition; this is the `eq` case. If `b`'s set precedes `a`'s, the `before` fact is transported along `p` to the level where it is stated, and the result is the right branch with the arguments reversed. No case here needed anything beyond the ingredients already built.

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

Well-foundedness is two nested inductions, and they are kept apart on purpose. The outer one is induction on the level, in the library's packaged form, and it hands down a hypothesis covering every lower level. The inner one is an ordinary descent along the accessibility that the finite stage already has, which is legitimate precisely because that stage is finite. A step down in level appeals to the outer hypothesis; a step within a level appeals to the inner one; and since the inner function recurses on nothing but its own accessibility argument, the two never have to be compared.

Fix a target `b` at level `k` and a point `u` of stage `k` with the same underlying set. The inner argument turns accessibility of `u` for the local relation `Below k` into accessibility of `b` for the limit relation. After unfolding `Acc`, an arbitrary predecessor is named `c`. If `c` has lower level, the outer induction hypothesis applies; if it has the same level, it becomes a local predecessor of `u` and the inner accessibility proof applies.

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

Discharging `step` splits by the branch of the hypothesis `c ≺ b`. In the left branch, `c` has strictly smaller level than `b`, hence than `k`; the inequality is moved under the equation `q` with `subst`, and then `ih` applies at level `level c`, exactly the cross-level case. In the right branch, `c` shares `b`'s level, so both live inside stage `k`, and the descent is handed to the inner accessibility: `ru` is the function that the `acc` constructor of `u`'s accessibility provides, and it is applied to the point `pc` corresponding to `c` and to the proof that `pc` is below `u`.

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

The right branch needs its bookkeeping made explicit. First `qc` composes the two level equations, `sym qb` with `q`, to certify that `level c ≡ k`; this is what lets `c` be seen at stage `k` at all. Then `pc` packages `c`'s underlying set with its membership in stage `k`, the membership being obtained by transporting `level-in c` along `qc`. A `Point k` is a set together with such a certificate, so this one construction moves the argument from the limit back into the finite stage where the inner order lives.

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

In the equal-level case, every predecessor `b` of `u` lies in the same finite stage `k` and is below `u` in that stage order. The equalities carried by the case merely align both endpoints with this fixed `k`; the accessibility of `u` for `Below k` then supplies accessibility of `b`. Thus the inner recursion descends only inside one finite-stage order.

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

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

The outer induction is well-founded induction on the natural-number level. Its hypothesis handles every predecessor whose level is strictly smaller than `k`; the inner accessibility argument handles predecessors that remain at level `k`. These two cases form the lexicographic proof and require no compatibility assumption between the orders on different finite stages.

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

The body of `outer` reduces its goal to the inner lemma. It first forms `here`, the point of stage `k` corresponding to `b`, built exactly like `pc` above; then `Ordered.wellFounded k (stageOrder k) here` supplies the accessibility of that point inside stage `k`'s order, and `accInside` takes it from there, with the remaining two arguments being the level equation `q` and the reflexive identification of `b`'s set with `here`'s. The final statement `limit-wf` says every member of the limit is accessible, obtained by instantiating the level induction at `level a` with the trivial equation `refl`.

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

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

limitOrder : SWO Limit
```

Consequently `≺` is a strict well-order on `Limit`: it is trichotomous, irreflexive and transitive, and the two-level induction proves it well-founded. Elements from different first-appearance levels are ordered by level; only equal-level elements are compared by a single finite-stage order.

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

Thus `limitOrder` is a strict well-order on the members of `Lset ω`: levels are the primary key, and elements with the same least level are compared by that finite stage’s order. Its least-element operation can therefore select from any merely inhabited proposition-valued family on the limit stage.

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

## Recap

Finite tallies climb through definable powersets, support the well-founded earliest-disagreement order at every numeral stage, and culminate in `limitOrder` on `Lset ω`.

`Tally` is all the finiteness this chapter owns: a finite family that hits every member, with no injectivity and no decidable equality asked for. `PowerStep.powerTally` carries one up to the definable power set, by enumerating the bit vectors over the tally and observing that every subset of a tallied stage is definable; `stageOrder` then runs that step along the numerals, so every finite stage has a tally.

`precedes` compares two subsets at the earliest point where they disagree. It is irreflexive for free, transitive by comparing two witnesses, and trichotomous by the excluded middle together with the base's smallest elements. Well-foundedness does not follow from the definition of the comparison alone. Here it comes from the tally through `Search`; the descending-chain example on subsets of the natural numbers shows why the finite-stage hypothesis matters.

`limitOrder` is a strict well-order on the members of `Lset ω`, with the level as the primary key and each finite stage's own order inside a level. It is the interface the axiom of choice will take: with it, `leastOf` picks a member out of any inhabited property of members of the limit stage, and picks the same one every time.