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.

{-# 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.

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.

  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.

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.

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.

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.

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.

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.

    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.

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.

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.

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.

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.

maskCount : ℕ → ℕ
maskCount zero    = 
maskCount (suc n) = maskCount n + maskCount n

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

maskCons 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.

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.

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.

     ∙ 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.

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.

  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.

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.

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.

       → Σ[ 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.

  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.

  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.

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.

  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.

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.

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.

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.

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.

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.

  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.

  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.

  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.

    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.

      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.

    (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.

    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.

  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.

      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.

                 (λ 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.

      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.

               (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.

    ; 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.

    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.

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.

  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.

  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.

            → (⟨ 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.

      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.

      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.

      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.

    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.

    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.

    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.

  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.

      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.

          (λ { (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.

        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.

    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.

        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.

        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.

          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.

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.

  ⟨ 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.

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.

                 × ((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.

    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.

      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.

        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.

      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.

        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.

  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.

    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.

    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.

      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.

      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.

        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.

      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.

      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.

    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.

      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.

      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.

      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.

        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.

        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.

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.

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.

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.

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.

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.

  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.

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.

    (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.

    (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.

  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.

    ; 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∈.

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