BedrockCanonical names for successor-stage members
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
⟪⟫↪-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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(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.
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.
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.
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.
; 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.
(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.
≺ᵥ-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.
→ 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.
≺ᵥ-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.
≺ᵥ-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.
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.
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.
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.
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.
→ 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.
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.
≺ᵥ-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.
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.
≺ᵥ-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.
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.
⊎ ((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.
≺ₙ-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.
≺ₙ-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.
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.
≺ₙ-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.
≺ₙ-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.
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.
→ 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.
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.
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.
(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.
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.
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.
→ (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.
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.
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.
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 ℕ.
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.
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.
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.
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.
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.
; 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.