BedrockNames for the members of a stage
A member of a successor stage is a definable subset of the stage below, and the previous chapters have said what that means twice over: once as a formula with parameters drawn from that stage, and once, after the parameters left 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 tower's limit level, where the previous chapter well-ordered everything; its parameters are members of the stage below, which the construction ahead will have well-ordered by then. 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.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Choice.Name {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Semantics open import FOL.Manipulation.Relabelling using ( mapTm; embed; embed-⊨ ) open import FOL.Manipulation.Parameters using ( countFo; constantsFo; absFo; ⊨-abs₁ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; module VCode ) open import V.Model {ℓ} using ( self∈sucV ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; Lset; Lset-mono; 𝒟ₒ; 𝒟ₒ-inv ) open import L.Definability {ℓ} using ( module DefOf ) 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.Coding.Bridge {ℓ} lem using () renaming ( graph to envGraph ) open import L.Coding.CodeSet {ℓ} lem using ( keyS; AllCodes ) open import L.Coding.Uniform {ℓ} lem using ( val-sat; module Table ) open import L.Choice.Finite {ℓ} lem using ( Limit; inSome; limitOrder; Tri-map ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( Tri; lt; eq; gt; SWO; IsLeast; leastOf ) open import Cubical.Foundations.Prelude using ( J; substRefl; toPathP ) open import Cubical.Foundations.Equiv using ( equivFun; invEq ) open import Cubical.Functions.Embedding using ( isEmbedding→Inj ) 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ℕ ) 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 ) 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 using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ᵥ open hPropStructure 𝒮ʟ using () renaming ( S to Sʟ ; _∈ˢ_ to _∈ʟ_ )
A parameter-free code is hereditarily finite
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 chapter's clauses 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: the previous chapter's inSome says a member of Lset ω has appeared by some finite stage, and the basic-axioms chapter's pr∈Lset-suc says a Kuratowski pair of two members of a stage appears two stages later. Climbing from one finite stage to a later one is monotonicity applied along the numerals' successors, which is the only recursion this section runs.
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 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 ω ⟩ 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 ω ⟩ 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
The induction itself is then fourteen one-line clauses, twelve for the formula constructors and two for the terms, and the constant clause is discharged by the empty type's eliminator. Nothing about the tag numbers matters beyond their being numerals.
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 ω ⟩ 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 ψ)) code∈limit (¬̇ φ) = tag∈limit 5 _ (code∈limit φ) code∈limit ⊤̇ = tag∈limit 6 _ (numeral∈limit 0) code∈limit ⊥̇ = tag∈limit 7 _ (numeral∈limit 0) code∈limit (∃̇ φ) = tag∈limit 8 _ (code∈limit φ) code∈limit (∀̇ φ) = tag∈limit 9 _ (code∈limit φ) code∈limit (∀̇∈ t φ) = tag∈limit 10 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ)) code∈limit (∃̇∈ t φ) = tag∈limit 11 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ))
The pair of the code with that membership is what the first key compares. One small fact travels with it, proved once by path induction: moving a formula from one arity to an equal one leaves its code alone. The trichotomy below needs exactly this, at the point where two names have been found to have the same arity.
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 χ ⌝ code-shift {i} e χ = J (λ j' e' → VCode.⌜ embed (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e' χ) ⌝ ≡ VCode.⌜ embed χ ⌝) (cong (λ ψ → VCode.⌜ embed ψ ⌝) (substRefl {B = λ k → Formula (⊥* {ℓ}) (suc k)} χ)) e
A parameter-free formula is recovered from its image
Two names with the same first key must turn out to be built from the same formula, or the comparison would rank two different names as neither below the other and equal to nothing. The coding chapter 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 in sight has at least one free variable, and every other clause is the identity on the constructor. On a formula that had no constants to begin with the erasure changes nothing, one clause at a time, and injectivity is then three compositions.
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) eraseFo (t ∈̇ u) = eraseTm t ∈̇ eraseTm u eraseFo (t ≐ u) = eraseTm t ≐ eraseTm u eraseFo (φ ∧̇ ψ) = eraseFo φ ∧̇ eraseFo ψ eraseFo (φ ∨̇ ψ) = eraseFo φ ∨̇ eraseFo ψ eraseFo (φ ⇒̇ ψ) = eraseFo φ ⇒̇ eraseFo ψ eraseFo (¬̇ φ) = ¬̇ eraseFo φ eraseFo ⊤̇ = ⊤̇ eraseFo ⊥̇ = ⊥̇ eraseFo (∃̇ φ) = ∃̇ eraseFo φ eraseFo (∀̇ φ) = ∀̇ eraseFo φ eraseFo (∀̇∈ t φ) = ∀̇∈ (eraseTm t) (eraseFo φ) eraseFo (∃̇∈ t φ) = ∃̇∈ (eraseTm t) (eraseFo φ) 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 χ) ≡ χ 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 ψ) eraseFo-embed (¬̇ φ) = cong ¬̇_ (eraseFo-embed φ) eraseFo-embed ⊤̇ = refl 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 φ) 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
Everything below is relative to one set A, the stage the names are written over, and on one well-order of that stage's members, so the chapter works in a module Naming A w. A name is an arity, a parameter-free formula with one more free variable than that, and a vector of that many parameters drawn from A's small member type. The extra variable is the one a subset is carved by; the rest receive the parameters, and the first key is read off the formula at once.
-- perf: the naming data are definitions of this module, not of another 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) 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) 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, which is where the previous chapter put them. 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.
private module SemM = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) DA.𝒮M open SemM using ( _^_ ) subsetOf : (⟪ A ⟫ → hProp ℓ) → S subsetOf P = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ P m ⟩) (λ p → ⟪ A ⟫↪ (p .fst)) ⟪⟫↪-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 ℓ 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.
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) 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 ⟩ bwd h = ∣ (m , equivFun (decode .snd) h) , refl ∣₁
Every member of the successor stage has a 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 the previous chapter turned such a formula into a parameter-free one of higher arity together with the constants it mentioned. Reading the second off the first is the whole of naming, and it is a function.
nameOf : Formula ⟪ A ⟫ 1 → Name nameOf φ = countFo φ , (absFo φ , constantsFo φ)
Its adequacy is the previous chapter's, spent here. 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 saying so is the only bookkeeping the identification costs.
private emptySat : (f : ⊥* {ℓ} → DA.SM) {n : ℕ} → DA.SM ^ n → Formula (⊥* {ℓ}) n → Ω emptySat f γ χ = γ ⊨ᶠ χ where open SemM.At (⊥* {ℓ}) f using () renaming ( _⊨_ to _⊨ᶠ_ ) 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 ∷ []) ⊨ᵐ φ) absSat φ m = embed-⊨ (hPropAlgebra (ℓ-suc ℓ)) DA.𝒮M DA.ι (absFo φ) (environment (nameOf φ) m) ∙ cong (λ f → emptySat f (environment (nameOf φ) m) (absFo φ)) sameReading ∙ sym (⊨-abs₁ (hPropAlgebra (ℓ-suc ℓ)) DA.𝒮M DA.ι φ (DA.ι m)) 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) 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) (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 gives up a formula in the first place.
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) where named : Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DA.defSet φ ≡ x) → Σ[ a ∈ Name ] (denote a ≡ x) named (φ , q) = nameOf φ , (denote-defSet φ ∙ q)
The denotation, read from inside
When the stage is an element of L, the denotation is also what the internalized satisfaction table says. The uniform-satisfaction chapter stated its reading at an arbitrary arity and an arbitrary environment, so the table's value at the key of the name's formula is satisfaction over the carrier at that very environment; composing that with the specification above identifies membership in the denotation with membership in the table's value. The name is data of the meta-language, and this is the sentence that makes it readable inside.
module Internal (pA : ⟨ isL A ⟩) where private Aʟ : Sʟ Aʟ = A , pA denote-table : (a : Name) (m : ⟪ A ⟫) (x : Sʟ) (x∈ : ⟨ x ∈ʟ AllCodes Aʟ ⟩) → fst x ≡ fst (keyS Aʟ (embed (formula a))) → (z : Sʟ) → fst z ≡ envGraph Aʟ (environment a m) → (⟪ A ⟫↪ m ∈ˢ denote a) ≡ (z ∈ʟ Table.val Aʟ Aʟ x x∈) denote-table a m x x∈ q z qz = denote-mem a m ∙ sym (val-sat Aʟ (embed (formula a)) x x∈ q (environment a m) z qz)
The order on the parameter vectors
The module's second parameter is the well-order of the stage's members, and the rest of the chapter spends it. The third key compares parameter vectors, and it compares them in the obvious way: at the first position where they differ, the given order decides.
The comparison is written across two lengths, and the two cases where a vector runs out are the empty type. That costs nothing where the lengths are equal, which is the only place the comparison is ever reached, and it buys the absence of a transport: the second key has already pronounced the arities equal by then, but the two vectors still have syntactically different lengths, and a comparison demanding one length would have to move one of them first.
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 ; trans∙ to ≺ₚ-trans ; wf∙ to ≺ₚ-wf ) infix 20 _≺ᵥ_ _≺ᵥ_ : ∀ {j k} → Vec ⟪ A ⟫ j → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ) [] ≺ᵥ [] = ⊥* [] ≺ᵥ (y ∷ q) = ⊥* (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.
≺ᵥ-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) → 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 ≺ᵥ-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) ≺ᵥ-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) 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) 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.
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 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 → 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 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 ≺ᵥ-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.
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 {i} e p q = J (λ j' e' → (subst (Vec ⟪ A ⟫) e' p ≺ᵥ q) ≡ (p ≺ᵥ q)) (cong (λ v → v ≺ᵥ q) (substRefl {B = Vec ⟪ A ⟫} p)) e ≺ᵥ-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 {i} e p q = J (λ j' e' → (p ≺ᵥ subst (Vec ⟪ A ⟫) e' q) ≡ (p ≺ᵥ q)) (cong (λ v → p ≺ᵥ v) (substRefl {B = Vec ⟪ A ⟫} q)) e
Three keys, in order
The comparison of names is the lexicographic one on those three keys, written out as a sum rather than declared as an inductive relation. That is a measurement, not a taste: an inductive declaration is checked for positivity, and positivity checking normalizes the constructors' arguments, which here means unfolding the limit order down to the search it is defined by. Written as a sum nothing unfolds, and the three cases read off the shape.
infix 20 _≺ₙ_ _≺ₙ_ : Name → Name → Type (ℓ-suc ℓ) a ≺ₙ b = (codeOf a ≺ codeOf b) ⊎ ( (codeOf b ≡ codeOf a) × ( (arity a < arity b) ⊎ ((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 carry an equality of one key across the other's comparison, and that is all the bookkeeping there is; the parameter case appeals to the vector comparison at three lengths, which is why that one was proved across lengths.
≺ₙ-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 ≺ₙ-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) = 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)) ≺ₙ-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 descends the keys, each new one reached only when the previous one has pronounced equality. The last stop is the only one with work in it. There the arities are equal but not identical, so the first name's parameters are moved to the second's length before the vectors are compared, and the two strict verdicts are moved back; and when the vectors agree, the two names agree, because the first key's equality now says the formulas have the same code, and a code determines a parameter-free formula.
Everything here is stated at the two names themselves rather than at their components. That is the second measurement of the chapter: a statement made at a name's three projections is equal to one made at the name only up to eta, and matching the two forced the whole limit order open, at eighty-seven seconds for one lemma.
≺ₙ-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) 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) → 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)) where shifted : Vec ⟪ A ⟫ (arity b) shifted = subst (Vec ⟪ A ⟫) e (params a) sameFormula : subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a) ≡ formula b 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) (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 , 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 is the same descent read as a recursion, one stage 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, the code is fixed and the arity descends; outermost, the code descends. Each stage is a separate function taking the outer stages' induction hypotheses as arguments, so each recurses on exactly one accessibility proof and the recursion is structural everywhere.
The name always arrives as a name, with equations saying where its keys sit. That is the same law as the trichotomy's, met again: an accessibility stated at a name's components would have to be matched against one stated at the name.
private accAtParam : (c : Limit) → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b) → (k : ℕ) → ((b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b) → (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 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))) = 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 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)) 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 = 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 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 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 packaged are a strict well-order on the names, which is the interface the choosing device takes; and the least-element search of the well-order chapter, applied to it, turns a merely inhabited family of names into a definite one. This is the whole of what the names were built for: a family of sets over one stage becomes a family of names, and a family of names has a least member.
nameOrder : SWO (Name) nameOrder = record { _<∙_ = _≺ₙ_ ; tri∙ = ≺ₙ-tri ; irr∙ = ≺ₙ-irr ; trans∙ = ≺ₙ-trans ; wf∙ = ≺ₙ-wf } leastName : (P : Name → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ Name ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ Name ] IsLeast nameOrder P a leastName = leastOf nameOrder lem
Recap
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 says so in the inner semantics the definable powerset is defined by, with denote-table identifying it with what the internalized table reads. names-complete says every member of the successor stage is denoted, truncated, which is how the definable powerset gives up its formula.
code∈limit puts the first key where the previous chapter's order can reach it, and code-inj makes that key faithful; _≺ᵥ_ orders the third key across lengths, and _≺ₙ_ is the three-key comparison itself, with all four laws and leastName, the least name of a non-empty family.
Three costs were measured, and every one of them is the same accident seen from a different side: something forces the limit order open, and the limit order unfolds into a search for a least ordinal. An inductive declaration of the comparison forces it in the positivity check; a statement made at a name's projections rather than at the name forces it when the two are matched, at eighty-seven seconds a lemma; and naming data reached from another module forces it at every comparison of codes, which was the largest of the three. Written as a sum, stated at names throughout, and with the data defined where it is used, the chapter costs nothing.