---
title: "Canonical names for successor-stage members"
module: L.Choice.CanonicalNames
lang: en
site: "Bedrock"
description: "Canonical names for successor-stage members"
stage: "The canonical well-order and Choice"
reading_order: 75
canonical: https://bedrock.institute/en/L.Choice.CanonicalNames.html
html: L.Choice.CanonicalNames.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/CanonicalNames.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.ConstantOccurrences, FOL.Manipulation.ParameterAbstraction, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Definability, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Choice.FiniteStageOrders, L.WellOrder.Base]
routes: [canonical-order]
translations: [https://bedrock.institute/zh/L.Choice.CanonicalNames.md, https://bedrock.institute/ja/L.Choice.CanonicalNames.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Canonical names for successor-stage members

A member of a successor stage is determined by a formula and finitely many parameters from the preceding stage. This chapter packages that data as a name, proves that every member has one, and orders all names so that a least representative can be chosen.

A member of a successor stage is a definable subset of the stage below, and the earlier chapters said what that means twice over: once in `L.Definability`, as a formula with parameters drawn from that stage, and once in `FOL.Manipulation.ParameterAbstraction`, after the parameters leave the syntax, as a **parameter-free formula together with a vector of parameters**. The second form is the one that can be compared. Its formula is a finite piece of syntax, so its code is a hereditarily finite set and has already appeared at the limit stage `Lset ω`, which `L.Choice.FiniteStageOrders` well-orders; its parameters are members of the stage below, which the surrounding construction has well-ordered by the time it calls this one. A **name** is that pair, with the arity between them, and this chapter builds it, shows every member of the successor stage has one, and well-orders the names.

The order is a three-key lexicographic comparison, written out. Nothing here is an instance of a general order on dependent sums, and that is deliberate: such a thing would have to carry a family of orders indexed by the first key and prove its four laws in that generality, which is a larger theorem than the one wanted, for a single use. The three keys are named, and each is compared by an order that already exists.

The explicit classical input is `lem : LEM (ℓ-suc ℓ)`. It supplies the finite-stage limit order used for formula codes and the least-element search used at the end. Keeping it as a module parameter records the common strength required by both constructions; the intervening coding, abstraction, lexicographic laws, and accessibility arguments add no further axiom.

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

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

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

The vocabulary a name is written in comes from the first-order language of set theory. A formula here carries a domain of constant symbols together with a fixed number of free-variable slots, and the constructors cover membership, equality, the connectives, falsity, and both kinds of quantifiers, with bounded forms listed alongside. This syntax already exists; the chapter only needs to name and compare formulas of a special shape, those whose constant domain is empty.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics
```

Several existing operations on formulas do the real work of turning a definition with constants into a name. The coding of terms and formulas as sets supplies the code that will become the first key; the relabelling lemma says that reading a formula under an embedding of constant domains preserves satisfaction; occurrence counting and parameter abstraction together replace constants by fresh variables and a parameter vector. On the side of the universe, the structure `𝒮ᵥ` interprets the language inside `V`, and the pair construction `pr` is what packages code fragments as sets.

```agda
open import FOL.Manipulation.ConstantMapping using ( mapTm; embed )
open import FOL.Manipulation.Relabelling using ( embed-⊨ )
open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo )
open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs₁ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

The constructible side contributes the objects being named. `Lset` is a stage of the constructible hierarchy inside `V`, and `𝒟ₒ` is the definable-powerset operator: it takes a set and returns the set of its subsets definable by a one-variable formula with constants from it. Crucially, `𝒟ₒ` hands back only a truncated witness that such a formula exists, so completeness of naming will inherit that truncation rather than a chosen formula. The module `DefOf` carries the inner satisfaction relation and its smallness facts, which denotation is built from.

```agda
open import V.Coding {ℓ} using ( pr; module VCode )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( Lset; Lset-mono; 𝒟ₒ; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
```

The first key needs a home where an order already reaches it. The numerals of the language, the von Neumann naturals, are ordinals inside `L`, and each numeral sits in the successor of its own stage; pairs of stage members appear two stages later. The limit stage `Lset ω` collects what appears by some finite stage, and `Limit` is a member of it together with a certificate of that membership. On this stage `limitOrder` well-orders everything, and `Tri-map` transports trichotomy verdicts along an equivalence, a tool the last key's trichotomy will reuse.

```agda
open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Axioms.Basic {ℓ} using ( pr∈Lset-suc )
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; inSome; limitOrder; Tri-map )
open import L.WellOrder.Base {ℓ-suc ℓ}
```

The abstract notion of order is a strict well-order packaged as a record: a strict comparison, trichotomy, irreflexivity, transitivity, and well-foundedness, together with a least-element search `leastOf` that consumes such a record. These four laws are exactly what the names will be shown to satisfy. On the type-theoretic side, the imported tools handle the dependent bookkeeping that arises because a name's formula and parameter vector have the arity as an index: a way to build a path into a dependent pair, a commutation of substitution with a constant function along a path, the two directions of an equivalence, and injectivity extracted from an embedding.

```agda
  using ( Tri; lt; eq; gt; SWO; IsLeast; leastOf )

open import Cubical.Foundations.Prelude using ( toPathP )
open import Cubical.Foundations.Transport using ( constSubstCommSlice )
open import Cubical.Foundations.Equiv using ( equivFun; invEq )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
```

Natural numbers supply the arities, and their order supplies the middle key. Its trichotomy here is decidable, so the comparison of names can branch on `arity a ≟ arity b` directly; transitivity and well-foundedness of `_<_` enter the corresponding laws. `⇔toPath` turns a proof of a propositional biconditional into a path, which is how the membership characterization of a denotation will be stated as an equality of propositions rather than two implications, and `toℕ` reads a bounded index as an ordinary numeral.

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Nat using ( _+_; +-comm )
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Data.FinData using ( toℕ )
```

The lexicographic comparison will be written as a sum type: each key's verdict is either strictly below or equal, and after equality the next key decides. So the chapter needs binary sums with their constructors, vectors of parameters with their map, and the well-founded induction toolkit: `Acc` expresses that every strict descent from an element terminates, `acc` packages such a proof, and `WFI` turns it into an induction principle. The vectors here are indexed by their lengths, which is what forces the arity transport questions studied later.

```agda
open import Cubical.Data.Sigma using ( ΣPathP )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Vec using ( map )
open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded; module WFI )
```

Two eliminations have their target types fixed by the mathematics. The empty type's recursor discharges the impossible cases, such as a parameter-free formula containing a constant. Propositional truncation turns a chosen witness into a mere existence claim: `∥ A ∥₁` is inhabited as soon as `A` is, and it may be eliminated only into proposition-valued targets. The hierarchy of cumulative sets contributes `sett`, a set assembled from a small index type, and the embedding `⟪_⟫` that regards a small type's element as a member of the universe.

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

The last group fixes the concrete interpretation the names will be read in. `#` turns a natural number into the corresponding numeral inside the universe, and `ω` is the infinite set, so numeral membership certificates like those in the limit stage can be produced. The direct logical operations on `hProp (ℓ-suc ℓ)` provide the truth values and connectives used here, and opening the `ZFStructure` semantics at the structure `𝒮ᵥ` fixes what a formula means inside `V`. Every satisfaction judgment below is this inner one, and that is what ties a name's denotation to the definable powerset's own notion of definability.

```agda
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_; ω )
```

These final declarations fix the interpretation used throughout the chapter: formulas are read in the set-theoretic structure on `V`, with proposition-valued truth.

```agda
open hPropStructure 𝒮ᵥ
```

## A parameter-free code is hereditarily finite

The first key of a name is the code of its parameter-free formula. Such a finite syntax code is hereditarily finite, so it already belongs to the limit stage where the established well-order can compare it.

The first key wants the formula as a member of `Lset ω`, so the first thing to establish is that its code is one. Read the coding clauses in `V.Coding` and nothing else is used: a numeral for the tag, a numeral for a de Bruijn index, and Kuratowski pairs holding the parts. The one construction that could leave the finite world is the constant clause, which puts an arbitrary set into the code, and a parameter-free formula has no constants at all.

So two closure facts suffice, and both are lifted rather than re-derived: `inSome` of `L.Choice.FiniteStageOrders` says a member of `Lset ω` has appeared by some finite stage, and `pr∈Lset-suc` of `L.Axioms.Basic` says a Kuratowski pair of two members of a stage appears two stages later. Advancing from one finite stage to a later one is monotonicity applied along the successors of the numerals, which is the only recursion here.

A membership certificate for the limit stage is hard to use directly, because it says only that the element is somewhere in the finite stages. The auxiliary predicate `AtStage` records which finite stage: a natural number `k` together with a proof that the element lies in `Lset (# k)`. Once an element is pinned to a stage, `raiseTo` moves the certificate forward, from stage `# k` to stage `# (d + k)`, by recursion on `d`: each successor step observes that a stage contains the numeral bounding it, via `self∈sucV`, and `Lset-mono` turns that into monotonicity of the stages.

```agda
private
  AtStage : S → Type (ℓ-suc ℓ)
  AtStage x = Σ[ k ∈ ℕ ] ⟨ x ∈ˢ Lset (# k) ⟩

  raiseTo : (x : S) (d k : ℕ) → ⟨ x ∈ˢ Lset (# k) ⟩ → ⟨ x ∈ˢ Lset (# (d + k)) ⟩
  raiseTo x zero    k h = h
```

Numerals are the atoms of this argument, so their placement comes first. By `numeral-ord`, `# k` is an ordinal in `L`, and `ord∈Lset-suc` places it in the successor of its own stage. The proof `#∈ω` says that the bounding numeral belongs to `ω`; monotonicity therefore lifts the numeral into the limit stage. The companion closure statement places `pr x y` in the limit whenever both components are there, exactly as the coding of composite syntax requires.

```agda
  raiseTo x (suc d) k h = Lset-mono (self∈sucV (# (d + k))) (raiseTo x d k h)

numeral∈limit : (k : ℕ) → ⟨ (# k) ∈ˢ Lset ω ⟩
numeral∈limit k = Lset-mono (#∈ω (suc k)) (ord∈Lset-suc (# k) (numeral-ord k))

pr∈limit : (x y : S) → ⟨ x ∈ˢ Lset ω ⟩ → ⟨ y ∈ˢ Lset ω ⟩
         → ⟨ pr x y ∈ˢ Lset ω ⟩
```

The proof of the pair statement has one wrinkle: `inSome` delivers its stage witnesses inside a propositional truncation, so the stage numbers cannot be picked out as data. The goal, however, is a membership proposition, and truncated witnesses may be eliminated into a proposition-valued target. The outer `PT.rec` unpacks the witness for `x`, and the inner one the witness for `y`, feeding both into the helper `both`, which does the actual work.

```agda
pr∈limit x y hx hy = PT.rec (snd (pr x y ∈ˢ Lset ω))
  (λ atX → PT.rec (snd (pr x y ∈ˢ Lset ω)) (both atX) (inSome y hy))
  (inSome x hx)
  where
  both : AtStage x → AtStage y → ⟨ pr x y ∈ˢ Lset ω ⟩
```

Given stage numbers `j` for `x` and `k` for `y`, the two elements are raised to the common stage `# (k + j)`, so that `pr∈Lset-suc` applies and puts the pair two stages later, under the numeral `# (suc (suc (k + j)))` that bounds it in `ω`; the summands of the common stage come in opposite orders, and one substitution along `+-comm` repairs that. With numerals and pairs closed under the limit stage, a tagged code, which is just the pair of a numeral and the payload, is closed as well, by `tag∈limit`. These three facts are the whole induction load for the syntax to come.

```agda
  both (j , hj) (k , hk) = Lset-mono (#∈ω (suc (suc (k + j))))
    (pr∈Lset-suc (# (k + j)) x y (raiseTo x k j hj)
      (subst (λ n → ⟨ y ∈ˢ Lset (# n) ⟩) (+-comm j k) (raiseTo y j k hk)))

tag∈limit : (k : ℕ) (x : S) → ⟨ x ∈ˢ Lset ω ⟩ → ⟨ VCode.mkTag k x ∈ˢ Lset ω ⟩
tag∈limit k x h = pr∈limit (# k) x (numeral∈limit k) h
```

With numerals, pairs and tags in place, the placement of every parameter-free code follows by structural induction on the syntax. The induction is short because the three closure facts above carry all the work; the constructor cases only reassemble them, and the constant case, the only one that could escape, is void because the constant domain is the empty type. The tag numbers appear as literals throughout, and nothing about their values is used beyond their being numerals.

Terms are handled first, and their induction is two clauses. A variable has no constant content, so its code is the numeral for its de Bruijn index wrapped in the tag `1`, and `tag∈limit` applies at once. The constant clause of a parameter-free term is a contradiction: the constant domain `⊥*` has no elements, so the impossible case is discharged by the empty type's recursor. The `mapTm` in the statement is the embedding of a parameter-free term into the working syntax, which replaces constants by host values; over `⊥*` it has nothing to replace.

```agda
codeTm∈limit : ∀ {n} (t : Term (⊥* {ℓ}) n)
             → ⟨ VCode.⌜ mapTm Empty.rec* t ⌝ᵗ ∈ˢ Lset ω ⟩
codeTm∈limit (con c) = Empty.rec* c
codeTm∈limit (var i) = tag∈limit 1 (# (toℕ i)) (numeral∈limit (toℕ i))

code∈limit : ∀ {n} (χ : Formula (⊥* {ℓ}) n) → ⟨ VCode.⌜ embed χ ⌝ ∈ˢ Lset ω ⟩
```

Formulas follow the same pattern, with one tag per constructor. Each binary clause pairs the codes of the two immediate subformulas or subterms under a tag, the connective and quantifier clauses wrap a single subcode, and falsity is tag `5` applied to the numeral zero. In every case the result is a `tag∈limit` or `pr∈limit` application to induction hypotheses, so the clause bodies are one line each.

```agda
code∈limit (t ∈̇ u)  = tag∈limit 0 _ (pr∈limit _ _ (codeTm∈limit t) (codeTm∈limit u))
code∈limit (t ≐ u)  = tag∈limit 1 _ (pr∈limit _ _ (codeTm∈limit t) (codeTm∈limit u))
code∈limit (φ ∧̇ ψ)  = tag∈limit 2 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
code∈limit (φ ∨̇ ψ)  = tag∈limit 3 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
code∈limit (φ ⇒̇ ψ)  = tag∈limit 4 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
```

The last four clauses cover the quantifiers and their bounded forms, with tags `6` through `9`; the bounded forms additionally pair in the code of the ranging term. What matters for the chapter is only the end result: every parameter-free formula has a code sitting in the limit stage, ready to be compared by the order that stage already carries. The tag numbering is arbitrary bookkeeping, not part of any mathematical claim.

```agda
code∈limit ⊥̇        = tag∈limit 5 _ (numeral∈limit 0)
code∈limit (∃̇ φ)    = tag∈limit 6 _ (code∈limit φ)
code∈limit (∀̇ φ)    = tag∈limit 7 _ (code∈limit φ)
code∈limit (∀̇∈ t φ) = tag∈limit 8 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ))
code∈limit (∃̇∈ t φ) = tag∈limit 9 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ))
```

A member of the limit stage carries a certificate of membership, so the first key is not the bare code but the code together with that certificate. This subsection packages the two, and records one auxiliary fact about transporting along equalities of arities that the comparison will need.

`limitCode` sends a parameter-free formula to the pair of its code and the membership proof just constructed; this pair is exactly an element of `Limit`, the type the limit-stage order acts on. The second statement concerns a subtlety of dependent syntax: a formula's type mentions its arity, so after two names have been found to have equal arities, one formula must be substituted along that equality before it can even be compared with the other. `code-shift` says this substitution is invisible to the code: transporting a formula of arity `suc i` along a path `i ≡ j` yields a formula with the same code.

```agda
limitCode : ∀ {n} → Formula (⊥* {ℓ}) n → Limit
limitCode χ = VCode.⌜ embed χ ⌝ , code∈limit χ

code-shift : {i j : ℕ} (e : i ≡ j) (χ : Formula (⊥* {ℓ}) (suc i))
           → VCode.⌜ embed (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e χ) ⌝
           ≡ VCode.⌜ embed χ ⌝
```

The proof invokes the general fact that a function whose result type does not depend on the index commutes with substitution in that index. The coding of formulas lands in the fixed type `S` of sets, regardless of the arity the formula lives at, so the transported formula's code equals the original's by `constSubstCommSlice`; the statement is arranged with `sym` so the path reads from the substituted formula back to the original.

```agda
code-shift e χ = sym (constSubstCommSlice
  (λ k → Formula (⊥* {ℓ}) (suc k)) S (λ _ ψ → VCode.⌜ embed ψ ⌝) e χ)
```

## A parameter-free formula is recovered from its image

At a fixed arity, coding does not identify two different parameter-free formulas. Injectivity follows by decoding the hereditarily finite image and then using injectivity of the syntax encoding.

Two names with the same code and the same arity must be built from the same formula, or the comparison would rank two different names as neither below the other and equal to nothing. `V.Coding` proved its own injectivity, but it proved it over the working syntax, whose constant domain is the carrier; what is needed here is injectivity for the parameter-free formulas, which reach that syntax through `embed`.

The gap is closed by an **erasure** running the other way, and the erasure can be crude because it only has to be a left inverse on the parameter-free formulas. A constant is sent to the variable of index zero, which is available because every formula under consideration has at least one free-variable slot, and every other clause is the identity on the constructor. On a formula with no constants the erasure changes nothing, one clause at a time, and injectivity is then three path compositions.

The erasure of a term does the only creative work. A constant, whose value in the working syntax is an arbitrary set, is replaced by the variable of index zero; a variable is left alone. This is legitimate only because the target restricts to formulas of arity `suc n`, so slot zero always exists. The erasure of a formula is then declared homomorphically, taking each constructor to itself with the erasures of the parts.

```agda
private
  eraseTm : ∀ {n} → Term S (suc n) → Term (⊥* {ℓ}) (suc n)
  eraseTm (con x) = var zero
  eraseTm (var i) = var i

  eraseFo : ∀ {n} → Formula S (suc n) → Formula (⊥* {ℓ}) (suc n)
```

The first five clauses cover the atomic and propositional formulas: the two atomic relations erase their term arguments, and the three binary connectives recurse on both subformulas. Nothing happens here beyond distributing the erasure through the constructor; the constant information has already been discarded at the term level.

```agda
  eraseFo (t ∈̇ u)  = eraseTm t ∈̇ eraseTm u
  eraseFo (t ≐ u)  = eraseTm t ≐ eraseTm u
  eraseFo (φ ∧̇ ψ)  = eraseFo φ ∧̇ eraseFo ψ
  eraseFo (φ ∨̇ ψ)  = eraseFo φ ∨̇ eraseFo ψ
  eraseFo (φ ⇒̇ ψ)  = eraseFo φ ⇒̇ eraseFo ψ
```

The remaining five clauses are literally the identity: falsity has no parts, and each quantifier rebuilds itself around the erased body. Every clause is forced; there is no choice in how a formula is erased, which is what makes the left-inverse computation below predictable.

```agda
  eraseFo ⊥̇        = ⊥̇
  eraseFo (∃̇ φ)    = ∃̇ eraseFo φ
  eraseFo (∀̇ φ)    = ∀̇ eraseFo φ
  eraseFo (∀̇∈ t φ) = ∀̇∈ (eraseTm t) (eraseFo φ)
  eraseFo (∃̇∈ t φ) = ∃̇∈ (eraseTm t) (eraseFo φ)
```

The left-inverse property is stated and proved one level at a time. For a term, `eraseTm` after `mapTm Empty.rec*` returns the term itself: the constant case is void because a parameter-free term has no constants, and the variable case is `refl`, since both composites rebuild the same variable. The formula-level statement then claims that erasing the embedding of a parameter-free formula gives back that formula, up to a path.

```agda
  eraseTm-embed : ∀ {n} (t : Term (⊥* {ℓ}) (suc n))
                → eraseTm (mapTm Empty.rec* t) ≡ t
  eraseTm-embed (con c) = Empty.rec* c
  eraseTm-embed (var i) = refl

  eraseFo-embed : ∀ {n} (χ : Formula (⊥* {ℓ}) (suc n)) → eraseFo (embed χ) ≡ χ
```

The proof proceeds by induction on the formula, reusing the term-level fact wherever a term occurs. Atomic and binary-connective clauses apply a binary congruence `cong₂` to the two recursive results, building the path for the composite from the paths for the parts.

```agda
  eraseFo-embed (t ∈̇ u)  = cong₂ _∈̇_ (eraseTm-embed t) (eraseTm-embed u)
  eraseFo-embed (t ≐ u)  = cong₂ _≐_ (eraseTm-embed t) (eraseTm-embed u)
  eraseFo-embed (φ ∧̇ ψ)  = cong₂ _∧̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
  eraseFo-embed (φ ∨̇ ψ)  = cong₂ _∨̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
  eraseFo-embed (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
```

Falsity needs only `refl`, since nothing was embedded into it, and the four quantifier clauses apply a unary congruence, or `cong₂` where the bounded form also carries a term. With this, every parameter-free formula has an explicit path from its erased image back to itself.

```agda
  eraseFo-embed ⊥̇        = refl
  eraseFo-embed (∃̇ φ)    = cong ∃̇_ (eraseFo-embed φ)
  eraseFo-embed (∀̇ φ)    = cong ∀̇_ (eraseFo-embed φ)
  eraseFo-embed (∀̇∈ t φ) = cong₂ ∀̇∈ (eraseTm-embed t) (eraseFo-embed φ)
  eraseFo-embed (∃̇∈ t φ) = cong₂ ∃̇∈ (eraseTm-embed t) (eraseFo-embed φ)
```

Injectivity is now one sentence. Suppose two parameter-free formulas at the same arity have equal embedded codes. The coding's own injectivity turns that into an equality of the embedded formulas; erasing both sides keeps the equality, because erasure is a function; and the left-inverse paths reduce each side to the original formula. The composite path is the desired `χ ≡ ψ`, so distinct parameter-free formulas of one fixed arity cannot have equal codes.

```agda
code-inj : ∀ {n} (χ ψ : Formula (⊥* {ℓ}) (suc n))
         → VCode.⌜ embed χ ⌝ ≡ VCode.⌜ embed ψ ⌝ → χ ≡ ψ
code-inj χ ψ e = sym (eraseFo-embed χ)
               ∙ cong eraseFo (VCode.⌜⌝-inj (embed χ) (embed ψ) e)
               ∙ eraseFo-embed ψ
```

## The naming data

A name records an arity, a parameter-free formula with one output variable, and a parameter vector of that arity. Its denotation is the subset of the stage cut out by the formula under that environment.

Everything in the rest of the chapter is relative to one set `A`, the stage the names are written over, and to one strict well-order of that stage's members, so the work proceeds inside a module `Naming A w`. A **name** is an arity, a parameter-free formula with one more free-variable slot than that, and a vector of that many parameters drawn from `A`'s small member type. The extra slot is the one a subset is carved by; the rest receive the parameters, and the first key is read off the formula at once.

The module takes the stage `A` and, crucially, a strict well-order of its members as parameters, since the third key will compare parameters by that order and nothing in this chapter constructs one over an arbitrary stage. The type `Name` is a dependent triple: a natural number `k`, a parameter-free formula with `suc k` free-variable slots, and a vector of `k` members of `A`'s carrier. The vector's length is forced to be the arity, so a name cannot pair a formula with the wrong number of parameters.

```agda
module Naming (A : S) (w : SWO ⟪ A ⟫) where
  module DA = DefOf A
  open DA using ( _⊨ᵐ_ )

  Name : Type ℓ
  Name = Σ[ k ∈ ℕ ] (Formula (⊥* {ℓ}) (suc k) × Vec ⟪ A ⟫ k)
```

The projections name the three keys' sources: `arity` returns the number, `formula` the embedded-free formula of exactly one more variable slot, and `params` the vector. Their types are dependent on the name itself, so `formula a` lives at arity `suc (arity a)` and `params a` at `arity a`; this dependence is the source of every transport question in the comparison to come.

```agda
  arity : Name → ℕ
  arity a = a .fst

  formula : (a : Name) → Formula (⊥* {ℓ}) (suc (arity a))
  formula a = a .snd .fst

  params : (a : Name) → Vec ⟪ A ⟫ (arity a)
```

The first key is a projection as well: `codeOf` applies `limitCode` to the formula, delivering its code in the limit stage together with the membership certificate, ready for `limitOrder` to compare.

```agda
  params a = a .snd .snd

  codeOf : Name → Limit
  codeOf a = limitCode (formula a)
```

What a name denotes is the subset of `A` its formula selects when the parameters are supplied in the **environment**, in the order expected by parameter abstraction. The environment is one member followed by the parameters, all read into the restricted carrier by the definable powerset's own constant interpretation, and the satisfaction is the inner one, so the denotation is a subset of `A` carved by exactly the notion `Def A` was defined by. Smallness is inherited: the inner satisfaction at any formula and any environment is small, so the subset is a `sett` over a small index type with no resizing spent.

A subset of `A` carved by a predicate is presented directly: `subsetOf` takes a family of propositions over `A`'s small member type and builds a `sett` whose index type is the dependent pair of a member `m` and a proof that the predicate holds at `m`, sent to the set `⟪ A ⟫↪ m`. An index is therefore a witness together with its certificate, and membership in the resulting set asks only that such a pair *merely* exists. This is the same shape `defSet` was built in, so predicates phrased in either form present the same kind of object.

```agda
  private
    module SemM = FOL.Semantics DA.𝒮M
    open SemM using ( _^_ )

    subsetOf : (⟪ A ⟫ → hProp ℓ) → S
    subsetOf P = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ P m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))
```

Two presentation details matter before the denotation itself. The auxiliary `⟪⟫↪-inj` records that the map `⟪ A ⟫↪` is an embedding, so a path between two of its values comes from a path between the underlying indices; this recovers `m' ≡ m` and will close the forward direction of the membership specification. The environment is then assembled: for a member `m` marking the free variable, it is `DA.ι m` followed by the parameters each decoded by `DA.ι`. The head entry fills the one extra slot that carves the subset, the tail entries fill the parameter slots, and the length of the environment is definitionally `suc (arity a)`, exactly the arity of the name's formula.

```agda
    ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
    ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

  environment : (a : Name) → ⟪ A ⟫ → DA.SM ^ (suc (arity a))
  environment a m = DA.ι m ∷ map DA.ι (params a)

  satAt : (a : Name) → ⟪ A ⟫ → hProp ℓ
```

The predicate that defines a name's denotation is `satAt a m`, the small proposition equivalent to the inner satisfaction of the embedded formula at the assembled environment. Taking it through `subsetOf` gives `denote a` as a set of the hierarchy, a subset of `A` selected by exactly the inner semantics. No new sizing decision is made anywhere: smallness enters once through `⊨ᵐ-small` and is spent on the `sett`'s index type.

```agda
  satAt a m = DA.⊨ᵐ-small (embed (formula a)) (environment a m) .fst

  denote : Name → S
  denote a = subsetOf (satAt a)
```

The specification says the word "denotes" literally: a member of `A` belongs to the denotation exactly when the inner world satisfies the name's formula at the environment the name prescribes. The compression to a small proposition was only an encoding, and the equivalence carries it back.

The theorem is a path of propositions, matching the form in which `defSet-mem` was stated, and it is proved by `⇔toPath` from two implications. The auxiliary `decode` re-expands `satAt a m` into the full pair that `⊨ᵐ-small` returns, so that both directions can use the equivalence in its second component, the one connecting the small proposition to the inner satisfaction statement.

```agda
  denote-mem : (a : Name) (m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ denote a) ≡ (environment a m ⊨ᵐ embed (formula a))
  denote-mem a m = ⇔toPath fwd bwd
    where
    decode = DA.⊨ᵐ-small (embed (formula a)) (environment a m)
```

Membership in a `sett` only *merely* supplies its index, so the forward direction eliminates a truncation into a proposition and obtains an index `(m' , h)` together with a path `q` from `⟪ A ⟫↪ m'` to `⟪ A ⟫↪ m`. Embedding injectivity turns `q` into `m' ≡ m`, transporting `h` along it yields a proof of `satAt a m`, and the equivalence of `decode` converts that proof into the satisfaction statement. Every step spends a proof where only a proposition is wanted, so no witness is chosen.

```agda
    fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩ → ⟨ environment a m ⊨ᵐ embed (formula a) ⟩
    fwd = PT.rec (snd (environment a m ⊨ᵐ embed (formula a)))
      (λ { ((m' , h) , q) →
        invEq (decode .snd) (subst (λ v → ⟨ satAt a v ⟩) (⟪⟫↪-inj q) h) })
    bwd : ⟨ environment a m ⊨ᵐ embed (formula a) ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩
```

The reverse direction runs the same equivalence the other way: a satisfaction proof becomes a proof of `satAt a m`, taken as the index `(m , proof)` with the trivial path, and truncated with `∣_∣₁`. Together the two directions identify membership with inner satisfaction without remainder, which is what the word "denotes" was required to mean.

```agda
    bwd h = ∣ (m , equivFun (decode .snd) h) , refl ∣₁
```

## Every member of the successor stage has a name

The definable-power-set specification supplies a formula with constants for each successor-stage member. Abstracting those constants produces the parameter-free formula and parameter vector that form its name.

A member of `𝒟ₒ A` is, by that operator's own specification, merely a subset definable by a formula of one free variable with constants from `A`; and parameter abstraction turns such a formula into a parameter-free one of higher arity together with its list of occurring constants. Reading the second off the first is the whole of naming, and it is a function.

The function `nameOf` assembles the three keys at once. `countFo φ` counts each constant occurrence, giving the arity, so the abstraction `absFo φ` lives at `1 + countFo φ` free slots, which is `suc` of the arity; `constantsFo φ` lists the constants in the same order, a vector of exactly that length in `⟪ A ⟫`. Note that `nameOf` takes a formula with constants, not yet a name's parameter-free component: the abstraction happens inside the definition, one clause per constructor.

```agda
  nameOf : Formula ⟪ A ⟫ 1 → Name
  nameOf φ = countFo φ , (absFo φ , constantsFo φ)
```

Adequacy follows from the parameter-abstraction theorem `⊨-abs₁`, after identifying the two interpretations of the empty constant domain. Two readings of a parameter-free formula are in play and they have to be identified first: the name's denotation reads it inside the constant domain `⟪ A ⟫`, through `embed`, while the abstraction theorem reads it at the empty constant domain. The two interpretations are functions out of the empty type, so they agree, and stating this agreement is the only verification the identification requires.

The abstraction theorem `⊨-abs₁` speaks of satisfaction over the empty constant domain, while the name's semantics reads over `⟪ A ⟫`. To compare the two statements term by term, `emptySat` fixes the shape of a satisfaction statement at an arbitrary constant interpretation `f : ⊥* → DA.SM`, so that changing `f` is a matter of applying a function to a function. The formula itself never mentions a constant, which is what makes this uniformity available.

```agda
  private
    emptySat : (f : ⊥* {ℓ} → DA.SM) {n : ℕ}
             → DA.SM ^ n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
    emptySat f γ χ = γ ⊨ᶠ χ
      where open SemM.At (⊥* {ℓ}) f using () renaming ( _⊨_ to _⊨ᶠ_ )
```

Two constant interpretations of a parameter-free formula both have type `⊥* → DA.SM`: the one the working semantics uses, sending every constant to `DA.ι (Empty.rec* b)`, and the eliminator `Empty.rec*` itself. Since `⊥*` has no elements, `funExt` plus the eliminator proves the two functions equal as `sameReading`, without inspecting anything. The statement `absSat` then compares the environment reading used by the denotation, through `embed`, with the empty-domain reading used by the abstraction theorem, at the same member `m` and the same abstracted formula.

```agda
    sameReading : (λ (b : ⊥* {ℓ}) → DA.ι (Empty.rec* b)) ≡ Empty.rec*
    sameReading = funExt (λ b → Empty.rec* b)

    absSat : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
           → (environment (nameOf φ) m ⊨ᵐ embed (formula (nameOf φ)))
           ≡ ((DA.ι m ∷ []) ⊨ᵐ φ)
```

The proof is a three-step path. The relabelling lemma `embed-⊨` says that embedding a parameter-free formula into a richer constant domain does not change what it says, which moves the left side to the `Empty.rec*`-marked reading; `sameReading` then substitutes the denotation's own reading for that one; and `⊨-abs₁`, read backwards, is exactly the abstraction theorem's identification of the abstracted formula's satisfaction with the original one at the single parameter. Each step is a theorem from an earlier chapter, connected rather than re-derived.

```agda
    absSat φ m =
        embed-⊨ DA.𝒮M DA.ι (absFo φ)
          (environment (nameOf φ) m)
      ∙ cong (λ f → emptySat f (environment (nameOf φ) m) (absFo φ)) sameReading
      ∙ sym (⊨-abs₁ DA.𝒮M DA.ι φ (DA.ι m))
```

With the two readings identified as propositions, `satAt-abs` lifts the identification from satisfaction statements to the small propositions the sets are built from. It compares `satAt (nameOf φ) m`, the small proposition behind the name's denotation, with `DA.smallSat φ m`, the small proposition behind `defSet φ`. The two auxiliary names `big` and `small` unpack the corresponding `⊨ᵐ-small` pairs, so each direction can use both of the packaged equivalences.

```agda
    satAt-abs : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
              → satAt (nameOf φ) m ≡ DA.smallSat φ m
    satAt-abs φ m = ⇔toPath fwd bwd
      where
      big = DA.⊨ᵐ-small (embed (formula (nameOf φ))) (environment (nameOf φ) m)
```

The forward direction composes three conversions, all applied to proofs: run the big equivalence backwards to reach the embedded satisfaction statement, transport the proof along the path `absSat φ m` to the empty-domain statement, then run the small equivalence forwards to reach `DA.smallSat φ m`. The path `absSat φ m` identifies the two satisfaction types, so ordinary transport moves a proof in the required direction. Their propositionhood is used to package each satisfaction type as an `hProp`; transport itself only requires the path.

```agda
      small = DA.⊨ᵐ-small φ (DA.ι m ∷ [])
      fwd : ⟨ satAt (nameOf φ) m ⟩ → ⟨ DA.smallSat φ m ⟩
      fwd h = equivFun (small .snd) (subst ⟨_⟩ (absSat φ m) (invEq (big .snd) h))
      bwd : ⟨ DA.smallSat φ m ⟩ → ⟨ satAt (nameOf φ) m ⟩
      bwd h = equivFun (big .snd)
```

The backward direction is the same composition with the path reversed: `sym (absSat φ m)` moves proofs the other way, and the two equivalences are applied in the opposite order. Nothing new is proved here; the point is that `satAt (nameOf φ) m` and `DA.smallSat φ m` are the same small proposition for every `m`, which is what makes the two sets equal in the next step.

```agda
        (subst ⟨_⟩ (sym (absSat φ m)) (invEq (small .snd) h))
```

Both subsets are cut out of `A` by a small predicate on its members, so once the two predicates are equal the two sets are equal by a congruence, with no appeal to extensionality. Completeness follows by transporting along that equality, and it is stated truncated because that is how the definable powerset yields a formula in the first place.

The equality `denote-defSet` is the predicate agreement `satAt-abs` made into an equality of sets: `funExt` gathers the pointwise equalities into an equality of predicate families, and `cong subsetOf` carries it to the presented sets. Completeness then takes the certificate `h : ⟨ x ∈ˢ 𝒟ₒ A ⟩` and inverts it with `𝒟ₒ-inv`, which merely supplies a formula `φ` with `defSet φ ≡ x`; the conclusion is correspondingly a truncated existence of a name and an equality, not a chosen name.

```agda
  denote-defSet : (φ : Formula ⟪ A ⟫ 1) → denote (nameOf φ) ≡ DA.defSet φ
  denote-defSet φ = cong subsetOf (funExt (satAt-abs φ))

  names-complete : (x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
                 → ∥ Σ[ a ∈ Name ] (denote a ≡ x) ∥₁
  names-complete x h = PT.map named (𝒟ₒ-inv A x h)
```

Inside the truncation, the step from the inverted data to the desired pair is ordinary: the formula `φ` is named by `nameOf φ`, and the required equality is `denote-defSet φ ∙ q`, the path from the name's denotation to `defSet φ` followed by the given path to `x`. Since the target `∥ Σ[ a ∈ Name ] (denote a ≡ x) ∥₁` is a proposition, `PT.map` may work under the truncation, mapping the merely supplied formula to a merely supplied name without ever inspecting which one it is.

```agda
    where
    named : Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DA.defSet φ ≡ x)
          → Σ[ a ∈ Name ] (denote a ≡ x)
    named (φ , q) = nameOf φ , (denote-defSet φ ∙ q)
```

## The order on the parameter vectors

Parameter vectors are compared lexicographically by the given well-order on members of `A`. The relation accepts two possibly different lengths: an exhausted vector has no predecessor in either mixed-length case, while two nonempty vectors compare their heads and continue to their tails only when the heads agree. This formulation makes transitivity available for three vectors at their actual lengths. Trichotomy is later invoked only after an arity path transports one vector to the other length.

Two well-orders are in play and both are fixed once with short names. The limit-stage order `limitOrder` compares formula codes and becomes `_≺_`; the module parameter `w`, the well-order of `A`'s members, compares parameters and becomes `_≺ₚ_`. Each opening also renames the trichotomy, irreflexivity, transitivity and well-foundedness laws, so the proofs to come can invoke either order's laws without long qualified names.

```agda
  open SWO limitOrder using () renaming
    ( _<∙_ to _≺_ ; tri∙ to ≺-tri ; irr∙ to ≺-irr
    ; trans∙ to ≺-trans ; wf∙ to ≺-wf )
  open SWO w using () renaming
    ( _<∙_ to _≺ₚ_ ; tri∙ to ≺ₚ-tri ; irr∙ to ≺ₚ-irr
```

The comparison itself is defined by pattern matching on both vectors, indexed by their lengths `j` and `k`. Whenever either vector is empty, no descent is possible, and the result type is the empty type: there is nothing below an exhausted vector at any position. These cases cost nothing, and the fact that they are refutable is what the transitivity and irreflexivity proofs will consume.

```agda
    ; trans∙ to ≺ₚ-trans ; wf∙ to ≺ₚ-wf )

  infix 20 _≺ᵥ_
  _≺ᵥ_ : ∀ {j k} → Vec ⟪ A ⟫ j → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ)
  []      ≺ᵥ []      = ⊥*
  []      ≺ᵥ (y ∷ q) = ⊥*
```

Two nonempty vectors are compared at their heads: either the head `x` drops below `y` in the parameter order, or the heads are equal as a path and the descent continues into the tails. The strict case is a left summand and the equal-head case a right one, so later proofs can branch on which position first decided. Note that the head equality is a path `x ≡ y`, which the mixed transitivity cases will substitute into comparisons.

```agda
  (x ∷ p) ≺ᵥ []      = ⊥*
  (x ∷ p) ≺ᵥ (y ∷ q) = (x ≺ₚ y) ⊎ ((x ≡ y) × (p ≺ᵥ q))
```

Three of the four laws are immediate inductions. Irreflexivity and trichotomy ask for equal lengths, since only there is a vector equal to another at all; transitivity does not, and gets three vectors of three lengths, with every case but the all-inhabited one refuted by the empty type.

Irreflexivity is proved by induction on the vector: a vector can never be below itself. The statement makes sense only at a single length, since `p ≺ᵥ p` requires the two occurrences to have the same length, and the induction consumes the statement at the tail, one length down. The transitivity statement follows, stated for three lengths at once.

```agda
  ≺ᵥ-irr : ∀ {k} (p : Vec ⟪ A ⟫ k) → p ≺ᵥ p → Empty.⊥
  ≺ᵥ-irr []      h             = Empty.rec* h
  ≺ᵥ-irr (x ∷ p) (inl h)       = ≺ₚ-irr x h
  ≺ᵥ-irr (x ∷ p) (inr (_ , h)) = ≺ᵥ-irr p h

  ≺ᵥ-trans : ∀ {i j k} (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ j) (r : Vec ⟪ A ⟫ k)
```

Transitivity is proved by simultaneous case analysis on the three vectors. If the first descent starts at an exhausted vector, its comparison type is already the empty type, and the same holds when the middle vector is exhausted; if the third is exhausted, the second comparison is refutable. In every such case the proof is the empty type's eliminator, with no mathematical content of its own.

```agda
           → p ≺ᵥ q → q ≺ᵥ r → p ≺ᵥ r
  ≺ᵥ-trans []      []      r       h k = Empty.rec* h
  ≺ᵥ-trans []      (y ∷ q) r       h k = Empty.rec* h
  ≺ᵥ-trans (x ∷ p) []      r       h k = Empty.rec* h
  ≺ᵥ-trans (x ∷ p) (y ∷ q) []      h k = Empty.rec* k
```

When all three vectors are inhabited, the comparison reads off the heads, and the first two mixed cases are the interesting ones. If `x` is below `y` while `y` equals `z`, substituting the path into the first comparison yields `x` below `z`; and symmetrically, an equality `x ≡ y` followed by `y` below `z` transports the second comparison backwards along the path. Both are instances of the same move: a path of elements acts on comparisons by transport.

```agda
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inl k) = inl (≺ₚ-trans x y z h k)
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inr (e , k)) =
    inl (subst (λ v → x ≺ₚ v) e h)
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inl k) =
    inl (subst (λ v → v ≺ₚ z) (sym e) k)
```

The last transitivity case keeps both heads where they are: the two paths concatenate into `x ≡ z` and the recursion descends into the tails, at whatever three lengths they carry. With transitivity done, trichotomy is stated for two vectors of one length, since only there can the two names coincide at all; the empty vectors are equal by `refl`.

```agda
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inr (e' , k)) =
    inr (e ∙ e' , ≺ᵥ-trans p q r h k)

  ≺ᵥ-tri : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Tri (p ≺ᵥ q) (p ≡ q) (q ≺ᵥ p)
  ≺ᵥ-tri []      []      = eq refl
  ≺ᵥ-tri (x ∷ p) (y ∷ q) = decide (≺ₚ-tri x y)
```

For inhabited vectors the heads are compared by the parameter order's trichotomy, and the helper `decide` transports the verdict from heads to vectors. A strict verdict either way becomes a left summand: the head decided, the tails never enter. The equal case is the only one that must consult the tails, and it is taken up next.

```agda
    where
    decide : Tri (x ≺ₚ y) (x ≡ y) (y ≺ₚ x)
           → Tri ((x ∷ p) ≺ᵥ (y ∷ q)) ((x ∷ p) ≡ (y ∷ q)) ((y ∷ q) ≺ᵥ (x ∷ p))
    decide (lt h) = lt (inl h)
    decide (gt h) = gt (inl h)
```

When the heads are equal by a path `e`, the vector comparison reduces to the tails', and `Tri-map` relabels the three outcomes. A tail strictly below becomes the right summand `e , h`; tail equality, under `cong₂ _∷_`, becomes equality of the whole vectors; and the mirrored verdict attaches `sym e`. The recursion is structural in the tails, closing the induction.

```agda
    decide (eq e) =
      Tri-map (λ h → inr (e , h)) (cong₂ _∷_ e) (λ h → inr (sym e , h))
        (≺ᵥ-tri p q)
```

Well-foundedness is the one that needs a plan. Descending from a vector, the head either drops in the given order, and then the tail is replaced by an arbitrary one of the same length, or the head stays and the tail drops. So the descent is two nested inductions: the given order's well-foundedness for the head, and the tail's accessibility for the tail, with the arbitrary tails supplied by the statement one length down. That third ingredient is why the whole thing recurses on the length as well, and why the head's induction is taken as an induction principle rather than as a second recursive argument: with all three appetites served in one recursion the descent has no single decreasing measure to offer.

The helper `consAcc` lifts accessibility from length `k` to length `suc k`: assuming every vector of length `k` is accessible, it builds accessibility for `y ∷ q`. Its input `prev` is exactly the statement at the previous length, which is what allows the strict case to replace the tail with an arbitrary `r` of the same length. The proof then runs the given order's well-founded induction on the head, so the head's descent is the engine and the tail's accessibility is consumed inside.

```agda
  private
    consAcc : (k : ℕ) → ((r : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) r)
            → (y : ⟪ A ⟫) (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q
            → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q)
    consAcc k prev = WFI.induction ≺ₚ-wf onHead
```

The induction hypothesis `ih` is stated carefully: for every `z` strictly below `y`, accessibility of `z ∷ q` holds for *every* tail `q` of length `k`, given the tail's own accessibility. The universal quantification over `q` is what makes the strict case work without recursion on the vector being examined, and it is available precisely because `≺ₚ-wf` was applied as an induction principle rather than invoked recursively.

```agda
      where
      onHead : (y : ⟪ A ⟫)
             → ((z : ⟪ A ⟫) → z ≺ₚ y → (q : Vec ⟪ A ⟫ k)
                  → Acc (_≺ᵥ_ {k} {k}) q → Acc (_≺ᵥ_ {suc k} {suc k}) (z ∷ q))
             → (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q
```

Accessibility is constructed data: `acc` pairs an element with a function taking every strictly-below element to its own accessibility. So the goal for `y ∷ q` is produced by `acc`, applied to a step function that must handle the two shapes a strict descent from `y ∷ q` can take, and the remainder of the proof is the body of that step.

```agda
             → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q)
      onHead y ih q (acc rq) = acc step
        where
        step : (r : Vec ⟪ A ⟫ (suc k)) → r ≺ᵥ (y ∷ q)
             → Acc (_≺ᵥ_ {suc k} {suc k}) r
```

The strict case has a head `z` below `y` and an arbitrary tail `r`, and here the induction hypothesis does all the work: it supplies `Acc` for `z ∷ r` from `z ≺ₚ y` and `prev r`, the accessibility of `r` at length `k`. The equal case keeps the head: the path identifies `z` with `y`, so transporting the accessibility of `y ∷ r` backwards along `sym e` produces accessibility of `z ∷ r`. This transport along a head path is the price of comparing across lengths, and it is paid once here.

```agda
        step (z ∷ r) (inl h)       = ih z h r (prev r)
        step (z ∷ r) (inr (e , h)) =
          subst (λ v → Acc (_≺ᵥ_ {suc k} {suc k}) (v ∷ r)) (sym e)
            (onHead y ih r (rq r h))

  ≺ᵥ-wf : (k : ℕ) (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p
```

The main theorem is induction on the length. The empty vector's accessibility is immediate, since its only would-be predecessor is the empty vector itself and that comparison is the empty type. For `x ∷ p`, `consAcc` is applied with `≺ᵥ-wf k` supplying the statement at the previous length for arbitrary tails, and `≺ᵥ-wf k p` supplying the accessibility of this vector's own tail; both come from one structural recursion on `k`.

```agda
  ≺ᵥ-wf zero    []      = acc (λ { [] h → Empty.rec* h })
  ≺ᵥ-wf (suc k) (x ∷ p) = consAcc k (≺ᵥ-wf k) x p (≺ᵥ-wf k p)
```

One derived fact travels with the comparison and is proved by path induction: moving a vector along an equality of lengths does not change what it is below or above. The two places that need it are the trichotomy and the descent, both of which meet two vectors whose lengths are equal but not identical.

The left lemma states that the comparison `subst (Vec ⟪ A ⟫) e p ≺ᵥ q` is a path to `p ≺ᵥ q`: transporting the compared vector along the length equality `e` leaves the comparison proposition unchanged. The proof does not unfold the vector cases at all. The general lemma `constSubstCommSlice` says that transporting along `e` commutes with a family of types that does not use the index, and the comparison against the fixed `q` is exactly such a family; the `sym` puts the equation in the direction the later proofs need.

```agda
  private
    ≺ᵥ-subst-left : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ k)
                  → (subst (Vec ⟪ A ⟫) e p ≺ᵥ q) ≡ (p ≺ᵥ q)
    ≺ᵥ-subst-left e p q = sym (constSubstCommSlice
      (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → v ≺ᵥ q) e p)
```

The right lemma is the mirror image: moving the *other* vector along its own length equality does not change what is below it. Both directions are needed because the name comparison transports parameters of the first name to the second's length in the `lt` case and in the opposite direction in the `gt` case, and later the well-foundedness proof moves either side. Stated once, in both orientations, no proof afterwards has to reason about `subst` on vectors.

```agda
    ≺ᵥ-subst-right : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i)
                   → (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q)
    ≺ᵥ-subst-right e p q = sym (constSubstCommSlice
      (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)
```

## Three keys, in order

Names are ordered lexicographically by formula code, arity, and parameter vector. The comparison is written as three explicit cases, so its trichotomy and transitivity follow one key at a time.

The comparison is a family of types read off from the definition. Its outer summand is strict comparison of formula codes under the limit order: if one name's code drops below the other's, the codes decide and nothing else is consulted. Its right summand carries the path `codeOf b ≡ codeOf a`, the equality of codes that licenses moving on to the next key, and packages it with the second key's comparison, strict inequality of natural-number arities.

```agda
  infix 20 _≺ₙ_
  _≺ₙ_ : Name → Name → Type (ℓ-suc ℓ)
  a ≺ₙ b = (codeOf a ≺ codeOf b)
         ⊎ ( (codeOf b ≡ codeOf a)
           × ( (arity a < arity b)
```

The innermost summand completes the descent: under equal codes and equal arities, carried again as paths `arity b ≡ arity a`, the parameter vectors are compared by `_≺ᵥ_`. Each level of nesting is therefore a pair of an equality of the previous key with the strict comparison of the next, which is exactly the shape the four laws' case analyses will follow, key by key.

```agda
             ⊎ ((arity b ≡ arity a) × (params a ≺ᵥ params b)) ) )
```

Irreflexivity and transitivity are then the three keys' own laws, sorted by case. The mixed cases of transitivity substitute an equality of one key into the other's comparison, and that is all the verification required; the parameter case appeals to the vector comparison at three lengths, which is why that one was proved across lengths.

A name can never be strictly below itself, and the three clauses say why: whichever summand witnesses `a ≺ₙ a` would witness a strict descent in one of the three keys from a key to itself. The code case contradicts the limit order's irreflexivity, the arity case is a natural number strictly below itself, refuted by `¬m<m`, and the parameter case contradicts vector irreflexivity at `params a`'s own length.

```agda
  ≺ₙ-irr : (a : Name) → a ≺ₙ a → Empty.⊥
  ≺ₙ-irr a (inl h)                 = ≺-irr (codeOf a) h
  ≺ₙ-irr a (inr (_ , inl h))       = ¬m<m h
  ≺ₙ-irr a (inr (_ , inr (_ , h))) = ≺ᵥ-irr (params a) h

  ≺ₙ-trans : (a b c : Name) → a ≺ₙ b → b ≺ₙ c → a ≺ₙ c
```

Transitivity is stated for three names and proved by case analysis on where the two comparisons decided. When both decided at the codes, the limit order's transitivity applies directly. The first mixed case has `a` strictly below `b` at the codes while the second comparison carries `codeOf c ≡ codeOf b`; substituting that equality backwards puts `codeOf a` below `codeOf c`, and the symmetric case is the same substitution read forwards. Each mixed case is one transport, nothing more.

```agda
  ≺ₙ-trans a b c (inl h) (inl k) =
    inl (≺-trans (codeOf a) (codeOf b) (codeOf c) h k)
  ≺ₙ-trans a b c (inl h) (inr (q , _)) =
    inl (subst (λ v → codeOf a ≺ v) (sym q) h)
  ≺ₙ-trans a b c (inr (q , _)) (inl k) =
```

The cases decided at the arity key reuse the same pattern with natural numbers. Two strict arity inequalities compose by `<-trans`; a strict one beside an equality of arities is transported into a strict inequality with the appropriate endpoint substituted. Note the direction of the carried paths: the comparison records `codeOf b ≡ codeOf a` and `arity b ≡ arity a`, equality stated at the larger name, so the concatenations and substitutions run against that orientation.

```agda
    inl (subst (λ v → v ≺ codeOf c) q k)
  ≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inl k)) =
    inr (q' ∙ q , inl (<-trans h k))
  ≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inr (e , _))) =
    inr (q' ∙ q , inl (subst (λ j → arity a < j) (sym e) h))
```

The final case is where all three keys agreed up to the parameters, and here the third key's transitivity at three possibly distinct lengths is exactly what is needed: `≺ᵥ-trans` takes `params a ≺ᵥ params b` and `params b ≺ᵥ params c` at whatever lengths those vectors carry and returns `params a ≺ᵥ params c`. The two arity paths concatenate to `arity a ≡ arity c`, completing the right summand with all three components.

```agda
  ≺ₙ-trans a b c (inr (q , inr (e , _))) (inr (q' , inl k)) =
    inr (q' ∙ q , inl (subst (λ j → j < arity c) e k))
  ≺ₙ-trans a b c (inr (q , inr (e , h))) (inr (q' , inr (e' , k))) =
    inr (q' ∙ q , inr (e' ∙ e , ≺ᵥ-trans (params a) (params b) (params c) h k))
```

Trichotomy is the third law, and it is the one that reads the comparison off rather than combines the other laws. The proof descends the keys in order: if the codes already decide, the verdict is given immediately; if the codes agree, the arities decide; if the arities agree too, the parameter vectors decide. Only this last stage needs care. Equal arities are connected by a path, not identified, so `params a` and `params b` live at different lengths; the vector comparison can only run after the first is transported to the second's length, and the strict verdicts it returns must be transported back before they count as comparisons of the original names. In the equality case something more is required: the two names must be presented as equal dependent triples, so the formulas themselves must agree, and that is exactly what injectivity of the code gives, since `code-shift` says transporting along the arity path leaves the code unchanged and the code verdict says the codes already agree.

The statement is a `Tri`, a three-way verdict carrying either a proof of `a ≺ₙ b`, a path `a ≡ b`, or a proof of `b ≺ₙ a`. The proof hands the whole question to the code order: `≺-tri` already returns such a verdict for the two codes, and a local helper `byCodes` converts a verdict at the codes into one at the names. The helper is introduced by type first, so the shape of the conversion is visible before its clauses.

```agda
  ≺ₙ-tri : (a b : Name) → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
  ≺ₙ-tri a b = byCodes (≺-tri (codeOf a) (codeOf b))
    where
    byCodes : Tri (codeOf a ≺ codeOf b) (codeOf a ≡ codeOf b) (codeOf b ≺ codeOf a)
            → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
```

The strict cases are immediate: a strict comparison of codes is the left summand of the name order, whichever way it points. The equality case opens the second key, delegating to `byArities`, which does for the arities what `byCodes` did for the codes.

```agda
    byCodes (lt h) = lt (inl h)
    byCodes (gt h) = gt (inl h)
    byCodes (eq ec) = byArities (arity a ≟ arity b)
      where
      byArities : NatOrder.Trichotomy (arity a) (arity b)
```

Here the verdicts take the right summand, and they carry the code equality itself. Note the orientation: the comparison records `codeOf b ≡ codeOf a`, equality stated at the larger name, so the strict case below needs `sym ec` while the dual case needs `ec` as written. When the arities are also equal, `≺ᵥ-tri` compares vectors; but `params a` sits at length `arity a` and `params b` at `arity b`, so the first vector is transported along the arity path `e` before the comparison runs.

```agda
                → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
      byArities (NatOrder.lt h) = lt (inr (sym ec , inl h))
      byArities (NatOrder.gt h) = gt (inr (ec , inl h))
      byArities (NatOrder.eq e) =
        byParams (≺ᵥ-tri (subst (Vec ⟪ A ⟫) e (params a)) (params b))
```

The transported vector is given a name, `shifted`, so the statements below stay readable at their real lengths. The equality case will need more than the vectors: to conclude `a ≡ b` outright, the formulas must agree as well, and `sameFormula` states this at the transported formula, whose type is that of the formula of a name with arity `arity b`. Without such an equality the two names could agree in both decided keys and in parameters yet still differ in syntax.

```agda
        where
        shifted : Vec ⟪ A ⟫ (arity b)
        shifted = subst (Vec ⟪ A ⟫) e (params a)

        sameFormula : subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a)
                    ≡ formula b
```

Why the formulas agree: transporting `formula a` along `e` does not change its code, by `code-shift`, and the first component of `ec` says the code of `formula a` equals the code of `formula b`. Concatenating gives equal codes, and `code-inj` turns equal codes back into equal parameter-free formulas. This is the same injectivity proved earlier in the chapter, here doing the work its statement anticipated. With `shifted` and `sameFormula` in hand, `byParams` converts a vector verdict into a verdict at the names.

```agda
        sameFormula =
          code-inj (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a))
            (formula b)
            (code-shift e (formula a) ∙ cong fst ec)

        byParams : Tri (shifted ≺ᵥ params b) (shifted ≡ params b)
```

The strict verdicts were obtained at the transported lengths, so their statements must be moved back. `≺ᵥ-subst-left` says that comparing `subst (Vec ⟪ A ⟫) e p` against `q` is the same proposition as comparing `p` against `q`; transporting `h` along that equality turns a comparison of `shifted` into one of `params a`. Each verdict also carries the code and arity equalities, oriented as the sum requires. The dual case is symmetric, using `≺ᵥ-subst-right` on the other side of the comparison.

```agda
                       (params b ≺ᵥ shifted)
                 → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
        byParams (lt h) = lt (inr (sym ec , inr (sym e ,
          transport (≺ᵥ-subst-left e (params a) (params b)) h)))
        byParams (gt h) = gt (inr (ec , inr (e ,
```

The equality verdict is a path between two elements of `Name`, which is itself a triple. `ΣPathP` pairs the arity path `e` with paths between the remaining components: `toPathP sameFormula` lifts the formula equality across the type family `Formula (⊥*) (suc k)`, and `toPathP ep` does the same for the vector equality. This is where `sameFormula` earns its place: with both decided keys equal and the parameters equal, it is only the formula equality that is still missing, and once supplied the two names are identical as data.

```agda
          transport (≺ᵥ-subst-right e (params b) (params a)) h)))
        byParams (eq ep) =
          eq (ΣPathP (e , ΣPathP (toPathP sameFormula , toPathP ep)))
```

## Descending the three keys

Well-foundedness follows by nested descent, one layer per key. Innermost, the code and the arity are fixed and the parameters descend, with the vector's accessibility as the decreasing argument; in the middle layer, the code is fixed and the arity descends; outermost, the code descends. Each layer is a separate function taking the outer layers' induction hypotheses as arguments, so each recurses on exactly one accessibility proof and the recursion is structural throughout. Everything is stated at names themselves, together with equations saying where each key sits; that is the same discipline the trichotomy observed, since a statement at a name's projections would have to be matched against one at the name.

The innermost layer is a function whose telescope records the whole descent picture at once. It is given: a fixed code `c`; the outer induction hypothesis `ihC`, covering every name whose code drops below `c`; a bound `k`; the middle induction hypothesis `ihK`, covering names with code `c` and arity below `k`; a parameter vector `p` with its own vector accessibility; and the name `a` under study, with three equations: `qc` pins its code at `c`, `ek` pins its arity at `k`, and `qp` identifies its transported parameters with `p`. The conclusion is simply that `a` is accessible.

```agda
  private
    accAtParam : (c : Limit)
               → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
               → (k : ℕ)
               → ((b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b)
```

The type of the vector accessibility parameter is stated at the single length `k`, matching `p`; this is why the parameters were transported into `p`'s length by the equation `qp` rather than compared in place. Accessibility of `a` is supplied as the constructor `acc` together with a step function: to prove every name is accessible, it suffices, for each `a`, to exhibit a function that takes any `b` below `a` and returns `b`'s accessibility.

```agda
               → (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p
               → (a : Name) → codeOf a ≡ c → (ek : arity a ≡ k)
               → subst (Vec ⟪ A ⟫) ek (params a) ≡ p
               → Acc _≺ₙ_ a
    accAtParam c ihC k ihK p (acc rp) a qc ek qp = acc step
```

The step function splits on which key decided `b ≺ₙ a`. If the code dropped, `qc` transports `codeOf b ≺ codeOf a` into `codeOf b ≺ c`, and the outer induction hypothesis finishes. If the arity decided, this predecessor judgment carries `q : codeOf a ≡ codeOf b`; hence `sym q ∙ qc : codeOf b ≡ c`. Transporting `arity b < arity a` along `ek : arity a ≡ k` gives `arity b < k`, so the middle induction hypothesis applies.

```agda
      where
      step : (b : Name) → b ≺ₙ a → Acc _≺ₙ_ b
      step b (inl h)           = ihC b (subst (λ v → codeOf b ≺ v) qc h)
      step b (inr (q , inl h)) = ihK b (sym q ∙ qc) (subst (λ j → arity b < j) ek h)
      step b (inr (q , inr (e , h))) =
```

The remaining case is the parameter key, and it is the only case that recurses in the innermost layer. For a predecessor judgment `b ≺ₙ a`, this branch supplies `e : arity a ≡ arity b`, while `ek : arity a ≡ k` pins the current name to the fixed arity. Thus `eb = sym e ∙ ek` has type `arity b ≡ k`; transporting `params b` along it produces `pb`, the predecessor vector at the fixed length. The code equation is aligned independently as `sym q ∙ qc`.

```agda
        accAtParam c ihC k ihK pb (rp pb hb) b (sym q ∙ qc) eb refl
        where
        eb : arity b ≡ k
        eb = sym e ∙ ek
        pb : Vec ⟪ A ⟫ k
```

The strict comparison `h` was made between `params b` and `params a` at their own lengths, while the accessibility being consumed belongs to `p`. Two moves close the gap: `≺ᵥ-subst-left` and `≺ᵥ-subst-right` say that transporting a vector along an equality of lengths does not change what it is below, so `h` is first rewritten into a comparison at the bound length; then `qp` transports the right endpoint from `params a` to `p`, giving `hb : pb ≺ᵥ p`. The recursive call feeds `hb` into `rp`, the accessibility of `p`, and `b` is returned accessible.

```agda
        pb = subst (Vec ⟪ A ⟫) eb (params b)
        hb : pb ≺ᵥ p
        hb = subst (λ v → pb ≺ᵥ v) qp
          (transport (sym (≺ᵥ-subst-right ek pb (params a)))
            (transport (sym (≺ᵥ-subst-left eb (params b) (params a))) h))
```

The middle layer fixes a code and descends through arities. Its telescope is shorter: the code induction hypothesis `ihC`, a bound `k` with its own accessibility in the natural-number order, and the name with its code pinned at `c` and its arity at `k`. What replaced the vector accessibility is the natural-number accessibility `rk`, since the arity key descends in ℕ.

```agda
    accAtArity : (c : Limit)
               → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
               → (k : ℕ) → Acc _<_ k
               → (a : Name) → codeOf a ≡ c → arity a ≡ k → Acc _≺ₙ_ a
    accAtArity c ihC k (acc rk) a qc ek =
```

The body hands everything to the innermost layer: the parameters are transported to `k`, and their vector accessibility is supplied outright by `≺ᵥ-wf`, which holds for every vector at every length and asks for no recursion here. The only genuine induction is on arities: the local `ihK` unwraps the natural-number accessibility `rk`, so a name with code `c` and strictly smaller arity is handled by a recursive call at that smaller bound. This is the layer where a strictly smaller arity, of any name at all, becomes a smaller bound.

```agda
      accAtParam c ihC k ihK (subst (Vec ⟪ A ⟫) ek (params a))
        (≺ᵥ-wf k (subst (Vec ⟪ A ⟫) ek (params a))) a qc ek refl
      where
      ihK : (b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b
      ihK b q h = accAtArity c ihC (arity b) (rk (arity b) h) b q refl
```

The outer layer descends through codes and needs no equation for the arity at all. Given accessibility of a code `c` and a name whose code is `c`, it invokes the middle layer at the bound `arity a`, supplying the natural-number accessibility that holds unconditionally. The local `ihC` unwraps the code accessibility: a name with strictly smaller code gets a recursive call at its own code. This mirrors the middle layer exactly, one level further out.

```agda
    accAtCode : (c : Limit) → Acc _≺_ c → (a : Name) → codeOf a ≡ c → Acc _≺ₙ_ a
    accAtCode c (acc rc) a qc =
      accAtArity c ihC (arity a) (<-wellfounded (arity a)) a qc refl
      where
      ihC : (b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b
```

The final theorem is a one-line composition of the three layers. Given a name `a`, the code order's own well-foundedness provides accessibility of `codeOf a`, and the outer layer converts that into accessibility of `a`, with the code equation holding by reflection. Every name is thus accessible under the three-key comparison, which is the well-foundedness law of a strict well-order.

```agda
      ihC b h = accAtCode (codeOf b) (rc (codeOf b) h) b refl

  ≺ₙ-wf : WellFounded _≺ₙ_
  ≺ₙ-wf a = accAtCode (codeOf a) (≺-wf (codeOf a)) a refl
```

## The bundle, and the least name

The four laws say that the names carry a strict well-order, and packaging them into that structure's record is what lets the general least-element search consume them. Applied to this order, the search turns a merely inhabited family of names into a definite least member: this is precisely the purpose for which the names were built, since a family of sets over one stage becomes a family of names, and a family of names has a least member.

The record `nameOrder` collects the four laws already proved, field by field: the comparison itself, the trichotomy, irreflexivity, transitivity, and well-foundedness. Nothing new is proved here; the point of the bundle is that downstream constructions can consume a strict well-order without knowing how this one was assembled.

```agda
  nameOrder : SWO (Name)
  nameOrder = record
    { _<∙_   = _≺ₙ_
    ; tri∙   = ≺ₙ-tri
    ; irr∙   = ≺ₙ-irr
```

The least-element search takes the bundle at its word. Its family argument is a function into `hProp`, so the property is stated at each name; the hypothesis is the truncation `∥ Σ ... ∥₁`, mere inhabitedness, carrying no chosen witness; and the conclusion is an explicit pair of a name and its leastness, a chosen witness after all, extracted by `leastOf` with the module's classical hypothesis `lem`. The truncation may be eliminated because the whole type of a least witness, `Σ[ a ∈ Name ] IsLeast nameOrder P a`, is a proposition: any two least witnesses coincide by trichotomy. Thus classical descent converts mere inhabitation into a definite least name.

```agda
    ; trans∙ = ≺ₙ-trans
    ; wf∙    = ≺ₙ-wf }

  leastName : (P : Name → hProp (ℓ-suc ℓ))
            → ∥ Σ[ a ∈ Name ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ Name ] IsLeast nameOrder P a
  leastName = leastOf nameOrder lem
```

## Recap

Every successor-stage member now has a name, and the names carry a strict well-order, so a least representative can be selected. A `Name` is an arity, a parameter-free formula of one more variable, and a vector of parameters from the stage; `denote` is the subset it carves, and `denote-mem` states this in the inner semantics by which the definable powerset is defined. `names-complete` says every member of the successor stage is denoted by some name, and the existence claim is truncated, because that is how the definable powerset yields its formula in the first place.

`code∈limit` places the first key where the limit-stage order can compare it, and `code-inj` is injective after the arities have been aligned: equal codes then recover equal parameter-free formulas. `_≺ᵥ_` orders the third key across lengths, and `_≺ₙ_` is the three-key comparison itself, with all four strict-well-order laws and `leastName`, which returns the least name of a non-empty family. The combination is what the choice construction ahead consumes: a family of subsets of one stage becomes a family of names, and `leastName` picks a canonical representative without ever choosing a formula from the truncated completeness statement.