BedrockFormulas for name comparison
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA definable subset can have many names. At the meta-level, a name consists of an arity k, a parameter-free formula with suc k variable slots, and a vector of k parameters from the carrier. Its denotation is then derived from these three pieces: the extra variable ranges over the candidate member, and the remaining variables receive the parameter vector. The denotation is therefore not a fourth component of the name.
To express this data inside L, the chapter represents the parameter vector by a finite environment graph and represents evaluation by the satisfaction graph. At a genuine formula key, satGraphAt relates that key to the set of environments satisfying the formula. Its output is exactly this satisfaction-environment set. NameAt combines the arity, parameter-free formula code, and parameter environment with the derived denotation that will later be shared by all competing names.
Names are compared lexicographically: first by the formula code under the limit-stage order, then by arity, and finally by the parameter vectors under the given order on the carrier. The formula ≺At expresses these three cases. LeastNameAt only states that the displayed name has no smaller name with the same denotation; the actual choice of a least name is the earlier construction CanonicalNames.leastName. StepAt locally quantifies two least names and compares them. The adequacy proved in this chapter reaches exactly ≺At versus the meta-level relation _≺ₙ_; the full adequacy of NameAt, LeastNameAt, and StepAt is established in the following development.
{-# OPTIONS --cubical --safe --guardedness #-}
The underlying language supplies universe levels, finite indices, vectors, and proposition-valued statements. Classical reasoning enters through one explicit hypothesis, LEM (ℓ-suc ℓ), whose level is large enough for the satisfaction constructions and well-orders used below. Keeping that hypothesis visible will let us distinguish descriptions that merely state a property from earlier constructions that actually choose a witness.
open import Base.Prelude open import Base.Classical using ( LEM )
Fix a universe level ℓ and a law of excluded middle at the required higher level. This is the classical interface carried by the chapter. The formula constructors below only assemble syntax, but the natural-number object, satisfaction graph, limit-stage code order, and canonical-name theory that they use were constructed under the same hypothesis. The module therefore records these semantic dependencies without performing another choice. LeastNameAt expresses minimality; CanonicalNames.leastName remains the construction that selects a least name.
module L.Choice.NameComparison {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
The object language can speak about membership and equality, combine propositions, and quantify both over the whole carrier and over a set. Its semantics is read in a proposition-valued structure. Constant mappings connect three presentations needed later: genuinely parameter-free formulas, formulas over the empty alphabet, and the same syntax interpreted over a constructible carrier. Because these mappings preserve the formula, they will allow the code of a parameter-free skeleton to be recognized internally.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed )
Formula codes, ordered pairs, and numerals are themselves sets in the cumulative hierarchy. The constructible substructure supplies the carrier in which the formulas are read, while transitivity lets membership in a constructible code set provide the constructibility facts needed for its components. Injectivity of pair and numeral coding later recovers arities and skeleton codes from equal keys. The stages Lset provide the setting for the limit-stage code order.
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset ) open import L.Ordinal {ℓ} using ( ∈#-elim; #∈#-elim ) open import L.Axioms.Basic {ℓ} using ( ∅ʟ; extensionalL )
An arity is represented by a numeral in the internal natural-number set, and a parameter vector is represented by the graph of a finite environment. The object-language formulas can inspect ordered pairs, applications, and domains, extend an environment by a candidate element, and define a subset extensionally. For a formula over a carrier, Sat is the set of environments satisfying that formula. This set-valued reading is the semantic value later recovered from the satisfaction graph.
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ ) open import L.Coding.Environment {ℓ} using ( env; lookup-spec ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro; envOverAt ) open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in-both; numL; sucAtL; sucAtL-adequate; consAtL ) open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
Satisfaction has already been organized into a table whose entries pair each subformula key with its recursively determined set of satisfying environments. Slot closure and totality ensure that every genuine key needed in the recursion receives an entry, and the satisfaction bridge identifies its constants with elements of the chosen carrier. The present chapter can therefore read a stored value at a key without running the satisfaction recursion again.
open import L.Coding.SatisfactionTable {ℓ} lem using ( slot; satTable; total; inSlot; entry-in ) open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed ) open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst ) open import L.Coding.CodeSet {ℓ} lem
For each carrier, AllCodes collects exactly the genuine formula keys over that carrier, and its two directions connect membership with an underlying formula. The uniform bridge then supports the relational formula satGraphAt B x y: when x is a genuine key over the carrier in slot B, y is the corresponding set of satisfying environments. GraphWitAt and the two graph readings expose this set-valued relation without starting a fresh recursion.
using ( keyS; AllCodes; AllCodes-out; key∈AllCodes ) open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge ) open import L.Coding.SatisfactionGraph {ℓ} lem using ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out ; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )
The environment tower and the tagged recursion data justify the satisfaction-graph reading at every syntactic constructor. Against this internal machinery, the canonical-name theory supplies the meta-level standard used for comparison. A meta-level Name stores an arity, a parameter-free formula, and a parameter vector; limitCode derives the first comparison key from the formula, while the denotation is separately derived by satisfaction. This distinction is what the later slot formula must preserve.
open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds ) open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 ) open import L.Coding.CodeDomain {ℓ} using ( Tags ) open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds ) open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )
The code of a name is a member of the limit stage and is compared by limitOrder. The third key comes from an arbitrary strict well-order on the carrier. Canonical naming has already combined these with natural-number arity into _≺ₙ_, proved that relation well-founded, and used it in leastName. Here the two non-numerical orders appear through relation slots with representation laws, so the chapter describes their comparison rather than reconstructing either order.
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
Natural-number order supplies the second comparison key: for numeral arities, membership of one numeral in another expresses strict inequality. Finite indices locate entries of parameter vectors and the earliest position at which two vectors differ. The adequacy argument later proves, by induction on their common length, that this first-difference description agrees with the recursive vector order used in _≺ₙ_.
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.Nat.Order using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
The proof data follow the lexicographic shape. Dependent pairs carry a position together with its evidence, while coproducts separate the code, arity, and parameter cases. Equalities of earlier keys permit dependent formulas and vectors to be transported to a common arity before the next key is compared. The empty type supplies the unique interpretation of constants for a formula that has no constants.
open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) import Cubical.Data.Empty as Empty open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Prelude using ( subst2 )
Existential and disjunctive satisfaction is propositionally truncated: it preserves that a witness exists while forgetting which witness was supplied. Consequently, outward readings such as those for formula codes and name comparison return truncated existence, and elimination is used only into propositions. This is propositional truncation; propositional resizing does not occur here. The cumulative hierarchy supplies set-valued membership and the extensional equality principles needed after such readings.
open import Cubical.Foundations.Transport using ( constSubstCommSlice ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties
Small members of a hierarchy set embed into the ambient hierarchy, and injectivity of that embedding later turns equality of represented parameters back into equality in the carrier. The empty set serves as the empty alphabet: it has no constants, so every map out of it is uniquely determined and a parameter-free formula keeps the same code under the required relabellings. The von Neumann numerals # k, their successor, and ω provide the internal arities used by environment domains and name comparison.
using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ ) open import Cubical.Functions.Embedding using ( isEmbedding→Inj ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet ) open InfinitySet using ( #_; ω; sucV )
The formulas ahead are interpreted in the constructible universe. Opening hPropStructure 𝒮ʟ fixes their carrier S: an element is an ambient set together with evidence that it is constructible. It also brings the proposition-valued equality and membership relations of this structure into scope. Thus a free variable or constant ranges over constructible sets, while ⟨_⟩ exposes the type of evidence carried by an equality or membership proposition when a proof uses it.
open hPropStructure 𝒮ʟ
There are two compatible readings of the same syntax. The absoluteness instance starts with the ambient universe structure 𝒮ᵥ and restricts it to the transitive class isL. In the outer reading, a constructible set is viewed through its underlying ambient set; in the inner reading, a constant denotes the constructible set that names it and the restricted structure supplies equality and membership. This chapter renames the inner satisfaction relation to ⊨. Consequently, for γ : S ^ n, the judgement γ ⊨ F says that F holds inside L under the finite environment γ. This is the reading needed for formulas that L itself will use to recognize and compare names.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
The formulas refer to earlier data by positions in an environment. Under a new binder, every such position must move past the newly bound value; after two binders, position i therefore becomes suc (suc i). The abbreviation sh2 records this move. It is used when FreeAt has bound the successor arity and its code key before consulting the skeleton and empty-alphabet code set, and when the denotation condition has bound a candidate element and its extended environment before consulting the original parameter environment.
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
Inside the denotation condition, the skeleton and the carrier's code set are consulted only after four values have entered the environment: the candidate element z, the extended environment c, its domain k, and the key under consideration. Their original positions must therefore be raised four times. sh4 performs exactly that shift, so the key can be required both to belong to the carrier's code set and to equal the pair formed from k and the skeleton.
sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = suc (suc (suc (suc i)))
One more existential binds the value v associated with the key, so the carrier is five places away when satGraphAt is invoked. Here v is the set of environments satisfying the encoded formula, rather than a truth value; the following membership atom asks whether the extended environment belongs to that set. The same shift reappears in LexAt: after binding an index, the two values at that index, an earlier index, and their proposed common value, the original parameter environments are again five places away. sh5 records the common index calculation for both formulas.
sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n))))) sh5 i = suc (suc (suc (suc (suc i))))
The same code at the empty alphabet
The empty alphabet is the small presentation ⟪ ∅ ⟫ of members of the empty set. If m were one of its symbols, the embedding ⟪ ∅ ⟫↪ would produce an ambient set, while the presentation law would say that this set belongs to ∅. The theorem ∅-empty rules out precisely such evidence, giving noAlpha m. Thus formulas over this alphabet cannot contain a constant node. They form one syntactic presentation of parameter-free formulas. Comparing it with the empty constant domain ⊥* used by meta-level names amounts to relating two empty types.
private noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥ noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)
Fo∅ n names the family Formula ⟪ ∅ ⟫ n: formulas over the empty alphabet with n available variable positions. Their lack of constants follows from the type of their constant symbols, rather than from an extra predicate on a formula. Meta-level names use the parallel family Formula ⊥* n. More precisely, a Name stores an arity, a formula from that family with one extra variable position, and a parameter vector of the stated arity; its denotation is derived from those three pieces and is not another stored component.
Fo∅ : ℕ → Type ℓ Fo∅ = Formula ⟪ ∅ {ℓ} ⟫
The map ε changes from the empty alphabet ⟪ ∅ ⟫ to the empty constant domain ⊥*. Given a supposed source symbol m, noAlpha m yields a contradiction, and empty elimination supplies the requested target. Hence mapFo ε relabels a formula over ⟪ ∅ ⟫ as a formula over ⊥*; in the other direction, embed may be specialized to relabel from ⊥* into ⟪ ∅ ⟫. Neither operation changes a constant occurrence, since there is none. The composition law for relabelling then yields the precise equalities of formula codes needed for the empty-alphabet characterization.
ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ} ε m = Empty.rec (noAlpha m)
To recognize parameter-free formula codes inside the model, we must first relate two presentations of having no constants. A formula ψ over ⟪ ∅ ⟫ uses as its constant domain the members of the empty set, while mapFo ε ψ presents the same syntax over the empty type ⊥*. The map ε exists because an alleged member of the empty set yields a contradiction. Reading ψ directly into the universe and first relabelling it by ε and then embedding it therefore differ only by maps out of an empty type. Function extensionality identifies those maps, and mapFo-comp identifies the composite relabelling. Thus sameCode proves an equality of the resulting universe-formulas themselves; applying the coding map to this equality will later give equality of their codes.
sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ) sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m))) ∙ sym (mapFo-comp ε Empty.rec* ψ)
The converse comparison begins with a parameter-free formula χ : Formula ⊥* n. It may be embedded first into formulas over ⟪ ∅ ⟫ and then relabelled by the inclusion of that alphabet into the universe, or embedded directly into formulas over the universe. By mapFo-comp, the first route is a single relabelling from ⊥*; since every two functions from ⊥* agree, that relabelling is the one used by the direct embedding. The equality sameCode' is exactly the orientation needed to pass from the key that AllCodes ∅ʟ assigns to the embedded formula to the usual universe-code of χ.
sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n) → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))
There is one further dependent-type issue. The arity is part of the type of a formula, so an equality e : i ≡ j moves ψ : Fo∅ i to subst Fo∅ e ψ : Fo∅ j. The key, however, should retain the same formula code after this move. The codomain of the function that reads and codes a formula is the fixed universe V ℓ, independent of the arity index. The general substitution computation constSubstCommSlice therefore says that transporting the formula does not change its code. codeShift records the equality in the direction from the transported formula's code back to the original one, ready for the arity adjustment in the decoding argument.
codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i) → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝ ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ codeShift e ψ = sym (constSubstCommSlice Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)
We can now prove the easy direction of the code-set bridge. For a parameter-free k-ary formula χ, embedding it over ⟪ ∅ ⟫ produces a formula whose key belongs to AllCodes ∅ʟ by key∈AllCodes. That key consists of the numeral # k and the code obtained by reading the embedded formula through the empty alphabet. The equality sameCode' identifies this formula with the direct universe embedding of χ; the latter code is precisely fst (limitCode χ). Transporting membership along that equality proves freeCode-in: the code set contains the arity-and-code key of every parameter-free formula.
freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩ freeCode-in k χ = subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ) (key∈AllCodes ∅ʟ (embed χ))
For the reverse direction, suppose pr (# k) c belongs to AllCodes ∅ʟ. The elimination theorem AllCodes-out decodes a member only under propositional truncation, and it takes an element of S, namely a set together with a proof that it is constructible. The underlying set of the desired input is already pr (# k) c; it remains to supply that constructibility proof. Once this is done, PT.map read transforms each possible decoded payload into the desired k-ary parameter-free payload without ever removing the truncation.
freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩ → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁ freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h) where cL : ⟨ isL (pr (# k) c) ⟩
That missing certificate follows from transitivity of constructibility. AllCodes ∅ʟ .snd says that the code set is constructible, while h says that the key belongs to it. Hence isL-trans h (AllCodes ∅ʟ .snd) proves that the key itself is constructible. Pairing this certificate with pr (# k) c gives the element of S required by AllCodes-out; no additional decoding or choice occurs here.
cL = isL-trans h (AllCodes ∅ʟ .snd)
Inside the truncation, AllCodes-out supplies an arity n, a formula ψ : Fo∅ n, and an equality saying that the given key is the key of ψ. The local function read turns each such payload into a parameter-free formula of the requested arity k together with an equality between c and its code. It does so by first transporting ψ to a formula ψ' : Fo∅ k and then relabelling its impossible constants along ε. Thus the proposed witness is mapFo ε ψ'. The pair equality provides both the arity equality needed for the transport and the code equality used in the returned dependent pair.
read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ)) → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step) where e : n ≡ k
The two components of the key equality finish the construction. Its first component has type # k ≡ # n; injectivity of numerals and symmetry yield e : n ≡ k, along which ψ is transported to ψ'. Its second component says that c is the universe-code obtained from the original ψ. By codeShift, that code agrees with the code of the transported ψ'; by sameCode, the latter agrees with the code of embed (mapFo ε ψ'). Composing these equalities gives exactly the certificate paired with the witness. Since read is applied only through PT.map, freeCode-out concludes merely that such a parameter-free formula exists under propositional truncation. It does not select a formula from the code set.
e = sym (#-inj′ (pr-inj q .fst)) ψ' : Fo∅ k ψ' = subst Fo∅ e ψ step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝ step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')
Constant-freeness, said as one atom
The code set stores a formula under a key made from its arity and its skeleton. To express this with one membership atom, FreeAt first binds the successor of the value in the arity slot, then binds its pair with the skeleton, and finally asks whether that pair belongs to the code-set slot. Thus, in meta-level notation, its shape is ∃[ z ] ∃[ y ]: z is the successor arity, while y is the key. The shifts record exactly which earlier slot remains visible beneath one or two binders. At this stage the formula only describes membership in the set supplied at C₀; its parameter-free meaning will follow when that slot is identified with the code set for the empty alphabet.
FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n FreeAt C₀ s a = ∃̇ ( sucAtL (suc a) zero ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s) ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )
The first pair of readings works over an arbitrary environment γ. The external equality qa identifies the value at the arity slot with the numeral # k; it is a hypothesis of the semantic reading, not another clause inside FreeAt. The skeleton and code-set slots remain arbitrary, so these lemmas isolate the logical content of the two binders before the particular code set is chosen.
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ) (qa : fst (lookup a γ) ≡ # k) where
For the forward construction, suppose the intended key pr (# (suc k)) (fst (lookup s γ)) already belongs to the set at C₀. This key supplies the two existential witnesses required by FreeAt: first the numeral # (suc k), then its pair with the skeleton. What remains is to verify the successor and pairing descriptions of these witnesses; the final atom is exactly the assumed membership.
FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩ → ⟨ γ ⊨ FreeAt C₀ s a ⟩ FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁ where numAt : S
An existential witness for the internal language is an element of S, so its underlying set must come with a proof of constructibility. The first witness numAt has this proof because every numeral belongs to L. For the second witness keyAt, the membership hypothesis places the key inside the constructible set held at C₀; transitivity of L then makes the key itself constructible. These proofs justify using the numeral and the key as bound values, rather than adding any mathematical condition to FreeAt.
numAt = # (suc k) , numL (suc k) keyAt : S keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd) hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩ hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
The adequacy equations for the two auxiliary formulas now perform the promised checks. For hsuc, the equality qa changes the value at the arity slot into # k, and the successor of that numeral is # (suc k). For hpr, adequacy of prAtL reduces satisfaction to equality with the ordered pair specified by its two component slots; keyAt was defined to be precisely that pair. Hence the two semantic facts connect the chosen witnesses to the one membership atom.
(cong sucV (sym qa)) hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl
The reverse reading extracts membership from a satisfaction of FreeAt. Satisfaction of an existential formula provides its witness only under propositional truncation, so the proof eliminates the outer truncation into the desired membership proposition. A representative of the outer existential contains the successor witness and a satisfaction of the inner existential; the latter still has its own propositional truncation and will be eliminated in turn.
FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩ → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩ FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ))) atNum where
Both truncation eliminations have the same codomain, so the proof names it Target: the intended key belongs to the set at C₀. This type is a proposition because membership in a set is proposition-valued. That fact is the precise license required by each truncation eliminator; no choice of a distinguished existential witness is being made.
Target : Type (ℓ-suc ℓ) Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
The branch atKey handles one representative of the inner existential. It is given the outer witness z together with the equation saying that z is the successor of the arity value, and it receives an inner witness y with two facts: y satisfies the pairing formula and its underlying set belongs to the set at C₀. The inner existential was truncated, but inside this elimination branch its representative may be used to prove the proposition Target.
atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ)) → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩ × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ ) → Target atKey z qz (y , (hp , hy)) =
Adequacy of prAtL identifies the underlying set of y with the pair whose first component is the underlying set of z and whose second component is the skeleton. The equation for z, followed by qa, identifies that first component with # (suc k). Consequently y is the intended key. Transporting the given membership of y along this equality proves membership of pr (# (suc k)) (fst (lookup s γ)), which is Target.
subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩) (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy
The outer elimination branch atNum receives a representative z together with two pieces of evidence. The first says that z satisfies the successor formula. The second, hk, is the still-truncated satisfaction of the inner existential. Thus atNum has enough information to determine the intended first component of the key, while postponing the inner witness until it can be eliminated into Target.
atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩ × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s) ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ ) → Target atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
Adequacy of sucAtL decodes the first fact into the equality required by atKey: z is the successor of the value at the arity slot. The proof then eliminates hk into the proposition Target and applies atKey to each representative. Together with the outer elimination already built into FreeAt-out, this accounts for both existential layers while preserving the propositional-truncation boundary.
∈ fst (lookup C₀ γ))) (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk
The next readings specialize the two previously arbitrary slots. The equality q₀ identifies the set at C₀ with AllCodes ∅ʟ, whose elements are keys for formulas over the empty alphabet, while qa again identifies the arity value with # k. Under these hypotheses, the membership characterized by FreeAt-in and FreeAt-out can be converted into an actual statement about parameter-free formulas of arity suc k.
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ) (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) (qa : fst (lookup a γ) ≡ # k) where
Starting from a satisfaction of FreeAt, FreeAt-out yields membership of the key in the set currently held at C₀. Transport along q₀ moves this membership into AllCodes ∅ʟ. The earlier decoding lemma freeCode-out then returns, under propositional truncation, a parameter-free formula χ of arity suc k whose limit-stage code is the value in the skeleton slot. This is the outward semantic reading of the one membership atom.
codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩ → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ] (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁ codeFree-out h = freeCode-out (suc k) (fst (lookup s γ)) (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀
The arity is suc k because a name for a definable subset uses one variable for the candidate element in addition to its k parameter positions. The formula witness in codeFree-out remains propositionally truncated. Although FreeAt-out may eliminate its bound witnesses locally because membership is a proposition, freeCode-out introduces a truncated formula witness at the final decoding step. The result therefore asserts that such a formula exists without selecting one.
(FreeAt-out C₀ s a γ k qa h))
Conversely, codeFree-in begins with a specific parameter-free formula χ of arity suc k and an equality identifying its limit-stage code with the skeleton slot. The lemma freeCode-in places the corresponding key in AllCodes ∅ʟ; transport along the code equality and then along the reverse of q₀ moves that membership to the actual skeleton and code-set slots. FreeAt-in packages the resulting membership with the two existential witnesses. This direction needs no truncated formula witness because χ is part of the input.
codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k)) → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩ codeFree-in χ q = FreeAt-in C₀ s a γ k qa (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀) (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)
Together, codeFree-out and codeFree-in give the promised reading of FreeAt once the arity and empty-alphabet code-set slots are identified. The outward direction says, under propositional truncation, that the skeleton is the code of a parameter-free formula with suc k variables. The inward direction starts with a specified formula and needs no such truncation. This finishes the recognition of a name's formula; the next question is how its finite parameter environment records the number k.
(freeCode-in (suc k) χ)))
How long a sequence is
We first characterize arbitrary membership in the set-coded graph. If pr x y belongs to env g, where g is indexed by Fin k, then merely there is an index i for which x ≡ # (toℕ i) and y ≡ g i. The result remains under propositional truncation because membership in a hierarchy set records only the mere existence of a generating entry. Thus memberOf exposes every possible index without choosing one.
private memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩ → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁ memberOf k g x y = PT.map (λ { (li , e) → lower li
The membership witness contains an equality between a stored graph entry and the queried pair. Injectivity of the ordered-pair constructor splits that one equality into equalities of the two components. The stored entry is written first in the witness, so both component paths are reversed to obtain the orientation required by memberOf: from x and y to the numeral key and the value supplied by g.
, (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })
Conversely, every prescribed index supplies an entry. For i : Fin k, the pair pr (# (toℕ i)) (g i) belongs to env g; the lifted index is the membership witness and the entry equation is reflexivity. Hence memberOf and entryOf give the two directions needed to recognize the horizontal coordinates of this finite graph.
entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k) → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩ entryOf k g i = ∣ lift i , refl ∣₁
The forward domain inclusion begins with the mere existence of a model element y such that pr x (fst y) lies in the graph. Its goal is the membership proposition x ∈ # k, so the outer propositional truncation may be eliminated into that goal. After fixing one representative y, it remains to recover an index from the graph membership and prove that its numeral belongs to # k.
dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ) → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩ dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry where atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))
For an explicit index i, only the first component equality matters to the domain. Since toℕ i < k, the numeral lemma #mono places # (toℕ i) in # k; transport along x ≡ # (toℕ i) then places x there. The second component equality identifies the graph value but is irrelevant to this inclusion. The helper atEntry fixes the value y before eliminating the remaining truncated index information.
→ ⟨ x ∈ # k ⟩ atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx) (#mono (toℕ i) k (toℕ<n i)) atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩ atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))
Applying memberOf supplies precisely that index information, still under propositional truncation. Because x ∈ # k is a proposition, PT.rec may feed each representative to atIndex. This closes the forward inclusion without extracting an index as ordinary data.
(memberOf k g x (fst y) p)
For the reverse inclusion, suppose x ∈ # k. Elimination for von Neumann numerals says, under propositional truncation, that x ≡ # m for some natural number m < k. Such an m determines an index in Fin k. The conclusion is itself a propositionally truncated existence of a graph value, so PT.map can transform each numeral witness without choosing one. The hypothesis cg will supply the constructibility certificate needed to present that value as an element of the model.
dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩) → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h) where atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))
For a representative m < k, let i be the corresponding finite index. The witness for the existential is the model element (g i , cg i), namely the value at that index together with its constructibility proof. The graph fact comes from entryOf: the pair with canonical first component # (toℕ i) is an entry. Transporting that first component to x gives the required membership of pr x (g i) in the graph.
→ Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ atNumeral (m , (p , qx)) = (g i , cg i) , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i) where i : Fin k
The conversion fromℕ' k m p turns the bound p : m < k into the index i. Its round-trip law toFromId' proves toℕ i ≡ m. Composing x ≡ # m with the numeral image of the symmetric round-trip equality gives qi : x ≡ # (toℕ i), exactly the path used to move the canonical entry to the queried first component. This completes the reverse domain inclusion.
i = fromℕ' k m p qi : x ≡ # (toℕ i) qi = qx ∙ cong #_ (sym (toFromId' k m p))
We can now compare these two set-level inclusions with the object-language domain formula. Fix an environment γ, a family g : Fin k → V ℓ, and an equation qe identifying the underlying set in slot e with env g; slot d remains the proposed domain. Each cg i certifies that g i is an element of the constructible model, exactly what the reverse inclusion needs when it builds an existential witness. In this context the next two lemmas read and fill domAt e d.
module _ {n : ℕ} (e d : Fin n) (γ : S ^ n) (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩) (qe : fst (lookup e γ) ≡ env g) where
Suppose γ satisfies domAt e d. To prove that the underlying set in slot d is # k, domAt-numeral applies extensionality inside L to the two model elements lookup d γ and (# k , numL k), then projects their equality to the underlying sets. It therefore suffices to prove, for every constructible test element x, that membership in the proposed domain and membership in the numeral are the same proposition. The forward implication begins by reading domain membership through domAt-in.
domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k domAt-numeral h = cong fst (extensionalL {a = lookup d γ} {b = # k , numL k} pt) where fwd : (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ fst x ∈ # k ⟩ fwd x hx = dom-into k g (fst x)
In the forward implication, domAt-in turns membership in slot d into the mere existence of a value paired with x in the set at slot e. Transport along qe places that entry in env g, and dom-into yields x ∈ # k. Conversely, dom-from turns x ∈ # k into the mere existence of an entry in env g. Since membership in the proposed domain is a proposition, that truncation may be eliminated; the local function put handles each displayed entry.
(subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe (domAt-in e d γ h x hx)) bwd : (x : S) → ⟨ fst x ∈ # k ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩ bwd x hx = PT.rec (snd (fst x ∈ fst (lookup d γ))) put (dom-from k g cg (fst x) hx) where
For one displayed entry, put transports its membership back along qe to the graph stored at slot e; domAt-out then gives membership in slot d. Thus the two implications form, by ⇔toPath, a path between the two membership propositions at every x. Extensionality assembles those pointwise paths into the equality of the proposed domain with # k. The truncated graph witness is used only to prove membership, so no value is selected from it.
put : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ env g ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩ put (y , p) = domAt-out e d γ h x y (subst (λ u → ⟨ pr (fst x) (fst y) ∈ u ⟩) (sym qe) p) pt : (x : S) → (fst x ∈ fst (lookup d γ)) ≡ (fst x ∈ # k) pt x = ⇔toPath (fwd x) (bwd x)
The converse starts from an equality saying that the set in slot d really is # k. To establish domAt e d, domAt-intro asks pointwise for the two implications that define a domain: mere existence of a value in the graph implies membership in d, and membership in d implies the mere existence of a value. The equations qe and qd reduce these to dom-into and dom-from, respectively. Thus filling the formula uses the same two set-level inclusions as reading it, in the opposite direction.
domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩ domAt-fill qd = domAt-intro e d γ step where step : (x : S) → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩
To fill the domain formula, it remains to prove its two pointwise implications. For the first, suppose some value is paired with fst x in the graph stored at slot e. Transport along qe puts this entry in env g, where dom-into shows that fst x belongs to the numeral # k. Transporting back along qd then places it in the proposed domain at slot d.
→ ⟨ fst x ∈ fst (lookup d γ) ⟩) × (⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩) step x = (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)
The reverse implication follows the same path in reverse. Membership in slot d is transported by qd to membership in # k; dom-from then supplies, under propositional truncation, a value paired with fst x in env g; and transport along the inverse of qe returns that entry to slot e. These two directions complete domAt-fill without choosing a value from the finite graph.
(subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe hy))) , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) (sym qe) (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))
What the satisfaction graph assigns
We now ask what the satisfaction graph assigns at a genuine formula key. Fix an ambient environment γ: slot B supplies the carrier, while x and y supply the proposed key and value. The abbreviation Bs = lookup B γ keeps the proof uniform in all three slots. Formulas considered below therefore have constants indexed by the members of the underlying set fst Bs.
module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where private Bs : S Bs = lookup B γ
The graph formula packages a satisfaction recursion through fourteen bound slots. For a model-language formula φ, fr φ supplies those slots with the carrier Bs, its canonical satisfaction table, the subformula-key slot, the environment tower, and the ten constructor-tag numerals, followed by the ambient environment γ. Each component is the canonical one already constructed for this carrier and formula.
fr : ∀ {m} (φ : Formula S m) → S ^ (14 + n) fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
The ten numerals do not index the code domain. They label the ten constructor clauses of the table specification, from zero through nine. tgs φ records that every designated tag slot in fr φ contains the numeral matching its constructor. This alignment lets the packaged table formula select the right clause for each syntactic form.
tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
The table also needs the correct family of environments for every arity. htow φ applies the established tower theorem to the components of fr φ: the value in the tower slot is Tower.tower Bs, the carrier slot is Bs, and the zero-tag slot contains the required numeral. Thus towerAt holds in the extended environment, with no new tower argument needed here.
htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩ htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl
The domain of the canonical table is exactly the slot of formula keys. One direction starts with a table entry and uses inSlot to put its key in slot Bs φ; because the entry is obtained under propositional truncation, elimination is into the membership proposition. The other direction uses total to give, merely, a table value for every key in the slot. domAt-intro combines these implications into hdom φ.
hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩ hdom φ = domAt-intro Ti Ci (fr φ) (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ))) (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h) , (λ h → total Bs φ (fst z) h))
The forward reading can now be stated precisely. Let ψ be a formula whose constants are members of fst Bs. If slot x contains its genuine key keyS Bs ψ, and slot y contains the satisfaction set of the translated model-language formula mapFo (asConst Bs) ψ, then satGraphAt B x y holds. The value is a set of satisfying environments, rather than a single truth value. graphAt-value proves the claim by supplying the canonical recursion witness to graphAt-in.
graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m) → fst (lookup x γ) ≡ fst (keyS Bs ψ) → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ)) → ⟨ γ ⊨ satGraphAt B x y ⟩ graphAt-value {m} ψ qx qy = graphAt-in B x y γ
The existential witness is assembled from the five canonical components in the order expected by GraphWitAt: the numeral assignment numν, the tower, the slot, the satisfaction table, and the carrier. It is then wrapped in propositional truncation, matching the existential semantics of the graph formula. What remains is to certify that these chosen components satisfy the carrier, tag, tower, closure, domain, entry, and table requirements.
∣ numν , (Tower.tower Bs , (slot Bs φ , (satTable Bs φ , (Bs
The carrier equation is reflexivity. The next three certificates say that the ten tag slots contain the intended numerals, that the environment slot is the tower over Bs, and that slot Bs φ is closed under the formula constructors with immediate subformulas. This last property is what allows the recursive table clauses at a compound formula key to consult entries at its immediate subformula keys.
, (refl , (tgs φ , (htow φ , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3 ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
The final requirements identify the table's domain, its selected entry, and its clause specification. The previously proved hdom φ gives the domain formula. For the entry, keyBridge Bs ψ relates the key of the carrier-language formula to that of φ, while qx and qy transport the canonical entry to slots x and y. Finally, SlotHolds.holds proves that the canonical table satisfies tableAt from the same carrier, tags, tower, slot, and table. The assembled witness therefore establishes the graph formula.
, (hdom φ , (subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩) (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ) , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁ where
Here φ is the model-language version of ψ. A constant of ψ is a member of the underlying carrier, and asConst Bs equips that member with the constructibility evidence needed to regard it as an element of S; mapFo applies this constant map throughout the formula. The separate keyBridge used above ensures that direct coding before this translation and internal coding after it produce the same underlying key.
φ : Formula S m φ = mapFo (asConst Bs) ψ
For the reverse reading, suppose satGraphAt B x y holds and slot x is the genuine key of ψ. graphAt-out exposes the fourteen existential components only under propositional truncation. The desired conclusion is an equality in the cumulative hierarchy V, and setIsSet says that this equality type is a proposition. Hence PT.rec may inspect each displayed graph witness locally without choosing one globally.
graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m) → fst (lookup x γ) ≡ fst (keyS Bs ψ) → ⟨ γ ⊨ satGraphAt B x y ⟩ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ)) graphAt-only {m} ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)
Unpacking one graph witness gives a proposed table T, a code domain C, an environment tower E, a carrier b, and all their certificates. The domain C need not be the canonical slot; what matters is that it is subcode-closed, that T satisfies the packaged table clauses, and that the genuine key lies in C. The last fact follows by applying domAt-out to the displayed table entry ha. With that membership and the same entry, SatSoundC.pinned applies to ψ and forces its recorded value to be the canonical satisfaction set.
where read : GraphWitAt B x y γ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ)) read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) = SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12 ψ (subst (λ u → ⟨ u ∈ fst C ⟩) qx
Both premises for pinning are read at the ambient key in slot x. Transporting by qx turns the domain membership obtained from hd and ha into membership of keyS Bs ψ in C, and turns ha itself into an entry of T at that key and the value in slot y. The pinned theorem then returns exactly the required equality: at a genuine formula key, any value admitted by the graph is the satisfaction set of the translated formula.
(domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha)) (lookup y γ) (subst (λ u → ⟨ pr u (fst (lookup y γ)) ∈ fst T ⟩) qx ha)
A name, described at slots
The denotation body tests one candidate z at a time. Its first conjunct, z ∈ B, restricts the set being described to the carrier. It then binds an environment c and requires c to be the coded environment obtained by putting z in front of the parameter environment e. At that point c and z precede the ambient assignment, so the reference to e is shifted through two binders.
DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n) DenoteBody B C s e = (var zero ∈̇ var (suc B)) ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e) ∧̇ ∃̇ ( domAt (suc zero) zero
The remaining three witnesses determine how the skeleton is evaluated. First k is required to be the domain of the extended environment c. Next key must belong to the code set in slot C and equal the pair of k with the skeleton code s. Finally v is a value admitted by the satisfaction graph for the carrier B at that key, and the last membership says c ∈ v. When C is the carrier's genuine code set, these clauses say that the extended environment satisfies the skeleton rather than merely consulting the graph at an arbitrary key.
∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C)) ∧̇ ( prAtL zero (suc zero) (sh4 s) ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )
A meta-level name consists of an arity, a parameter-free formula, and a parameter vector. NameAt represents these by an arity slot a, a skeleton code slot s, and an environment slot e; its denotation slot d records the set derived from those data. The first conjunct checks that the pair formed from the successor of a and s belongs to the empty-alphabet code set. The successor is essential: a name with a parameters needs one further variable for the candidate member. The next conjunct requires a to be a member of the model's natural numbers.
NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n NameAt B C C₀ s a e d = FreeAt C₀ s a ∧̇ ( (var a ∈̇ con ωʟ)
The third conjunct makes e an environment with exact domain a and values in B; in particular, it ties the parameter vector to the arity recorded in the preceding slot. The last conjunct characterizes d extensionally. For every candidate, membership in d is equivalent to satisfaction of DenoteBody, whose first conjunct already restricts the candidate to B. Thus d is derived from the three pieces of a name rather than stored as an additional piece of the meta-level name.
∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )
DenoteOf z is the meta-level payload corresponding to the four existential layers of DenoteBody. It records an extended environment c, its proposed domain k, a formula key, and a graph value v, together with all the conditions connecting them. Keeping this data in one dependent tuple exposes the witnesses needed to assemble the object-language formula while retaining the dependencies of each later condition on the earlier choices.
module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where DenoteOf : (z : S) → Type (ℓ-suc ℓ) DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ] ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩ × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
The payload follows the semantic chain exactly. The first two satisfaction proofs say that c extends the old environment and that k is its domain. Membership of key in C certifies that the following graph lookup is made at a genuine code when C is instantiated by AllCodes B. The explicit equation then identifies that key with the pair of k and s. The last two proofs say that v is the graph value at this key and that c belongs to v. Here v is a set of satisfying environments, not a Boolean truth value.
× ( ⟨ fst key ∈ fst (lookup C γ) ⟩ × ( (fst key ≡ pr (fst k) (fst (lookup s γ))) × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩ × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )
DenoteBody-in turns this explicit payload into satisfaction of the body. The carrier membership remains the outer conjunct, while the witnesses c, k, key, and v are introduced in the same order as the four existential binders. Most conditions are already stated as satisfaction proofs. The exception is the equation defining key: the pairing formula's adequacy path converts that set-theoretic equation into satisfaction of prAtL.
DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩ DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm))))))))) = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp
Each object-language existential is interpreted by propositional truncation, so the construction wraps every one of the four witnesses before closing the proof. The final line closes these four layers from the graph value out to the extended environment. Consequently the resulting satisfaction records that suitable data exist, while the untruncated witnesses remain available only in the input DenoteOf z used to build it.
, ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁
DenoteBody-out preserves the same boundary in the reverse direction. The outer carrier membership is available directly because it lies outside every existential. The four witnesses, however, are exposed only within nested propositional truncations. Each use of truncation elimination targets ∥ DenoteOf z ∥₁, again a proposition, so the proof may transform each local choice of witnesses without selecting a tuple globally.
DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩ → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁ DenoteBody-out z (hz , hc) = hz , PT.rec squash₁ (λ { (c , (hc , hk)) → PT.rec squash₁ (λ { (k , (hk , hkey)) → PT.rec squash₁
At the key layer, the body supplies satisfaction of the pairing formula, whereas DenoteOf requires the decoded equation fst key ≡ pr (fst k) (fst (lookup s γ)). Reading the pairing formula's adequacy path in the forward direction produces precisely this equation. The innermost map then retains the graph and membership proofs with the witness v, and the surrounding eliminations rebuild the whole payload under one propositional truncation.
(λ { (key , (hi , (hp , hv))) → PT.map (λ { (v , (hg , hm)) → c , (k , (key , (v , (hc , (hk , (hi , ( subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp , (hg , hm) ))))))) }) hv }) hkey }) hk }) hc
NameAt-in takes five inputs. The first three establish the fixed conjuncts: the skeleton is parameter-free at the stated arity, the arity lies in the model's natural numbers, and the parameter graph is an environment over the carrier. The remaining two inputs give the two pointwise directions needed to characterize the denotation. From z ∈ d, the first returns z ∈ B together with an explicit DenoteOf z; conversely, the second turns z ∈ B and an explicit DenoteOf z into z ∈ d.
module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where NameAt-in : ⟨ γ ⊨ FreeAt C₀ s a ⟩ → ⟨ fst (lookup a γ) ∈ ω ⟩ → ⟨ γ ⊨ envOverAt e a B ⟩ → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
Both directions are stated separately for every candidate because extAt expresses equality of sets by pointwise membership. They deliberately use an untruncated DenoteOf z: this lemma is an introduction rule, so its caller supplies the concrete data from which satisfaction of the body can be built. Recovering such data from an arbitrary satisfaction of NameAt is a separate adequacy argument, and its result in the following chapter remains under propositional truncation.
→ ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z) → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z → ⟨ fst z ∈ fst (lookup d γ) ⟩) → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ NameAt-in hf ha he into back =
The proof feeds these two directions to the introduction rule for extAt. For z ∈ d, the first direction supplies carrier membership and a payload, which DenoteBody-in converts into satisfaction of the body. Conversely, satisfaction of the body is read by DenoteBody-out as carrier membership and a propositionally truncated payload. Truncation elimination may then apply the second input because its target, z ∈ d, is a proposition. Combining this extensional characterization with the first three inputs establishes the whole name formula.
hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd)) (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ))) (back z (DenoteBody-out B C s e γ z h .fst)) (DenoteBody-out B C s e γ z h .snd))))
The order, with no recursion of its own
The comparison formulas next bind data in blocks, so references to the ambient assignment must be shifted uniformly. sh3 moves an ambient slot past three new binders. In LexAt these binders hold an index i and the two values read from the parameter environments at i, allowing the original slots for the two environments and the parameter order to remain in scope. The same shift later carries ambient slots past the skeleton, arity, and environment of a competing name in LeastNameAt.
private sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i))
sh6 performs the corresponding move past six binders. It is used when StepBody binds two names, each represented by a skeleton, an arity, and a parameter environment. The fully extended assignment therefore has the six new values before the original one, while the carrier, the two order relations, the two code sets, and the denotations being compared remain ambient slots. These shifts preserve the intended references; they add no ordering assumption and perform no comparison themselves.
sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i)))))
The parameter key asks for the first position at which two parameter environments differ. LexAt begins by binding an element i of the set in the arity slot. When that slot contains the numeral for an arity, its members are exactly the numerals for smaller positions, so this bounded existential ranges over the possible indices without introducing a separate order on indices.
LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n LexAt P a e₁ e₂ = ∃̇∈ (var a) ( ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero) ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero
After choosing i, two existential witnesses give values u and v with e₁(i)=u and e₂(i)=v, and a third application asserts that the ordered pair of u and v belongs to the parameter relation P. The bounded universal then considers every j ∈ i; for each such j, an existential witness x must be a value of both environment graphs at j. Thus the formula says "strictly ordered here, with a common value at every earlier position." Only after the two environments are identified as single-valued graphs does a common value imply equality of the corresponding parameters. In the later adequacy argument, graph lookup and injectivity of the carrier embedding supply precisely that implication. The formula itself performs no recursion.
∧̇ ( appAt (sh3 P) (suc zero) zero ∧̇ ∀̇∈ (var (suc (suc zero))) ( ∃̇ ( appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )
The full name comparison now combines the three keys in their lexicographic priority: skeleton code, arity, and parameter environment. Its first disjunct applies the relation in slot R to s₁ and s₂. By the adequacy of application, this says that the ordered pair of the two skeleton codes belongs to R. Keeping R as a slot makes the formula uniform; the later adequacy theorem instantiates it with a relation representing the limit-stage code order.
≺At : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ = appAt R s₁ s₂ ∨̇ ( (var s₂ ≐ var s₁)
The second disjunct handles equal skeleton codes. It records the equality in the direction s₂ = s₁ and then offers the remaining two lexicographic cases: either a₁ ∈ a₂, which means that the first arity is smaller when both slots contain numerals, or a₂ = a₁ and LexAt P a₁ e₁ e₂ settles the comparison at the first differing parameter. The orientations s₂ = s₁ and a₂ = a₁ match the later transports that move the second name's code and parameter vector to the first name's data.
∧̇ ( (var a₁ ∈̇ var a₂) ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )
To prove a reusable reading of LexAt, we isolate the formula occurring under the agreement existential. At a previously considered position j, Body requires one value x to satisfy both applications, hence to occur in both environment graphs at j. In the extended assignment the five new entries are x, j, v, u, and i, so each reference to an ambient environment is shifted past five binders.
module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where private Body : Formula S (suc (suc (suc (suc (suc n))))) Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero
With i, u, and v fixed, Inner i u v records the body left by the first three existential binders. Its first two components say that the graphs e₁ and e₂ contain the pairs (i,u) and (i,v). The third says that the pair (u,v) belongs to the relation P. These are still satisfaction statements for appAt; their decoded membership form will be recorded separately so that the two presentations can be related explicitly.
Inner : (i u v : S) → Type (ℓ-suc ℓ) Inner i u v = ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩ × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩ × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩
The fourth component of Inner is agreement below i. For every model element j belonging to i, it supplies the semantic existential ∃[ x ∶ S ] saying that one x satisfies Body. This existential is a propositional truncation: it retains the existence of a common value at j without exposing a chosen value as data. The bounded universal is therefore read as a function that supplies one such truncated existence for each j ∈ i.
× ((j : S) → ⟨ fst j ∈ fst i ⟩ → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩) ) )
Agrees i states the same agreement after decoding the two applications. For every j ∈ i, merely there is an element x : S such that the pair formed from the underlying sets of j and x belongs to both graphs e₁ and e₂. When i is an arity numeral, its members represent precisely the earlier positions. This definition records only a common graph value. Equality of the corresponding meta-level parameters is derived later from the known environment graphs and the injectivity of the carrier embedding.
Agrees : (i : S) → Type (ℓ-suc ℓ) Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩ → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩ × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁
Differs collects the complete decoded witness for a first difference. It contains an index i, values u and v, membership of i in the set stored at the arity slot, graph memberships for (i,u) and (i,v), the strict parameter comparison at that position, and Agrees i. When the arity slot is a numeral and the two graph slots are parameter environments of that arity, these fields are exactly the data needed for a lexicographic first difference.
Differs : Type (ℓ-suc ℓ) Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩ × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩ × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩
The strict comparison field has the same relational form as the code case of ≺At: the ordered pair of the underlying values of u and v belongs to the set in slot P. The final field Agrees i records a common value at every earlier position; for the intended single-valued environment graphs, this certifies that no earlier parameters differ. Thus Differs separates the mathematical content of the first-difference witness from the object-language binders used to express it.
× ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )
The map pack converts only the agreement component of Inner into Agrees; the first three components are irrelevant to this local conversion. For a fixed j ∈ i, a witness x for the semantic existential comes with two satisfactions of appAt. Applying appAt-adequate to each turns them into the two graph memberships required by Agrees, while preserving the same witness x.
private pack : (i u v : S) → Inner i u v → Agrees i pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map (λ { (x , (p₁ , p₂)) → x , ( subst ⟨_⟩
This conversion is performed inside the existing propositional truncation. PT.map sends every possible witness and its two application proofs to the same witness with two membership proofs. Since the target is again a truncated existence, no representative is extracted and no choice principle is used. Pointwise mapping is enough to obtain Agrees i for every earlier position.
(appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁ , subst ⟨_⟩ (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) }) (hj j hj')
unpack provides the converse conversion needed to satisfy the formula. From Agrees i and a position j ∈ i, it receives a truncated common-value witness. For each representative x, it keeps that witness and prepares to turn the two graph memberships back into satisfactions of the two applications in Body.
unpack : (i u v : S) → Agrees i → (j : S) → ⟨ fst j ∈ fst i ⟩ → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩ unpack i u v hj j hj' = PT.map (λ { (x , (p₁ , p₂)) → x
The same adequacy paths are now used in the reverse direction. Each membership proof is transported along the symmetric path of appAt-adequate, producing the corresponding conjunct of Body. Again PT.map keeps the construction inside the truncated existential, so unpack proves the required semantic existence without selecting a common value globally.
, ( subst ⟨_⟩ (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁ , subst ⟨_⟩ (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) }) (hj j hj')
LexAt-in starts from the explicit data in Differs. The index i and the values u and v become the witnesses for the bounded existential and the two following existentials, with hi certifying the bound. In the extended assignment γ₃ = v ∷ u ∷ i ∷ γ, the first two graph memberships are transported backward along appAt-adequate to satisfy the applications for e₁(i)=u and e₂(i)=v. The remaining relation and agreement fields fit the same conjunction, with unpack supplying its bounded-universal component.
LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj))))))) = ∣ i , (hi , ∣ u , ∣ v , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁ , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂
The final field of Differs completes the introduction proof. The membership of (u,v) in P is transported backward along appAt-adequate to satisfy the third application, while unpack turns agreement below i into the bounded universal's semantic form. The assignment γ₃ = v ∷ u ∷ i ∷ γ makes the binder order explicit; the surrounding constructors then close the existentials for v, u, and i, from the inside out.
, ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁ where γ₃ : S ^ (suc (suc (suc n))) γ₃ = v ∷ u ∷ i ∷ γ
Reading LexAt outward must preserve the witness boundary created by its existentials. Accordingly, LexAt-out targets ∥ Differs ∥₁, a proposition, and eliminates the outer truncation only into that target. The local function atValue performs the mathematical decoding: once particular i, u, and v, the bound proof, and the remaining satisfaction data are available inside the eliminations, it builds an untruncated Differs record. No such record is chosen outside those local scopes.
LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁ LexAt-out = PT.rec squash₁ atIndex where atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v
The first half of atValue recovers the index and the two graph lookups. The bound proof hi already has the form required by Differs. Reading the two adequacy paths forward converts satisfaction of the applications into membership of (i,u) in e₁ and membership of (i,v) in e₂. Thus the two values remain attached to the same index at which the formula found them.
, ( hi , ( subst ⟨_⟩ (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁ , ( subst ⟨_⟩ (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂
The third application is decoded in the same way, yielding membership of (u,v) in the parameter relation P. The function pack supplies the final field by translating the bounded agreement from application form to the two graph memberships required by Agrees i. These pieces form one explicit Differs record inside atValue; the surrounding eliminations will retain only its propositional truncation.
, ( subst ⟨_⟩ (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp , pack i u v h ) ) ) ) ))
The innermost existential supplies the second value v together with Inner i u v, but only within its truncation. The handler atSecond uses each locally available pair (v,h) to build Differs by atValue and immediately places the result in ∥ Differs ∥₁. This is exactly the permitted elimination: the witness is used to prove a proposition and is not exposed by the result.
atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁ atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁
One layer farther out, atFirst receives a particular first value u and a truncated existence of the second value. It eliminates that inner truncation with atSecond, whose result is again ∥ Differs ∥₁. The argument therefore passes from the first value to the completed first-difference record without ever requiring a globally available v.
atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁ atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h
Finally atIndex receives an index i, its proof hi of lying below the arity, and the truncated remainder beginning with u. Eliminating that remainder with atFirst completes the outward reading. Taken together, the three handlers follow the existential nesting from i to u to v, while every elimination has the same propositional target. Hence LexAt-out establishes that a first-difference record merely exists, with no choice of its index or values.
atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩ × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ ) → ∥ Differs ∥₁ atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h
Reading the comparison, and one step of the family
The meta-level payload Below now arranges the three comparison keys in the same priority as ≺At. Its outer sum says either that the ordered pair of skeleton codes (s₁,s₂) belongs to the relation in slot R, or that the codes are equal and a later key decides. A value of this sum explicitly identifies a branch and carries its evidence; the definition does not assert that such a branch can be decided for arbitrary slot values. This distinction matters because object-language disjunction is interpreted by propositional truncation.
module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where Below : Type (ℓ-suc ℓ) Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩ ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ)) × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
Under equal skeleton codes, the inner sum first offers the arity comparison a₁ ∈ a₂. When the slots contain arity numerals, this membership says that the first arity is smaller. If the arities are equal instead, Differs supplies the first-difference evidence for the parameter key. The equalities are deliberately oriented as s₂ = s₁ and a₂ = a₁, matching the later transport of the second name's data to the first name's types.
⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ)) × Differs P a₁ e₁ e₂ γ ) ) )
≺At-in translates an explicit value of Below into satisfaction of the comparison formula. In the code branch, the relation membership is transported backward along appAt-adequate and introduced as the outer left disjunct. In the arity branch, the code equality accompanies the outer right disjunct, and the arity membership enters the inner left disjunct. These are introduction steps only: the supplied branch evidence is packaged into the truncated semantics of each object-language disjunction.
≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ ≺At-in (inl h) = ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁ ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁ ≺At-in (inr (q , inr (q' , h))) =
The parameter branch takes the remaining route through both disjunctions. It carries the code and arity equalities into their right branches, then invokes LexAt-in on the supplied Differs record. Thus the same first-difference data already decoded above becomes satisfaction of the parameter clause. All three cases of Below are therefore inserted into ≺At without searching for a branch or extracting any existential witness.
∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁
The reverse direction has a necessarily weaker target: ≺At-out returns ∥ Below ∥₁. Satisfaction of the outer object-language disjunction is itself truncated, so PT.rec may inspect a branch only while constructing this proposition. The local function outer separates the code case from the equal-code case. In the latter it retains the equality s₂ = s₁ and passes the still-unsorted inner disjunction to inner.
≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁ ≺At-out = PT.rec squash₁ outer where inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ)) → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
Given the code equality, inner reads the two remaining keys. An arity membership immediately yields the middle case of Below. Otherwise the payload contains the arity equality a₂ = a₁ and satisfaction of LexAt, so only the first-difference component remains to be decoded. The signature keeps these alternatives explicit while fixing the code equality shared by both.
⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ)) × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ ) → ∥ Below ∥₁ inner q (inl h) = ∣ inr (q , inl h) ∣₁ inner q (inr (q' , h)) =
In the parameter case, LexAt-out supplies only ∥ Differs ∥₁, exactly as the existential semantics requires. PT.map sends each locally represented Differs record to the third case of Below, adjoining the already known code and arity equalities. The result remains under one propositional truncation, so the conversion carries existence to existence and never asks for a chosen first-difference witness.
PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)
The type of outer is the semantic split at the first comparison key. Its left side is satisfaction of the application of R to the two skeleton slots; its right side retains the equality s₂ = s₁ together with satisfaction of the remaining arity-or-parameter disjunction. Decoding the left side yields the code case of Below, while eliminating the inner disjunction uses inner. This two-stage reading mirrors the nesting of ≺At and keeps the final result at ∥ Below ∥₁, where neither disjunction is turned into a chosen branch.
outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩ ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ)) × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂) ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ ) → ∥ Below ∥₁
The last two clauses finish the outward reading of the comparison. In the code branch, appAt-adequate converts satisfaction of the relation application into membership of the ordered pair of skeleton codes in R, producing the first case of Below. In the equal-code branch, the inner object-language disjunction is still propositionally truncated, so it is eliminated only into ∥ Below ∥₁. Thus every one of the three comparison keys can be recovered, but the formula does not reveal which key decided the comparison outside the truncation.
outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁ outer (inr (q , h)) = PT.rec squash₁ (inner q) h
To describe the comparison of two least names, the body of the step needs six fresh slots. The first three indices are fixed here: s6a, a6a, and e6a refer respectively to the first name's skeleton code, arity numeral, and parameter environment. After all six binders have been entered, these data lie at de Bruijn positions five, four, and three. Giving the positions names keeps the later formulas about leastness and comparison readable while leaving the binder arithmetic in one place.
private s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n)))))) s6a = suc (suc (suc (suc (suc zero)))) a6a = suc (suc (suc (suc zero))) e6a = suc (suc (suc zero))
The remaining indices s6b, a6b, and e6b point to positions two, one, and zero, where the second name's data will be found. This reversal is the usual de Bruijn effect: the witnesses are bound in the order s₁,a₁,e₁,s₂,a₂,e₂, while each new witness is prepended to the environment. Consequently the fully extended environment is e₂ ∷ a₂ ∷ s₂ ∷ e₁ ∷ a₁ ∷ s₁ ∷ γ, and the six indices select precisely the two intended triples.
s6b = suc (suc zero) a6b = suc zero e6b = zero
A least name is expressed as a property of name data already occupying the slots s, a, and e. Its first conjunct requires those data to satisfy NameAt and hence to denote d. The second conjunct universally quantifies over a competing skeleton code, arity numeral, and parameter environment. The three nested universals place that competitor at positions two, one, and zero, while sh3 keeps the carrier, both code sets, and the denotation d referring to their original slots.
LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n LeastNameAt R P B C C₀ s a e d = NameAt B C C₀ s a e d ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)
The implication restricts attention to competitors that are also names of the same d; names denoting other sets are irrelevant to this minimum. Its conclusion negates ≺At competitor current, so no competing name of d strictly precedes the current one in the three-key order. This formula only states leastness. It neither searches for a name nor removes a propositional truncation to select one. The explicit least-name construction belongs to the meta-language naming development and uses its excluded-middle hypothesis.
(suc (suc zero)) (suc zero) zero (sh3 d) ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero (sh3 s) (sh3 a) (sh3 e)) )))
Repeated existential elimination will need to change the property carried by a witness without choosing that witness globally. The helper exists-map captures exactly this operation. If each B x gives merely a C x, then mere existence of a pair (x , B x) gives mere existence of (x , C x). The outer PT.rec eliminates the original propositional truncation into another propositionally truncated type, and the inner PT.map retains the same x while transforming its second component. At no point does the result expose a particular witness of A.
private exists-map : {A : Type (ℓ-suc ℓ)} {B C : A → Type (ℓ-suc ℓ)} → ((x : A) → B x → ∥ C x ∥₁) → ∥ Σ A B ∥₁ → ∥ Σ A C ∥₁ exists-map f = PT.rec squash₁ (λ { (x , h) → PT.map (x ,_) (f x h) })
The operator ∃₆ binds six object-language variables around an arbitrary body. Its intended use is to supply the two triples of data needed for two names, but the operator itself does not mention names, leastness, or an order. Keeping this binder frame separate lets its semantic introduction and elimination rules be proved once for any formula with six additional free positions; the mathematical conditions on the witnesses will be supplied by StepBody.
∃₆ : ∀ {n} → Formula S (suc (suc (suc (suc (suc (suc n)))))) → Formula S n ∃₆ φ = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ φ)))))
For a body φ and an environment γ, Six records the untruncated data that can introduce the six existentials: witnesses s₁,k₁,p₁,s₂,k₂,p₂ together with satisfaction of φ. The names k and p anticipate their later roles as arity numerals and parameter environments; at this generic stage they are simply elements of the carrier S. Since successive binders prepend their witnesses, the satisfaction environment lists them in reverse order as p₂,k₂,s₂,p₁,k₁,s₁ before the original γ.
module _ {n : ℕ} (φ : Formula S (suc (suc (suc (suc (suc (suc n))))))) (γ : S ^ n) where Six : Type (ℓ-suc ℓ) Six = Σ[ s₁ ∈ S ] Σ[ k₁ ∈ S ] Σ[ p₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ k₂ ∈ S ] Σ[ p₂ ∈ S ] ⟨ (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) ⊨ φ ⟩
The introduction rule starts with all six witnesses explicitly available in a value of Six. It supplies them to the six existential binders in their binding order, wrapping the remaining satisfaction proof in the propositional truncation contributed by each existential. No search or choice is involved: the witnesses are input data. The nested constructors also explain why the environment seen by the body has the reverse order recorded in the definition of Six.
∃₆-in : Six → ⟨ γ ⊨ ∃₆ φ ⟩ ∃₆-in (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , h)))))) = ∣ s₁ , ∣ k₁ , ∣ p₁ , ∣ s₂ , ∣ k₂ , ∣ p₂ , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
The outward rule begins with satisfaction of the six-fold existential and must end in ∥ Six ∥₁, rather than in an exposed six-tuple. Each use of exists-map crosses one existential layer while retaining its locally available witness inside the common propositional target. The chain handles s₁, k₁, p₁, s₂, and k₂ in turn. At the innermost layer, PT.map passes the pair consisting of p₂ and the body's satisfaction proof into the same final truncated payload.
∃₆-out : ⟨ γ ⊨ ∃₆ φ ⟩ → ∥ Six ∥₁ ∃₆-out = exists-map (λ s₁ → exists-map (λ k₁ → exists-map (λ p₁ → exists-map (λ s₂ →
After the fifth application of exists-map, the innermost existential already has the shape needed for the last component, so the identity map suffices. Together, ∃₆-in and ∃₆-out express the semantic content of the binder frame with the correct asymmetry: explicit six-witness data introduces the formula, whereas satisfaction of the formula yields only the mere existence of such data. This generic result can now be specialized without reopening any of the six truncations.
exists-map (λ k₂ → PT.map (λ p → p))))))
The concrete body places three conditions on the two triples selected by the six indices. The first triple must satisfy LeastNameAt for x, and the second must satisfy it for y. Both use the same carrier and the same code sets, while R and P provide the two relation slots used by name comparison. All seven surrounding slots are shifted by sh6, since the body reads them through the six newly bound witnesses.
StepBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S (suc (suc (suc (suc (suc (suc n)))))) StepBody R P B C C₀ x y = LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x) ∧̇ ( LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y)
The third condition compares the two triples with ≺At, placing the name of x strictly before the name of y. Hence StepBody says precisely that two least names over one carrier have been supplied and that the first precedes the second in the three-key name order. It contains no comparison of the stages at which x and y are born, no outer recursive table, and no claim that the represented relation is well-founded. Those belong to the larger construction in which this one-step description is used.
∧̇ ≺At (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b )
StepAt closes StepBody with the six existential binders. As an object-language formula, it asserts merely that there are data for a least name of x, data for a least name of y, and a comparison placing the first before the second. The formula describes this single comparison branch; it does not itself produce either least name, perform the surrounding stage recursion, or prove well-foundedness. Its existential semantics also means that reading a satisfied StepAt outward must preserve propositional truncation.
StepAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n StepAt R P B C C₀ x y = ∃₆ (StepBody R P B C C₀ x y)
For fixed slots and environment, StepOf specializes the generic type Six to StepBody. An element therefore contains six explicit carrier elements and a proof that, in the reversed extended environment, they satisfy the two least-name conditions and the name comparison. Naming this untruncated payload separates it from the proposition expressed by StepAt: the following introduction rule can consume a StepOf directly, while the outward rule can return only ∥ StepOf ∥₁. This is the precise witness boundary of the six-binder step formula.
module _ {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) where StepOf : Type (ℓ-suc ℓ) StepOf = Six (StepBody R P B C C₀ x y) γ
With the six witnesses and the proof of the body already present in StepOf, the introduction direction is immediate. Each witness is placed under its existential quantifier in binding order, so the resulting assignment satisfies StepAt. This step uses the supplied proofs of the two least-name conditions and of the comparison; it does not construct any name.
StepAt-in : StepOf → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ StepAt-in = ∃₆-in (StepBody R P B C C₀ x y) γ
In the converse direction, satisfaction of StepAt can be unpacked only as ∥ StepOf ∥₁. Thus there merely exist two triples satisfying the two least-name formulas, together with satisfaction of the comparison formula from the first triple to the second. The propositional truncation preserves this existence while withholding the six particular witnesses, exactly as required by the semantics of existential quantification.
StepAt-out : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ StepOf ∥₁ StepAt-out = ∃₆-out (StepBody R P B C C₀ x y) γ
Against the names the meta-language built
To compare the formula with the intended meta-level relation, fix a constructible set A and a strict well-order w on its carrier ⟪ A ⟫. Names over A take every parameter from this carrier, so w supplies exactly the order needed for their parameter vectors. The resulting adequacy argument is relative to these data and therefore applies to any constructible set equipped with such an order on its carrier.
module Adequacy (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where private module NM = Naming A w
The naming construction now provides the type Name and the comparisons to be matched. A name of arity k contains a parameter-free formula with suc k variable positions and a vector of exactly k parameters. Its formula code is derived from that formula, and _≺ₙ_ compares names by code first, arity second, and parameter vector last. Renaming the relation of w to _≺ₚ_ simply records its role as the parameter order.
open NM using ( Name; arity; params; codeOf; _≺ᵥ_; _≺ₙ_ ) open SWO w using () renaming ( _<∙_ to _≺ₚ_ )
The recursive vector order is compared with an explicit first-difference relation Lex. For two vectors of the same length, Lex p q chooses an index i, requires the entry of p there to precede the entry of q under _≺ₚ_, and requires equality of the entries at every j with j<i. Unlike the object-language agreement formula, this meta-level relation can state entry equality directly and needs no common graph value as an intermediary.
Lex : ∀ {k} → Vec ⟪ A ⟫ k → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ) Lex {k} p q = Σ[ i ∈ Fin k ] ( (lookup i p ≺ₚ lookup i q) × ((j : Fin k) → toℕ j < toℕ i → lookup j p ≡ lookup j q) )
The map from Lex to the recursive order follows the location of the first difference. At index zero, the strict comparison of the heads is already the first clause of _≺ᵥ_. At a successor index, agreement below that index makes the two heads equal, while the same witness with its index decreased compares the tails. This is structural recursion on the vectors and uses no classical principle.
lex-vec : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Lex p q → p ≺ᵥ q lex-vec (x ∷ p) (y ∷ q) (zero , (h , _)) = inl h lex-vec (x ∷ p) (y ∷ q) (suc i , (h , ag)) = inr (ag zero (suc-≤-suc zero-≤) , lex-vec p q (i , (h , λ j hj → ag (suc j) (suc-≤-suc hj))))
For the reverse map, follow the two clauses of _≺ᵥ_. An order proof for two empty vectors is impossible. If the nonempty vectors are ordered because their heads are strictly ordered, index zero witnesses Lex; no smaller index exists, so the agreement condition is vacuous.
vec-lex : ∀ {k} (p q : Vec ⟪ A ⟫ k) → p ≺ᵥ q → Lex p q vec-lex [] [] h = Empty.rec* h vec-lex (x ∷ p) (y ∷ q) (inl h) = zero , (h , λ j hj → Empty.rec (¬-<-zero hj)) vec-lex (x ∷ p) (y ∷ q) (inr (e , h)) = suc (vec-lex p q h .fst) , ( vec-lex p q h .snd .fst
In the remaining clause, the heads are equal and the tails are recursively ordered. Applying the induction hypothesis to the tails yields their first differing index; shifting it to a successor gives the corresponding index in the original vectors. The supplied head equality proves agreement at position zero, the first position below that shifted index.
, step ) where step : (j : Fin (suc _)) → toℕ j < suc (toℕ (vec-lex p q h .fst)) → lookup j (x ∷ p) ≡ lookup j (y ∷ q) step zero _ = e
At every other position below the shifted index, removing one successor from the numerical inequality reduces the claim to the tails' own agreement. This completes the reverse direction. Hence the explicit first-difference relation and the recursive vector order coincide, allowing the parameter argument to pass between their two presentations without changing the comparison.
step (suc j) hj = vec-lex p q h .snd .snd j (pred-≤-pred hj)
The parameters, on both sides
Formula codes are compared by a second pre-existing order. Each codeOf t lies in the limit stage, whose strict well-order is limitOrder; writing its relation as _≺ˡ_ makes the code key explicit alongside the parameter key _≺ₚ_. No new ordering is defined here: these are precisely the two orders whose internal representations enter the three-key name comparison.
open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )
A parameter is an element of the small carrier ⟪ A ⟫, so it includes both an underlying set and evidence that the set belongs to A. The map ix forgets the membership evidence and retains the underlying set in V. This canonical embedding is the common representation used when parameter values occur in environment graphs and in ordered pairs belonging to the represented relation.
ix : ⟪ A ⟫ → V ℓ ix m = ⟪ A ⟫↪ m
The same underlying set can also be regarded as an element of the constructible model. Since A is constructible and ix m belongs to A, transitivity of constructibility shows that ix m is constructible. Pairing the set with this proof gives ixL m : S, the form required when a parameter is used as an object-language value.
ixL : ⟪ A ⟫ → S ixL m = ix m , isL-trans (∈∈ₛ {a = ix m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) pA
For a name t, the family pfam t reads its parameter vector pointwise. Its domain is Fin (arity t), and its value at i is the underlying V-set of the parameter stored at that index. Thus the arity fixes the domain definitionally, and the graph env (pfam t) gives the internal environment representation of exactly that parameter vector.
pfam : (t : Name) → Fin (arity t) → V ℓ pfam t i = ix (lookup i (params t))
No information about a carrier element is lost by passing to its underlying set. The canonical map ⟪ A ⟫↪ is an embedding, hence ix u ≡ ix v implies u ≡ v. This injectivity is essential in the reverse parameter argument: when two environment graphs share a value at an earlier index, equality of their underlying V-sets can be read back as equality of the corresponding entries of the parameter vectors.
ix-inj : (u v : ⟪ A ⟫) → ix u ≡ ix v → u ≡ v ix-inj u v = isEmbedding→Inj isEmb⟪ A ⟫↪ u v
It remains to state what the two internal relation sets must represent. For codes, Rrep reads membership of the ordered pair of u and v in Rs as u ≺ˡ v, while Rfill proves that membership from the comparison. For parameters, Prep and Pfill give the same two directions between membership of the pair of their ix-images in Ps and u ≺ₚ v. These four laws are hypotheses. Under them, the three-key formula is adequate for any two constructible relation sets with these representations; neither relation is constructed here.
module Keys (Rs Ps : S) (Rrep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩ → u ≺ˡ v) (Rfill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩) (Prep : (u v : ⟪ A ⟫) → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩ → u ≺ₚ v) (Pfill : (u v : ⟪ A ⟫) → u ≺ₚ v → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩)
To apply the four representation laws to a particular parameter comparison, fix two names together with the object-language slots in which their data are read. The local argument is governed by five identifications: one for the parameter relation, one for the first arity, one between the two arities, and one for each parameter environment. Under these hypotheses, it will translate between the explicit first difference Lex and the graph-based record Differs in both directions.
where
The first four identifications establish the common frame. The slot P holds the relation set Ps; the slot a₁ holds the numeral for t₁'s arity; and qk : arity t₂ ≡ arity t₁ makes the two parameter vectors comparable at one length. Finally, e₁ holds the graph of pfam t₁, whose value at an index is the embedded parameter of the first name. Notice that qk is an equality of natural-number arities, rather than an equation for an object-language slot.
module _ {n : ℕ} (P a₁ e₁ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name) (qP : fst (lookup P γ) ≡ fst Ps) (qa : fst (lookup a₁ γ) ≡ # (arity t₁)) (qk : arity t₂ ≡ arity t₁) (q₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
The fifth identification gives the second environment the same domain. First transport params t₂ along qk from length arity t₂ to length arity t₁; then embed each transported entry into V and take the resulting graph. Thus both environments can be queried by an index in Fin (arity t₁). The private families introduced next name their entries before and after this transport, beginning with pr₁ for the first vector.
(q₂ : fst (lookup e₂ γ) ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) qk (params t₂))))) where private pr₁ : Fin (arity t₁) → ⟪ A ⟫
At an index i of the common length, pr₁ i is simply the entry found in t₁'s parameter vector. It remains an element of the small carrier ⟪ A ⟫; the embedding ix is applied only when this parameter is placed into an environment graph or an ordered pair in the model. Keeping these two levels separate lets the parameter order act on carrier elements themselves.
pr₁ i = lookup i (params t₁)
The companion family pr₂ reads the transported vector of t₂. It has the same domain as pr₁, but its values are still carrier elements belonging to the second name. Consequently pr₁ i ≺ₚ pr₂ i and pr₁ j ≡ pr₂ j are well-typed statements at every common index, precisely the strict comparison and prior agreement required by Lex.
pr₂ : Fin (arity t₁) → ⟪ A ⟫ pr₂ i = lookup i (subst (Vec ⟪ A ⟫) qk (params t₂))
The first graph can now be read at an exact index. Suppose the pair with key # (toℕ i) and value fst u belongs to the set in slot e₁. Transporting this membership along q₁ places it in env (pfam t₁), and lookup-spec identifies its second component with that graph's unique value. Since this value is ix (pr₁ i), at₁ recovers the equality fst u ≡ ix (pr₁ i).
at₁ : (i : Fin (arity t₁)) (u : S) → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₁ γ) ⟩ → fst u ≡ ix (pr₁ i) at₁ i u h = subst ⟨_⟩ (lookup-spec (pfam t₁) i (fst u)) (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₁ h)
The same reading applies to the second graph, with the transported family in place of pfam t₁. Membership of the pair at key # (toℕ i) is first moved along q₂; lookup-spec then yields fst u ≡ ix (pr₂ i). Hence at₁ and at₂ give the functional consequence needed here: they identify every value found at a valid index with the particular parameter entry represented there.
at₂ : (i : Fin (arity t₁)) (u : S) → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₂ γ) ⟩ → fst u ≡ ix (pr₂ i) at₂ i u h = subst ⟨_⟩ (lookup-spec (λ j → ix (pr₂ j)) i (fst u)) (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₂ h)
The reverse use of lookup-spec supplies the canonical entry of the first graph. Reflexivity says that ix (pr₁ i) is the value prescribed by pfam t₁ at i; reading the lookup equation backward turns this equality into membership in env (pfam t₁). Transport along the reverse of q₁ then places the same pair in the set actually stored at e₁. This is the witness put₁ i.
put₁ : (i : Fin (arity t₁)) → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ fst (lookup e₁ γ) ⟩ put₁ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ z ⟩) (sym q₁) (subst ⟨_⟩ (sym (lookup-spec (pfam t₁) i (ix (pr₁ i)))) refl)
The witness put₂ i is constructed in exactly the same way for the transported second family and the slot e₂. Together, the four lemmas give both directions of graph lookup for the two names: at₁ and at₂ identify any alleged values, while put₁ and put₂ exhibit the prescribed ones. The forward translation will use the latter pair to build Differs; the reverse translation will use the former pair to recover Lex.
put₂ : (i : Fin (arity t₁)) → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ fst (lookup e₂ γ) ⟩ put₂ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ z ⟩) (sym q₂) (subst ⟨_⟩ (sym (lookup-spec (λ j → ix (pr₂ j)) i (ix (pr₂ i)))) refl)
An index used by Lex is a finite number, whereas an index carried by Differs must be an element of the constructible model. The helper numAt crosses this small boundary: it pairs the von Neumann numeral # m with its constructibility proof numL m. It does not by itself assert that the numeral lies below an arity; that membership will be supplied separately from the finite-index bound.
numAt : (m : ℕ) → S numAt m = # m , numL m
For the forward translation, an element of Lex supplies a finite index i, a strict comparison hlt at that index, and equality agree at every earlier index. The record Differs begins with the model element numAt (toℕ i) and the two values ixL (pr₁ i) and ixL (pr₂ i). Because a finite index is smaller than its length, #mono turns toℕ<n i into membership of its numeral in the arity numeral; transport along qa places that membership in the arity slot.
lex-fill : Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂)) → Differs P a₁ e₁ e₂ γ lex-fill (i , (hlt , agree)) = numAt (toℕ i) , ( ixL (pr₁ i) , ( ixL (pr₂ i) , ( subst (λ z → ⟨ # (toℕ i) ∈ z ⟩) (sym qa)
The next fields certify what happens at the differing index. The witnesses put₁ i and put₂ i put the two embedded parameter values into their respective environment graphs. The representation law Pfill turns hlt : pr₁ i ≺ₚ pr₂ i into membership of their ordered pair in Ps; transport along the reverse of qP moves that membership to the relation set stored in slot P. Thus the three membership fields of Differs express exactly the two lookups and the strict parameter comparison.
(#mono (toℕ i) (arity t₁) (toℕ<n i)) , ( put₁ i , ( put₂ i , ( subst (λ z → ⟨ pr (ix (pr₁ i)) (ix (pr₂ i)) ∈ z ⟩) (sym qP) (Pfill (pr₁ i) (pr₂ i) hlt)
It remains to build Agrees below the chosen index. Given a model element j with fst j ∈ # (toℕ i), the numeral elimination theorem says, under propositional truncation, that fst j is # m for some m < toℕ i. Mapping the local construction step over this result will provide one shared value for the two graphs at that earlier position. The truncation is preserved: the particular natural number recovered from numeral membership is never exposed outside the proposition required by Agrees.
, agrees ) ) ) ) ) ) where agrees : Agrees P a₁ e₁ e₂ γ (numAt (toℕ i)) agrees j hj = PT.map step (∈#-elim (toℕ i) (fst j) hj) where
The function step makes the shared-value claim precise. From a number m < toℕ i and an equality identifying fst j with # m, it must return a model element x whose pair with the key fst j belongs to both environment graphs. The supplied value is the first family's entry at the corresponding finite index, packaged as ixL (pr₁ jx). For the first graph, put₁ jx already gives the required membership at the canonical numeral key; the equality of the two presentations of that key transports it to fst j.
step : Σ[ m ∈ ℕ ] ((m < toℕ i) × (fst j ≡ # m)) → Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩ × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) step (m , (hm , qj)) = ixL (pr₁ jx) , ( subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₁ γ) ⟩)
For the second graph, the earlier-index hypothesis agree identifies pr₁ jx with pr₂ jx. Transporting put₂ jx along the reverse of this equality changes its value from ix (pr₂ jx) to the shared value ix (pr₁ jx); transporting the key as before then gives membership at fst j. Hence both graphs contain the very same value at every position below i, completing one result of step and therefore the Agrees field of Differs.
(sym qjx) (put₁ jx) , subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₂ γ) ⟩) (sym qjx) (subst (λ y → ⟨ pr (# (toℕ jx)) (ix y) ∈ fst (lookup e₂ γ) ⟩) (sym (agree jx (subst (_< toℕ i) (sym qm) hm))) (put₂ jx)) ) where
The remaining identification concerns the key of the shared entry. From m < toℕ i and the fact that i is itself below arity t₁, transitivity makes m a valid element jx : Fin (arity t₁). Converting jx back to a natural number returns m; the path qm records this round trip and will let the graph memberships use their canonical numeral key.
jx : Fin (arity t₁) jx = fromℕ' (arity t₁) m (<-trans hm (toℕ<n i)) qm : toℕ jx ≡ m qm = toFromId' (arity t₁) m (<-trans hm (toℕ<n i)) qjx : fst j ≡ # (toℕ jx)
The equality qj identifies the original model key with # m, while qm identifies m with the number of jx. Their composite is qjx : fst j ≡ # (toℕ jx). This is the precise change of key used above to transport both canonical graph entries to the position named by j; it completes the construction of Agrees, and hence the forward bridge lex-fill.
qjx = qj ∙ cong #_ (sym qm)
The reverse bridge starts from a Differs record and must recover an explicit first difference. Its recorded index i belongs to the arity numeral, but the numeral-membership elimination theorem recovers the corresponding smaller natural number only under propositional truncation. Accordingly lex-read returns the propositional truncation of Lex: numeral elimination hides the chosen number, and PT.map performs the otherwise explicit reconstruction without removing that truncation.
lex-read : Differs P a₁ e₁ e₂ γ → ∥ Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂)) ∥₁ lex-read (i , (u , (v , (hi , (h₁ , (h₂ , (hp , ag))))))) = PT.map atIndex (∈#-elim (arity t₁) (fst i) (subst (λ z → ⟨ fst i ∈ z ⟩) qa hi))
Inside the mapped construction, the hidden witness is available as a concrete number m, together with m < arity t₁ and an equation identifying the model index with # m. The function atIndex must now produce Lex itself. It chooses the corresponding finite index and will prove the two obligations of a first difference there: strict comparison at that index and agreement at every smaller one.
where atIndex : Σ[ m ∈ ℕ ] ((m < arity t₁) × (fst i ≡ # m)) → Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂)) atIndex (m , (hm , qi)) = ι , (below , agrees) where
The bound on m gives ι : Fin (arity t₁). As before, the numeral round trip changes the equation for # m into qι : fst i ≡ # (toℕ ι), so the recorded membership in the first environment can be queried at the canonical key for ι. The lookup lemma at₁ then identifies the recorded value fst u with the embedded first parameter ix (pr₁ ι).
ι : Fin (arity t₁) ι = fromℕ' (arity t₁) m hm qι : fst i ≡ # (toℕ ι) qι = qi ∙ cong #_ (sym (toFromId' (arity t₁) m hm)) qu : fst u ≡ ix (pr₁ ι)
Applying at₂ to the second graph likewise gives fst v ≡ ix (pr₂ ι). The relation atom in Differs says that the ordered pair of the recorded values belongs to the set in slot P; after rewriting that set to Ps and the two values to their embedded parameters, the representation law Prep reads the atom as the required strict comparison pr₁ ι ≺ₚ pr₂ ι.
qu = at₁ ι u (subst (λ z → ⟨ pr z (fst u) ∈ fst (lookup e₁ γ) ⟩) qι h₁) qv : fst v ≡ ix (pr₂ ι) qv = at₂ ι v (subst (λ z → ⟨ pr z (fst v) ∈ fst (lookup e₂ γ) ⟩) qι h₂) below : pr₁ ι ≺ₚ pr₂ ι below = Prep (pr₁ ι) (pr₂ ι)
The transports just described finish the proof named below. It remains to recover agreement before ι. For any j with toℕ j < toℕ ι, the bounded clause ag supplies, merely, one model element whose value occurs in both environment graphs at that position. Since the desired equality of the two embedded parameter sets is a proposition, this propositional truncation may be eliminated directly into it.
(subst2 (λ y z → ⟨ pr y z ∈ fst Ps ⟩) qu qv (subst (λ z → ⟨ pr (fst u) (fst v) ∈ z ⟩) qP hp)) agrees : (j : Fin (arity t₁)) → toℕ j < toℕ ι → pr₁ j ≡ pr₂ j agrees j hj = ix-inj (pr₁ j) (pr₂ j) (PT.rec (setIsSet (ix (pr₁ j)) (ix (pr₂ j))) same
To invoke ag, the finite inequality is first converted by #mono into membership of # (toℕ j) in # (toℕ ι), then transported along qι to the recorded bound. The resulting truncated witness has exactly the shape handled by same: an element x together with membership of the pair (# (toℕ j), fst x) in each environment graph. Thus the truncation contains all the data needed for the equality, while none of that witness data escapes.
(ag (numAt (toℕ j)) (subst (λ z → ⟨ # (toℕ j) ∈ z ⟩) (sym qι) (#mono (toℕ j) (toℕ ι) hj)))) where same : Σ[ x ∈ S ] ( ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₁ γ) ⟩ × ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
For a chosen shared value x, at₁ identifies fst x with ix (pr₁ j) and at₂ identifies the same set with ix (pr₂ j). Reversing the first path and composing it with the second gives equality of the two embedded parameters. Injectivity of ix then reflects that equality back to pr₁ j ≡ pr₂ j, which is precisely the earlier-index condition of Lex. The reverse bridge is now complete.
→ ix (pr₁ j) ≡ ix (pr₂ j) same (x , (k₁ , k₂)) = sym (at₁ j x k₁) ∙ at₂ j x k₂
Both halves
Under the four representation laws supplied to Keys, the two relation slots stand for limitOrder on formula codes and the given order on carrier parameters. The two halves now compare the same three keys. order-in sends a concrete proof of t₁ ≺ₙ t₂ to satisfaction of ≺At; order-out reads such a satisfaction only as ∥ t₁ ≺ₙ t₂ ∥₁. The outward half retains the propositional truncation contributed by disjunction and existential satisfaction. This completes the adequacy of the comparison formula ≺At itself, and no stronger result about the other formulas is proved here.
The remaining boundary is precise. A meta-level Name stores an arity, a parameter-free formula, and a parameter vector; its denotation is derived. Internally, NameAt adds slots for those data and the derived denotation, which it checks using the set of satisfying environments returned by satGraphAt. LeastNameAt states that no smaller name has the same denotation, but does not choose a name. The complete adequacy of NameAt, LeastNameAt, and StepAt, including recovery of their witnesses, belongs to L.Choice.NameComparisonAdequacy; the actual least-name choice remains CanonicalNames.leastName.
Recap
Two path-induction lemmas now remove a type-level obstacle from the full three-key comparison. The first, envShift, concerns an arity equality e : arity t ≡ k. Transporting params t along e, reading its entries, and forming their environment graph yields the same graph as reading params t at its original length. When e is reflexivity the claim reduces immediately, and path induction handles every equality.
private envShift : (t : Name) {k : ℕ} (e : arity t ≡ k) → env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) e (params t)))) ≡ env (pfam t) envShift t e = sym (constSubstCommSlice
The equation is oriented from the graph of the transported vector to the original graph env (pfam t). This orientation is useful in the final proof: the hypothesis for the second environment identifies its slot with the original graph, and the reverse of envShift then identifies that same slot with the graph at the first name's arity, exactly the form expected by the first-difference bridge.
(Vec ⟪ A ⟫) (V ℓ) (λ _ v → env (λ i → ix (lookup i v))) e (params t))
The second lemma, vecShift, performs the parallel simplification for the vector order. Comparing p with q after transporting q along an equality of lengths gives the same proposition as comparing the original vectors. Again the equality proof contributes no mathematical case: path induction reduces it to reflexivity. Together, envShift and vecShift keep the graph presentation and the vector comparison synchronized when the arities are identified.
vecShift : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i) → (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q) vecShift e p q = sym (constSubstCommSlice (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)
The final comparison is carried out at arbitrary slots of an arbitrary environment. Two slots hold the represented relations Rs and Ps; for each name, three more hold its formula code, arity numeral, and parameter graph. The eight equations qR, qP, qs₁, qs₂, qa₁, qa₂, qe₁, and qe₂ pin those readings to two concrete names t₁ and t₂. Under precisely these hypotheses, the internal formula can be compared with _≺ₙ_.
module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name) (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps) (qs₁ : fst (lookup s₁ γ) ≡ fst (codeOf t₁)) (qs₂ : fst (lookup s₂ γ) ≡ fst (codeOf t₂)) (qa₁ : fst (lookup a₁ γ) ≡ # (arity t₁))
The last four slot equations pin the two arities and the two environment graphs; in particular, no chosen coordinates are built into the theorem. To read the second and third keys, equality found between slot values must be lifted back to equality of the dependent data carried by names. The first helper, codeSame, addresses the code key: from equality of the two skeleton slots it reconstructs an equality codeOf t₂ ≡ codeOf t₁ in the type Limit.
(qa₂ : fst (lookup a₂ γ) ≡ # (arity t₂)) (qe₁ : fst (lookup e₁ γ) ≡ env (pfam t₁)) (qe₂ : fst (lookup e₂ γ) ≡ env (pfam t₂)) where private codeSame : fst (lookup s₂ γ) ≡ fst (lookup s₁ γ) → codeOf t₂ ≡ codeOf t₁
An element of Limit is an underlying set together with evidence that it belongs to Lset ω. That evidence is proposition-valued, so Σ≡Prop says that a path between the underlying sets determines a path between the complete codes. The required underlying path is the composite sym qs₂ ∙ q ∙ qs₁: from the second code to its slot, across the recorded skeleton equality, and on to the first code. This explains both why the proof component needs no separate comparison and why the resulting equality has the orientation required by the second branch of the name order.
codeSame q = Σ≡Prop (λ x → snd (x ∈ Lset ω)) (sym qs₂ ∙ q ∙ qs₁)
The reverse conversion starts with equality in Limit, where a code consists of an underlying set together with its proof of membership in the limit stage. Projecting with fst gives equality of the underlying code sets. Composing it with the two slot identifications yields the orientation required by the later branches of the formula: the second skeleton slot equals the first.
codeBack : codeOf t₂ ≡ codeOf t₁ → fst (lookup s₂ γ) ≡ fst (lookup s₁ γ) codeBack ec = qs₂ ∙ cong fst ec ∙ sym qs₁
The parameter branch must read the second environment at the first name's arity. Given ek : arity t₂ ≡ arity t₁, path induction identifies the graph of params t₂ with the graph obtained after transporting that vector to the new length. Reversing this graph equality and composing it with the identification of slot e₂ gives exactly the transported environment expected by the first-difference bridge.
shiftEnv : (ek : arity t₂ ≡ arity t₁) → fst (lookup e₂ γ) ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) ek (params t₂)))) shiftEnv ek = qe₂ ∙ sym (envShift t₂ ek)
The forward theorem now follows the three possible reasons why one name precedes another. In the code branch, Rfill turns the strict comparison of the two formula codes by the limit order into membership of their ordered pair in Rs. The equations for R, s₁, and s₂ transport that membership to the three slots of the formula, and ≺At-in places the resulting witness in the first branch of ≺At.
order-in : t₁ ≺ₙ t₂ → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ order-in (inl h) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ (inl (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩) (sym qR) (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) (sym qs₁) (sym qs₂)
In the arity branch, equality of codes first supplies the required equality of the two skeleton slots through codeBack. The strict inequality arity t₁ < arity t₂ becomes membership # (arity t₁) ∈ # (arity t₂) by the von Neumann numeral law #mono; the two arity-slot equations then carry this membership to the formula. Thus the second key is used only after the first key has been shown equal.
(Rfill (codeOf t₁) (codeOf t₂) h)))) order-in (inr (ec , inl h)) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ (inr (codeBack ec , inl (subst2 (λ y z → ⟨ y ∈ z ⟩) (sym qa₁) (sym qa₂) (#mono (arity t₁) (arity t₂) h))))
The parameter branch begins with equal codes and equal arities. The arity path transports the second parameter vector to the first vector's length; vec-lex then turns their recursive vector comparison into an explicit first differing index. The map lex-fill then turns that witness into the Differs payload used to satisfy LexAt: it records the index, the strict comparison there, and all earlier agreements, using shiftEnv to identify the transported second graph. This constructs the third branch of ≺At directly from the comparison evidence, without extracting any witness from a propositional truncation.
order-in (inr (ec , inr (ek , hv))) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ (inr (codeBack ec , inr (qa₂ ∙ cong #_ ek ∙ sym qa₁ , lex-fill P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek) (vec-lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) (transport (sym (vecShift ek (params t₁) (params t₂))) hv)))))
The reverse theorem retains the propositional truncation carried by the object-language disjunctions and existentials. Accordingly, ≺At-out exposes the three cases only inside a truncation, and PT.rec may analyze them because the target is itself the proposition ∥ t₁ ≺ₙ t₂ ∥₁. In the code case, the slot equations move the recorded pair membership back to Rs; Rrep then reads it as the strict limit-order comparison of the two genuine codes and supplies the first branch of the naming comparison.
order-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ t₁ ≺ₙ t₂ ∥₁
order-out h = PT.rec squash₁ read (≺At-out R P s₁ a₁ e₁ s₂ a₂ e₂ γ h)
where
read : Below R P s₁ a₁ e₁ s₂ a₂ e₂ γ → ∥ t₁ ≺ₙ t₂ ∥₁
read (inl k) = ∣ inl (Rrep (codeOf t₁) (codeOf t₂)
In the arity case, the formula first says that the second skeleton slot equals the first; codeSame lifts this underlying equality to equality of the two codes in Limit. The other premise, transported through the arity-slot equations, is membership of the first arity numeral in the second. Numeral elimination converts that membership into arity t₁ < arity t₂, so equality at the first key and strict comparison at the second assemble the arity branch of _≺ₙ_.
(subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) qs₁ qs₂ (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩) qR k))) ∣₁ read (inr (q , inl k)) = ∣ inr (codeSame q , inl (#∈#-elim (arity t₁) (arity t₂)
The parameter case must first recover a common length. The formula gives an equality from the second arity slot to the first; composing it with the two slot equations yields equality of the corresponding von Neumann numerals, and #-inj′ recovers ek : arity t₂ ≡ arity t₁. With this path fixing the type of the second vector, lex-read interprets the LexAt record against the two environment graphs. Its result is an explicit first difference Lex still inside propositional truncation, exactly preserving the existential boundary of the formula.
(subst2 (λ y z → ⟨ y ∈ z ⟩) qa₁ qa₂ k))) ∣₁ read (inr (q , inr (q' , dif))) = PT.map atLex (lex-read P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek) dif) where ek : arity t₂ ≡ arity t₁
Inside that truncation, atLex completes the third case. The induction lex-vec turns the explicit first difference into the recursive vector order against the transported second vector, and vecShift removes the transport from the resulting proposition. Together with codeSame q and the recovered arity path ek, this is the parameter branch of _≺ₙ_; PT.map keeps the whole result truncated. Thus, under the two representation laws and the slot identifications, order-in constructs satisfaction of ≺At from a naming comparison, while order-out recovers only ∥ t₁ ≺ₙ t₂ ∥₁. This theorem is the adequacy of the comparison formula itself; the corresponding readings of NameAt, LeastNameAt, and StepAt require additional arguments.
ek = #-inj′ (sym qa₂ ∙ q' ∙ qa₁) atLex : Lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) → t₁ ≺ₙ t₂ atLex lx = inr (codeSame q , inr (ek , transport (vecShift ek (params t₁) (params t₂)) (lex-vec (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) lx)))