BedrockAdequacy of name comparison
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapMany definable subsets admit more than one name. An internal comparison must therefore do more than recognize a formula and its parameters: it must connect each displayed set with names that denote it, express leastness among all names of that same set, and compare the resulting least names. This chapter proves that the object-language descriptions perform exactly these tasks. In the reverse direction, the recovered names remain under propositional truncation.
{-# OPTIONS --cubical --safe --guardedness #-}
The shared prelude supplies the book's universe, proposition, finite-index, and vector conventions. The only classical hypothesis named by this chapter is the law of excluded middle. It is imported as an ordinary type and will be passed explicitly to the constructions that require it, so later uses of a satisfaction table or a name order retain an auditable assumption boundary.
open import Base.Prelude open import Base.Classical using ( LEM )
The module therefore carries lem at the successor universe level throughout. Its role is inherited through naming, the order on finite syntax codes, and uniform satisfaction; it is not a licence to extract arbitrary witnesses from propositional truncations. The adequacy proved below has an intentionally asymmetric shape: concrete names can be inserted into the formulas, while a satisfying assignment is read back only as the propositionally truncated existence of suitable names.
module L.Choice.NameComparisonAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
The semantic comparison needs one syntax and two closely related structures. Formula is the common object language, and constant relabelling moves a formula between the empty constant domain, a carrier's members, and the surrounding set universe. The structure on V supplies the ambient interpretation. Its extensionality principle will later turn pointwise agreement of membership propositions into equality of the sets denoted by two presentations.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula ) import FOL.Absoluteness open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
Names are finite syntactic data interpreted over a constructible carrier, so the proof must connect coding with L. Formula codes are sets assembled from numerals and pairs; a parameter-free code already lies in the limit stage where limitOrder can compare it. On the semantic side, constructibility and its transitivity package ambient sets as elements of the structure on L, while internal numerals, the empty constructible set, and environment graphs provide the concrete objects that the name formulas mention.
open import V.Coding {ℓ} using ( pr; module VCode ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Ordinal {ℓ} using ( #∈ω; ω-ord ) open import L.Axioms.Basic {ℓ} using ( ∅ʟ; LsetS ) open import L.Coding.Environment {ℓ} using ( env )
The model-side vocabulary expresses the data of a name without yet recovering one. envOverAt says that a candidate set is a single-valued graph with the prescribed domain, values in the carrier, and no non-pair debris; its transport lemma lets those three named sets be replaced along slot equalities. consAtL describes how an environment is enlarged by a candidate member, domAt records its length, and extAt identifies a denotation by its members. The recovery module will be crucial in the reverse direction, because the environment-graph conditions determine each parameter value uniquely.
open import L.Coding.Model {ℓ} using ( envOverAt; envOverAt-transport; domAt ) open import L.Coding.Expressions {ℓ} using ( extAt-in; extAt-out; numL; consAtL ) open import L.Coding.EnvironmentSet {ℓ} lem using ( module Recover; envS; envOver ) open import L.Coding.SatisfactionGraph {ℓ} lem using ( satGraphAt ) open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
The next bridge explains how a carrier-level formula becomes a value in the uniform satisfaction table. Constants naming members of the carrier are relabeled into the model, their assignment is represented both as an environment and as an internal graph, and the formula is addressed by a genuine key in the carrier's code set. Requiring that key to lie in AllCodes is essential: only at such a key do the graph readings force the recorded value to agree with actual satisfaction.
open import L.Coding.SatisfactionBridge {ℓ} lem using ( consAtL-in; consAtL-out; asConst; values; envFor; envFor-graph ) renaming ( graph to envGraph ) open import L.Coding.CodeSet {ℓ} lem using ( keyS; AllCodes ) open import L.Coding.UniformSatisfaction {ℓ} lem
The mathematical interface now comes into view. CanonicalNames supplies a meta-language name, its code, parameter vector, denotation, and three-key order; FiniteStageOrders supplies the order of the first key. NameComparison supplies the object-language descriptions to be justified. In particular, NameAt has exactly four conceptual conjuncts: a parameter-free skeleton, an arity numeral in ω, a parameter graph of that arity over the carrier, and an extensional account of the denotation.
using ( val-at; val-sat; keyIn; keyIn≡; keyIn∈; module Table ) open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode ) open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder ) open import L.Choice.NameComparison {ℓ} lem using ( NameAt; NameAt-in; LeastNameAt; ≺At; StepAt; StepOf; StepAt-in; StepAt-out; DenoteOf; DenoteBody; DenoteBody-in; DenoteBody-out
The rest of the imported interface separates three jobs that must not be conflated. The code, graph, and domain readings recover the data represented in slots. The Adequacy module compares two already given names by code, arity, and parameters. This chapter adds the missing statement that arbitrary satisfying slot data comes from names, and that the recovered names have the stated minimality property. It still returns those names under propositional truncation, so none of its read lemmas selects a witness. Only downstream does InternalWellOrder use leastNameOf, built from the established well-order, to obtain particular least names for the filling direction.
; FreeAt; codeFree-in; codeFree-out ; graphAt-value; graphAt-only ; domAt-numeral; domAt-fill; module Adequacy ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
Three representation changes recur in the proof. A family indexed by Fin k is tabulated as a length-indexed vector and read back entrywise. Logical equivalence between membership propositions is converted into the paths needed for set extensionality. Finally, paths between proof-carrying carriers transport formula codes and satisfaction sets whose types depend on those carriers. The empty type handles the branches that these comparisons show to be impossible.
open import Cubical.Data.Vec.Properties using ( FinVec→Vec; FinVec→Vec→FinVec ) open import Cubical.Data.Vec using ( map ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Transport using ( constSubstCommSlice ) import Cubical.Data.Empty as Empty
Propositional truncation records exactly the strength of the reverse readings. It preserves that a witness exists while forgetting which witness it was, and it can be eliminated when the target is itself a proposition. The hierarchy operations complement this discipline: ⟪ A ⟫ is the small type indexing the members of a set A, its embedding sends an index to the corresponding member, and ∈-asFiber recovers such an index from membership. Thus a uniquely determined entry of an environment can be recovered as data without turning a merely existing formula or name into chosen data.
import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber )
Arity crosses the semantic boundary through the von Neumann naturals. The meta-language number k is represented by the set-theoretic numeral # k, and ω contains precisely these numerals. Consequently the arity clause of a name can be read in either direction, and the middle key of name comparison can be expressed internally by membership of one numeral in another rather than by an additional relation parameter.
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω )
Opening the proposition-valued structure on L fixes the type S of model elements and the set-theoretic vocabulary used by every later formula. An element of S consists of an ambient set together with evidence that it is constructible. Environments therefore store proof-carrying constructible sets, while membership and equality in a formula inspect their underlying ambient sets through the structure.
open hPropStructure 𝒮ʟ
The absoluteness module relates the ambient structure on V to the structure whose elements are constructible sets. The notation γ ⊨ φ used below is the satisfaction relation in this constructible structure. Every entry of γ therefore carries both an underlying set and its constructibility proof, while the established adequacy and absoluteness lemmas connect formula satisfaction with membership and equality of the underlying sets.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
One lemma about vectors
The remaining private indices record how outer slots survive new quantifiers. If a formula introduces two witnesses before consulting an old slot, its de Bruijn index must be raised twice. The map sh2 performs exactly this shift. It is used when the denotation argument first binds a candidate member and then an extended environment, after which the original parameter-graph slot must still be found.
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
Minimality introduces a different local context. To test whether the current name is least, the object language universally binds a competing skeleton code, arity numeral, and parameter graph. Every previously available slot then lies three places farther away, and sh3 is the uniform embedding that preserves those references beneath the competitor's three data.
sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i))
Reading a denotation through the satisfaction graph creates the deepest local context used in that argument. In front of the original environment stand five new values: the candidate member, its extended environment, the environment length, the formula key, and the table value at that key. sh5 carries an outer slot across all five, allowing the graph clause to refer back to the original carrier.
sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n))))) sh5 i = suc (suc (suc (suc (suc i))))
The step formula binds two complete pieces of name data before it compares anything. Each piece consists of a skeleton code, an arity numeral, and a parameter graph, giving six new entries in total. sh6 embeds every outer slot beneath this frame, so the two least-name clauses and the final name comparison continue to speak about the same carrier, code sets, relation slots, and objects.
sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i)))))
The six fixed indices name the entries of that local frame. Because successive existential witnesses are pushed onto the front of the environment, the first name's skeleton code, arity, and parameter graph are found at indices 5, 4, and 3, while the second name's skeleton code is at index 2. Recording these positions once keeps every later occurrence aligned with the order in which the witnesses were introduced.
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)) s6b = suc (suc zero)
Indices 1 and 0 hold the second name's arity and parameter graph, completing the local environment in the order p₂, k₂, s₂, p₁, k₁, s₁ from nearest to farthest. These six bindings are the two names' data inside StepAt. They are distinct from the six outer witnesses later bound by InternalWellOrder.Stp, which describe a stage tower, its definable power set, a table value, a code set, a code order, and the empty-alphabet code set. The inner formula supplies a local name comparison to that consumer; it does not yet assert an internal well-order.
a6b = suc zero e6b = zero
The first vector lemma normalizes lookup after an entrywise map. Looking up index i in map f v gives exactly f applied to the entry of v at i. Induction on the vector proves the head case by reflexivity and reduces the tail case to the induction hypothesis. Later, this equality lets the proof move without ambiguity between carrier indices and their images as model elements.
lookup-map : {ℓ' ℓ'' : Level} {X : Type ℓ'} {Y : Type ℓ''} (f : X → Y) {k : ℕ} (v : Vec X k) (i : Fin k) → lookup i (map f v) ≡ f (lookup i v) lookup-map f (x ∷ v) zero = refl lookup-map f (x ∷ v) (suc i) = lookup-map f v i
The second vector lemma normalizes the other presentation used by recovery. Tabulating a family g : Fin k → X as FinVec→Vec g and then looking up i returns g i. This is not the converse of lookup-map; rather, the two lemmas remove two different representation layers. One exposes an entry through entrywise mapping, and the other exposes an entry through tabulation. Together they connect a recovered finite family with the parameter vector stored in a name.
lookup-tab : {ℓ' : Level} {X : Type ℓ'} {k : ℕ} (g : Fin k → X) (i : Fin k) → lookup i (FinVec→Vec g) ≡ g i lookup-tab g i j = FinVec→Vec→FinVec g j i
The chapter's frame
The local module now fixes the mathematical setting for every subsequent reading. The ambient set A is accompanied by pA, making it an element Aʟ of the constructible structure, and w is a well-order of the small type ⟪ A ⟫ indexing its members. Slot equalities involving the carrier use the proof-carrying element Aʟ because later formulas and transports depend on the model element, not merely on its first projection.
module At (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where private Aʟ : S Aʟ = A , pA
Opening Naming A w fixes the meta-language objects against which adequacy is measured. A name is a dependent triple: an arity k, a parameter-free formula with suc k variable positions, and a vector of exactly k members of A. Its code comes from the formula, and its denotation is the subset of A cut out by the formula under those parameters. The name order first compares formula codes by limitOrder, then arities by the natural-number order, and finally equal-length parameter vectors lexicographically by w. The remainder of the chapter proves that the slot descriptions recover precisely this comparison at the level of propositions, while retaining truncation and the stated minimality conditions.
module NM = Naming A w
Fixing the constructible carrier and its well-order puts two complementary interfaces side by side. Adequacy supplies the embedding of carrier members, the parameter family of a name, and the comparison module Keys; Naming supplies names together with their arity, parameter-free formula, parameter vector, and the code, extended environment, and denotation derived from those data. The relation _≺ₙ_ compares such names by their three keys.
This distinction also fixes the logical strength of the chapter. NameAt has four conceptual conjuncts, for the skeleton, arity, parameter graph, and denotation. Adequacy fills them from a given name and reads them back only as the propositionally truncated existence of a name. Minimality will be a property of a recovered name, while the choice of a particular least name occurs downstream. When InternalWellOrder uses the result, the six bindings inside StepAt, two triples of name data, remain distinct from the six outer infrastructure witnesses of Stp.
open Adequacy A pA w using ( ix; pfam; module Keys ) open NM using ( Name; arity; formula; params; codeOf; denote; environment ; _≺ₙ_ )
The parameter sequence, filled in
A parameter vector first has to cross from meta-language data to an object-language environment. The family g : Fin k → ⟪ A ⟫ gives one carrier member at each of the k indices. If slots e, a, and B hold respectively the graph of its embedded values, the numeral # k, and the carrier A, then envOverAt e a B is satisfied. Its four conditions say that the graph is single-valued, has exactly that finite domain, takes values in the carrier, and contains only ordered pairs.
paramSeq-in : ∀ {n} (e a B : Fin n) (γ : S ^ n) (k : ℕ) (g : Fin k → ⟪ A ⟫) → fst (lookup e γ) ≡ env (λ i → ix (g i)) → fst (lookup a γ) ≡ # k → fst (lookup B γ) ≡ A → ⟨ γ ⊨ envOverAt e a B ⟩
These four graph properties need not be proved again after the three sets have been placed in arbitrary slots. The canonical environment with entries Aʟ, # k, and envS Aʟ g already satisfies them at indices two, one, and zero. envOverAt-transport carries that satisfaction to γ along the three given equalities. The equalities are reversed because the transport starts at the canonical sets and ends at the sets stored in the requested slots.
paramSeq-in e a B γ k g qe qa qB = envOverAt-transport (Aʟ ∷ (# k , numL k) ∷ envS Aʟ g ∷ []) γ (suc (suc zero)) (suc zero) zero e a B (sym qe) (sym qa) (sym qB) (envOver Aʟ g)
And read back as a vector
For the reverse reading, the arity and carrier slots are fixed by qa and qB, while h asserts that the set in slot e satisfies the environment conditions. No graph presentation is assumed for e; finding one is precisely the task. Opening Recover with these data exposes a family indexed by Fin k and a proof that its canonical graph is the original set.
module _ {n : ℕ} (e a B : Fin n) (γ : S ^ n) (k : ℕ) (qa : fst (lookup a γ) ≡ # k) (qB : fst (lookup B γ) ≡ A) (h : ⟨ γ ⊨ envOverAt e a B ⟩) where private module R = Recover Aʟ k γ e a B qa qB h
The recovered family is genuine data, so it can be tabulated as a vector of length k. This does not remove a truncation by choice. At each index, the domain condition merely supplies an entry, but single-valuedness makes the type of entries a proposition; elimination of propositional truncation into that proposition therefore yields the unique entry. Its value lies in A, and the carrier's membership fibre supplies the corresponding element of ⟪ A ⟫ without truncation. Applying FinVec→Vec to these elements produces paramSeq-out.
paramSeq-out : Vec ⟪ A ⟫ k
paramSeq-out = FinVec→Vec R.g
Tabulation changes the presentation of the family, so the graph equation closes the round trip. R.recovers identifies the set in slot e with the graph of the recovered finite family. The lookup law for FinVec→Vec then identifies each entry of the tabulated vector with the corresponding family value; function extensionality and congruence of env lift those pointwise paths to an equality of graphs. Thus the recovered vector presents exactly the original environment set, including the absence of extraneous members guaranteed by the ordered-pair condition.
paramSeq-graph : fst (lookup e γ) ≡ env (λ i → ix (lookup i paramSeq-out)) paramSeq-graph = R.recovers ∙ cong env (funExt (λ i → cong ix (sym (lookup-tab R.g i))))
Four elements, sealed where they are made
The denotation clause has four existential witnesses of its own, distinct from the four conceptual conjuncts of NameAt. The first witness is the environment obtained from a name t and a candidate carrier member m: place m before the parameter vector of t, then represent that extended assignment as an element of the model. The construction envFor Aʟ includes the required proof of constructibility, so envAt t m can occupy an object-language slot.
opaque envAt : Name → ⟪ A ⟫ → S envAt t m = envFor Aʟ (environment t m)
The object-language formulas inspect the underlying set of that model element. The equation envAt-fst identifies it with envGraph Aʟ (environment t m), the canonical graph of the candidate followed by the parameters. This is the exact presentation needed both by the formula that adjoins the candidate to the old parameter environment and by the formula that checks the domain of the extended environment.
envAt-fst : (t : Name) (m : ⟪ A ⟫) → fst (envAt t m) ≡ envGraph Aʟ (environment t m) envAt-fst t m = envFor-graph Aʟ (environment t m)
The second witness represents a natural number inside the constructible model. numAt j pairs the von Neumann numeral # j with its constructibility proof numL j. In the denotation argument it will be used at j = suc (arity t), because the extended environment contains the candidate in addition to the arity t parameters.
numAt : ℕ → S numAt j = # j , numL j
Projecting the underlying set of numAt j returns # j definitionally, so numAt-fst is reflexivity. This simple equation is what connects the meta-language length of the extended vector with the set-theoretic numeral seen by domAt; no decoding of a numeral is needed in this filling direction.
numAt-fst : (j : ℕ) → fst (numAt j) ≡ # j numAt-fst j = refl
The third witness is the key at which uniform satisfaction stores the formula of the name. Since formula t has no constants, embed (formula t) regards it as a formula whose constant alphabet is the member type of A; no constant is actually introduced. keyIn Aʟ packages the resulting formula key as a constructible model element, giving keyAt t.
keyAt : Name → S keyAt t = keyIn Aʟ (embed (formula t))
The packaged key and the key used by the code-set interface have the same underlying set. The equation keyAt-fst states precisely that fst (keyAt t) is fst (keyS Aʟ (embed (formula t))). This lets later membership and graph arguments use the abstract model element while reasoning about the concrete ordered-pair code supplied by keyS.
keyAt-fst : (t : Name) → fst (keyAt t) ≡ fst (keyS Aʟ (embed (formula t))) keyAt-fst t = keyIn≡ Aʟ (embed (formula t))
The same key is certified to belong to AllCodes Aʟ. This membership is a semantic condition, not redundant bookkeeping: the satisfaction graph is required to have the intended value at genuine formula keys, whereas its behaviour away from the code domain is irrelevant. Thus keyAt-∈ is what allows the table value at keyAt t to be read as satisfaction of the formula of t.
keyAt-∈ : (t : Name) → ⟨ keyAt t ∈ˢ AllCodes Aʟ ⟩ keyAt-∈ t = keyIn∈ Aʟ (embed (formula t))
The fourth witness is the value selected by the uniform satisfaction table at that genuine key. Table.val Aʟ Aʟ takes both the key and its membership in the code domain, and returns a constructible model element. Its underlying set will later be identified by val-sat with exactly the encoded environments over A that satisfy embed (formula t); here valAt records the table lookup needed for that identification.
valAt : Name → S valAt t = Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t)
Because valAt t is defined by that table lookup, valAt-val is reflexivity. Keeping the equation explicit lets the denotation argument pass cleanly between the named fourth witness and the general theorem about Table.val. Together, the four constructions now provide exactly the witnesses bound by DenoteOf: an extended environment, its length numeral, a genuine formula key, and the table value at that key.
valAt-val : (t : Name) → valAt t ≡ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) valAt-val t = refl
What the key of a name's formula is
To compare the description's key with the table's key, first observe what relabeling does to a parameter-free formula. The formula χ has constants in the empty type. Embedding it directly into the ambient universe and first embedding it into the carrier and then mapping carrier members into the universe therefore use two functions with the same empty domain. Function extensionality makes those functions equal, and the composition law for mapFo yields sameEmbed χ. This is a fact about the empty constant alphabet, not a claim that arbitrary relabeling leaves arbitrary formulas unchanged.
private sameEmbed : ∀ {m} (χ : Formula (⊥* {ℓ}) m) → mapFo ⟪ A ⟫↪ (embed χ) ≡ embed χ sameEmbed χ = mapFo-comp Empty.rec* ⟪ A ⟫↪ χ ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))
The table key of a formula with m variable positions is an ordered pair: the numeral # m and the code of the formula after its constants have been mapped into the ambient universe. By sameEmbed, that mapped formula is the direct embedding of χ, whose code is the underlying set of limitCode χ. Congruence of the coding operation therefore gives keyCode. For a name, where m = suc (arity t), this is exactly the equality that will align the table key with the pair formed from the extended-environment length and the skeleton code.
keyCode : ∀ {m} (χ : Formula (⊥* {ℓ}) m)
→ fst (keyS Aʟ (embed χ)) ≡ pr (# m) (fst (limitCode χ))
keyCode χ = cong (λ u → pr (# _) VCode.⌜ u ⌝) (sameEmbed χ)
The denotation proof also needs the parameter environment in two equivalent presentations. The family pfam t sends each finite index to the ambient set underlying the corresponding parameter. Alternatively, mapping the naming embedding NM.DA.ι over params t gives a vector of model elements, whose canonical graph is envGraph Aʟ. The lookup law for vector mapping identifies their values pointwise; function extensionality and congruence of env then give valuesOf t, an equality of the two environment graphs.
valuesOf : (t : Name) → env (pfam t) ≡ envGraph Aʟ (map NM.DA.ι (params t)) valuesOf t = cong env (funExt (λ i → sym (cong fst (lookup-map NM.DA.ι (params t) i))))
Every entry of the extended environment is constructible. An index i : Fin (suc (arity t)) selects either the candidate or one of the parameters, and in either case lookup i (environment t m) already carries proof that its underlying set belongs to A. Since A is constructible, transitivity of constructibility yields valuesL t m i. This pointwise fact supplies the constructibility premise needed when domAt verifies the domain of the extended environment.
valuesL : (t : Name) (m : ⟪ A ⟫) (i : Fin (suc (arity t))) → ⟨ isL (values Aʟ (environment t m) i) ⟩ valuesL t m i = isL-trans (snd (lookup i (environment t m))) pA
The denotation, both ways
Before comparing denotation membership with the object-language clause, one must know that every member of denote t lies in the carrier. Membership in this denotation merely presents a carrier index mm whose extended environment satisfies the formula, together with a path from the represented carrier member to the ambient set y. The witness is propositionally truncated, but the goal y ∈ A is itself a proposition, so PT.rec may use that witness without selecting or retaining an index.
private denoteMem : (t : Name) (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ A ⟩ denoteMem t y = PT.rec (snd (y ∈ A)) step where step : Σ[ p ∈ Σ[ mm ∈ ⟪ A ⟫ ] ⟨ NM.satAt t mm ⟩ ] (⟪ A ⟫↪ (p .fst) ≡ y)
Inside the permitted truncation elimination, the recovered package is a pair p and an equality q. Its first component is a concrete member index of A, so the canonical small-membership witness, converted by ∈∈ₛ, proves that its embedded image belongs to A. Transporting this membership along q proves y ∈ A. The argument uses only the presentation of membership and the fact that its target is a proposition; it introduces neither a choice function nor a new classical step.
→ ⟨ y ∈ A ⟩ step (p , q) = subst (λ u → ⟨ u ∈ A ⟩) q (∈∈ₛ {a = ⟪ A ⟫↪ (p .fst)} {b = A} .snd (∈ₛ⟪ A ⟫↪ (p .fst)))
The module Named now fixes the slots in which the four pieces of NameAt will be compared with a meta-language name: carrier B, the carrier code set C, the empty-alphabet code set C₀, skeleton s, arity a, parameter graph e, and denotation d. The carrier equation qB is an equality of complete model elements, including their constructibility proofs, whereas qC and q₀ identify only underlying sets. The difference is forced by use: formulas below are typed over the member type of the model element in slot B, while code-set membership observes only the underlying sets in C and C₀.
module Named {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) (qB : lookup B γ ≡ Aʟ) (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ)) (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where private
This dependence on the carrier is isolated in Fo. For a model element X and an arity j, Fo X j is the type of formulas whose constants range over the small member type ⟪ fst X ⟫. Thus a formula read over the carrier stored in a slot has the correct type before any semantic comparison is made; the carrier cannot be replaced merely by an equality of underlying sets after the fact.
Fo : S → ℕ → Type ℓ Fo X j = Formula ⟪ fst X ⟫ j
For a name t, the parameter-free formula t is first embedded into formulas whose constants may range over members of the fixed carrier A; because the original constant domain is empty, this adds no actual parameter. Its type is then transported along sym qB from Fo Aʟ to Fo (lookup B γ), producing ψAt t. The transport is possible because qB identifies the complete carrier elements. This slot-relative formula is the one whose key and satisfaction value can now be compared with the fixed-carrier constructions above.
ψAt : (t : Name) → Fo (lookup B γ) (suc (arity t)) ψAt t = subst (λ X → Fo X (suc (arity t))) (sym qB) (embed (formula t))
The formula used by the description is first transported from the fixed carrier Aʟ to the carrier stored in slot B. Since the formula type itself depends on the carrier, qB must identify the complete proof-carrying carrier, not only its underlying set. Path induction on qB then shows that forming the code-set key commutes with this transport. Thus the key computed from ψAt t at the slot carrier is the same set as the key of embed (formula t) at Aʟ.
keyψ : (t : Name) → fst (keyS (lookup B γ) (ψAt t)) ≡ fst (keyS Aʟ (embed (formula t))) keyψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ) (λ X ψ → fst (keyS X ψ)) (sym qB) (embed (formula t)))
The same dependence occurs for the value of uniform satisfaction. At the slot carrier, the relevant set is Sat applied to the transported formula after its constants have been relabelled into that carrier. At Aʟ, it is Sat applied to the correspondingly relabelled embedded formula. Substitution along qB commutes with this whole construction, so the two satisfaction sets have equal underlying sets.
satψ : (t : Name)
→ fst (Sat (lookup B γ) (mapFo (asConst (lookup B γ)) (ψAt t)))
≡ fst (Sat Aʟ (mapFo (asConst Aʟ) (embed (formula t))))
satψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ)
(λ X ψ → fst (Sat X (mapFo (asConst X) ψ)))
The final argument to the path-induction principle is the embedded formula itself. This closes the proof of satψ without making any independent semantic choice: the equality follows solely by substituting the carrier in a dependent construction. Together, keyψ and satψ let the denotation argument pass between the slot carrier and Aʟ while keeping both the formula key and its satisfaction set aligned.
(sym qB) (embed (formula t)))
For a fixed meta-language name t, Data t records the four slot equalities needed to represent it. The skeleton slot contains the underlying set of codeOf t; the arity slot contains # (arity t); the parameter slot contains the environment graph env (pfam t); and the denotation slot contains denote t. These four equations mirror the four conceptual conjuncts of NameAt. They assert that the current slots are aligned with this particular name; they do not assert that all names with a given denotation are unique.
Data : Name → Type (ℓ-suc ℓ) Data t = (fst (lookup s γ) ≡ fst (codeOf t)) × ( (fst (lookup a γ) ≡ # (arity t)) × ( (fst (lookup e γ) ≡ env (pfam t)) × (fst (lookup d γ) ≡ denote t) ) )
To compare the denotation clause with denote t, the module Body fixes t and the first three components of Data t. The skeleton equality qs aligns the formula key, and the parameter equality qe aligns the parameter graph. The arity equality qa records the remaining slot alignment for the same name; once t is fixed, the denotation argument obtains the extended length directly as suc (arity t). The private vector δp presents the parameters in the restricted semantic carrier required by the satisfaction bridge.
module Body (t : Name) (qs : fst (lookup s γ) ≡ fst (codeOf t))
(qa : fst (lookup a γ) ≡ # (arity t))
(qe : fst (lookup e γ) ≡ env (pfam t)) where
private
δp : Vec NM.DA.SM (arity t)
The parameters of a name already lie in the small member type ⟪ A ⟫. Mapping NM.DA.ι over them does something more precise than merely retaining their indices: it equips each represented set with its membership in A, making an element of the restricted model carrier NM.DA.SM. The resulting vector δp has length arity t and is therefore the exact tail of the inner environment at which the name's formula will be evaluated.
δp = map NM.DA.ι (params t)
The slot equation qe describes the same parameters through the external family pfam t, whereas the satisfaction bridge expects the graph of the restricted-carrier vector δp. The equality valuesOf t identifies these two presentations entry by entry. Composing it with qe gives qd', which says that the parameter slot contains exactly envGraph Aʟ δp. This is the form needed both to build an extended environment and to recognize one later.
qd' : fst (lookup e γ) ≡ envGraph Aʟ δp qd' = qe ∙ valuesOf t
The fourth condition in the denotation payload identifies its key. Starting from the sealed keyAt t, keyAt-fst exposes the code-set key of the embedded formula, and keyCode computes that key as the ordered pair of # (suc (arity t)) with the formula's limit-stage code. The skeleton equation qs replaces this second component by the set in slot s. What remains is to express the first component through the sealed length numeral.
qkey : fst (keyAt t) ≡ pr (fst (numAt (suc (arity t)))) (fst (lookup s γ)) qkey = keyAt-fst t ∙ keyCode (formula t) ∙ cong (pr (# (suc (arity t)))) (sym qs) ∙ cong (λ u → pr u (fst (lookup s γ)))
The last congruence uses numAt-fst in the reverse direction, replacing the set-theoretic numeral by the underlying set of numAt (suc (arity t)) inside the ordered pair. The completed equation qkey therefore has exactly the form required by DenoteOf: the chosen key is the pair of the chosen domain numeral and the skeleton slot. In the reverse proof, the same calculation will be reconstructed from the payload's key equation.
(sym (numAt-fst (suc (arity t))))
The forward direction begins with an actual member m : ⟪ A ⟫, an ambient element z presenting the same underlying set, and a proof that this set lies in denote t. It supplies the four witnesses of DenoteOf in semantic order: the environment obtained by adjoining m to the parameters, its length numeral, the formula key, and the table value at that key. Six conditions link these witnesses. Five describe their shape and alignment; the sixth converts the assumed denotation membership into membership of the environment in the table value.
denote-fill : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ fst z → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩ → DenoteOf B C s e γ z denote-fill z m qm hz = envAt t m , (numAt (suc (arity t)) , (keyAt t , (valAt t , ( hcons , (hdom , (hkey , (qkey , (hgraph , hmem))))))))
The first condition says that the chosen environment is obtained by adjoining the candidate member to the parameter environment. The inward reading of consAtL receives qd' for the old parameter graph, sym qm for the candidate stored in slot z, and envAt-fst t m for the newly constructed graph. It then proves the object-language extension formula. This establishes that the formula will be evaluated with the candidate in its extra variable slot and the original parameters following it.
where hcons : ⟨ (envAt t m ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩ hcons = consAtL-in Aʟ δp (NM.DA.ι m) (envAt t m ∷ z ∷ γ) zero (suc zero) (sh2 e) qd' (sym qm) (envAt-fst t m)
The second condition fixes the domain of that extended environment. Its length is suc (arity t): one position for the candidate, followed by arity t parameter positions. The inward adequacy lemma for domAt is given the underlying values of environment t m and a proof that each value is constructible. The latter follows from membership in the constructible carrier and transitivity of L.
hdom : ⟨ (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩ hdom = domAt-fill (suc zero) zero (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) (suc (arity t)) (values Aʟ (environment t m)) (valuesL t m)
The same domain lemma must also see the chosen witnesses as the sets it is meant to compare. The equality envAt-fst t m exposes the environment graph underlying envAt t m, while numAt-fst (suc (arity t)) exposes the expected von Neumann numeral under the length witness. With these two projections, the domain formula states exactly that the numeral codes the length of the chosen environment.
(envAt-fst t m) (numAt-fst (suc (arity t)))
The third condition places the chosen key in the genuine code domain. The constructor keyAt already provides membership in AllCodes Aʟ; the slot equation qC transports this membership to the set stored in slot C. This hypothesis cannot be omitted. The satisfaction graph is forced to carry the semantic value of a formula at genuine code keys, whereas its behavior outside the code domain need not determine such a value.
hkey : ⟨ fst (keyAt t) ∈ fst (lookup C γ) ⟩ hkey = subst (λ u → ⟨ fst (keyAt t) ∈ u ⟩) (sym qC) (keyAt-∈ t)
The fifth condition says that the chosen value is the value admitted by the satisfaction graph at the chosen key. The graph formula is evaluated after five new entries have been placed before the ambient assignment: value, key, length numeral, extended environment, and candidate. Its first alignment hypothesis identifies the underlying set of keyAt t with the key of ψAt t at the slot carrier. This is exactly where keyψ carries the earlier key calculation across qB.
hgraph : ⟨ (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩ hgraph = graphAt-value (sh5 B) (suc zero) zero (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ) (ψAt t)
The second alignment hypothesis identifies the chosen value. First valAt-val exposes it as the table value at keyAt t. The law val-at identifies that table value with the Sat set of the embedded formula over Aʟ. Finally satψ, read in the required direction, transports this set to the slot carrier. The two alignment equations now allow graphAt-value to establish the graph condition without changing either the key or its semantic value.
(keyAt-fst t ∙ sym (keyψ t)) ( cong fst (valAt-val t) ∙ cong fst (val-at Aʟ Aʟ (embed (formula t)) (keyAt t) (keyAt-∈ t) (keyAt-fst t)) ∙ sym (satψ t) )
The sixth condition is the decisive membership: the encoded extended environment must belong to the selected graph value. The hypothesis says that the member represented by m lies in denote t. The characterization NM.denote-mem t m turns this into inner satisfaction of embed (formula t) by environment t m. Thus denotation membership supplies exactly the semantic fact that the uniform table is designed to record.
hmem : ⟨ fst (envAt t m) ∈ fst (valAt t) ⟩
hmem = subst (λ u → ⟨ envAt t m ∈ˢ u ⟩) (sym (valAt-val t)) inTable
where
inner : ⟨ NM.DA._⊨ᵐ_ (environment t m) (embed (formula t)) ⟩
inner = subst ⟨_⟩ (NM.denote-mem t m) hz
The law val-sat identifies that inner satisfaction with membership of envAt t m in the table value at keyAt t; it is read backwards here because the proof starts from satisfaction. Transport along valAt-val then replaces the explicit table value by the sealed witness valAt t. This proves the sixth condition and completes denote-fill: all four witnesses and all six relations among them have been obtained from the data of t and the assumed membership in its denotation.
inTable : ⟨ envAt t m ∈ˢ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) ⟩
inTable = subst ⟨_⟩
(sym (val-sat Aʟ (embed (formula t)) (keyAt t) (keyAt-∈ t)
(keyAt-fst t) (environment t m) (envAt t m)
(envAt-fst t m))) inner
For the reverse direction, suppose an explicit DenoteOf payload is given for z: four bound elements together with the six conditions just described. The goal is to prove that the member m represented by z belongs to denote t. By the reverse direction of NM.denote-mem, it is enough to reconstruct inner satisfaction of the embedded formula at environment t m. The remaining equalities successively identify the arbitrary environment, numeral, key, and value supplied by the payload.
denote-read : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ fst z
→ DenoteOf B C s e γ z → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩
denote-read z m qm (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
= subst ⟨_⟩ (sym (NM.denote-mem t m)) inner
where
The extension condition is read first. Its outward adequacy theorem compares the old graph qd', the candidate identification sym qm, and the satisfaction proof hc. It follows that the underlying set of the arbitrary witness c is exactly envGraph Aʟ (environment t m). Thus the first existential witness is not merely some extension of the parameter graph: its graph is the canonical environment obtained by putting m before the parameters of t.
qcg : fst c ≡ envGraph Aʟ (environment t m) qcg = consAtL-out Aʟ δp (NM.DA.ι m) (c ∷ z ∷ γ) zero (suc zero) (sh2 e) qd' (sym qm) hc
The domain condition then determines the numeral witness. Since qcg identifies c with the graph of environment t m, domAt-numeral reads hk as an equality between the underlying set of k and the numeral for that environment's length. The length is suc (arity t), and valuesL supplies the constructibility needed by the domain adequacy theorem. Hence fst k ≡ # (suc (arity t)).
qk : fst k ≡ # (suc (arity t)) qk = domAt-numeral (suc zero) zero (k ∷ c ∷ z ∷ γ) (suc (arity t)) (values Aʟ (environment t m)) (valuesL t m) qcg hk
The payload's fourth condition hp says that its key is the pair of its own domain witness k and the skeleton slot. Rewriting the first component by qk and the second by qs gives the pair of # (suc (arity t)) with the formula code. Finally, keyCode (formula t) is read backwards to recognize this pair as the code-set key of embed (formula t). The resulting equality qkey' identifies the arbitrary payload key with the genuine formula key.
qkey' : fst key ≡ fst (keyS Aʟ (embed (formula t))) qkey' = hp ∙ cong (λ u → pr u (fst (lookup s γ))) qk ∙ cong (pr (# (suc (arity t)))) qs ∙ sym (keyCode (formula t))
The membership condition hi says that this recovered key belongs to the set stored in slot C. Transport along qC turns it into membership in AllCodes Aʟ, producing key∈. This is a membership proof, not a choice of a new key: the key has already been supplied by the DenoteOf payload and identified by qkey'. Its role is to put that key inside the domain where the uniform table and the satisfaction graph have their semantic specification.
key∈ : ⟨ key ∈ˢ AllCodes Aʟ ⟩ key∈ = subst (λ u → ⟨ fst key ∈ u ⟩) qC hi
It remains to identify the arbitrary value witness v. The uniqueness reading graphAt-only applies to the graph proof hg once qkey' and keyψ have aligned its key with ψAt t at the slot carrier. It first identifies fst v with the corresponding Sat set. The transport satψ moves that set back to Aʟ, and val-at, read backwards, identifies it with Table.val Aʟ Aʟ key key∈. Thus qval recovers the table value required to turn the final membership hm into inner satisfaction in the next step.
qval : fst v ≡ fst (Table.val Aʟ Aʟ key key∈) qval = graphAt-only (sh5 B) (suc zero) zero (v ∷ key ∷ k ∷ c ∷ z ∷ γ) (ψAt t) (qkey' ∙ sym (keyψ t)) hg ∙ satψ t ∙ sym (cong fst (val-at Aʟ Aʟ (embed (formula t)) key key∈ qkey'))
The last component of DenoteOf says that the extended environment c belongs to the recovered value v. The path qval identifies this value with the uniform satisfaction table at the recovered code key. Transporting membership along that path therefore gives exactly the table membership required for the next semantic reading.
inTable : ⟨ c ∈ˢ Table.val Aʟ Aʟ key key∈ ⟩
inTable = subst (λ u → ⟨ fst c ∈ u ⟩) qval hm
The adequacy equation val-sat now reads membership in that table value as satisfaction of the embedded formula. Its hypotheses use qkey' to identify the recovered key and qcg to identify c with the graph of the extended environment. Thus inner states that environment t m satisfies the formula of t; the enclosing result then uses denote-mem in reverse to recover membership in denote t.
inner : ⟨ NM.DA._⊨ᵐ_ (environment t m) (embed (formula t)) ⟩ inner = subst ⟨_⟩ (val-sat Aʟ (embed (formula t)) key key∈ qkey' (environment t m) c qcg) inTable
The preceding readings were stated for a member m of the carrier. The lemma member-fill reformulates the forward reading for an arbitrary constructible element z: membership of its underlying set in denote t implies both membership in the carrier slot and the full witness package DenoteOf. The first conclusion is transported from actual membership in A along the slot equation qB.
member-fill : (z : S) → ⟨ fst z ∈ denote t ⟩ → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z member-fill z hz = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (cong fst qB)) hA , denote-fill z (fib .fst) (fib .snd) (subst (λ u → ⟨ u ∈ denote t ⟩) (sym (fib .snd)) hz)
To apply the member-level lemma, one must recover the carrier member represented by z. The containment lemma denoteMem first turns membership in the denotation into membership in A. The fibre presentation of membership then provides an m : ⟪ A ⟫ together with the equation ⟪ A ⟫↪ m ≡ fst z; this is ordinary dependent data, so no choice principle or truncation elimination is involved.
where hA : ⟨ fst z ∈ A ⟩ hA = denoteMem t (fst z) hz fib : Σ[ mm ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ fst z) fib = ∈-asFiber {a = fst z} {b = A} hA
The converse reformulation starts with membership of z in the carrier slot and a DenoteOf package. After recovering the represented carrier member, the earlier lemma denote-read turns that package into membership of the embedded member in denote t. Transport along the fibre equation changes this conclusion back into membership of fst z.
member-read : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩
→ DenoteOf B C s e γ z → ⟨ fst z ∈ denote t ⟩
member-read z hz hDen = subst (λ u → ⟨ u ∈ denote t ⟩) (fib .snd)
(denote-read z (fib .fst) (fib .snd) hDen)
where
Here the required fibre comes from the carrier-slot hypothesis. The equation qB identifies the underlying set in that slot with A, so transport first produces fst z ∈ A; ∈-asFiber then returns the corresponding member of ⟪ A ⟫ and its embedding equation. Consequently the two member lemmas apply to every element of the model that satisfies the relevant membership hypothesis, not only to an element already presented in the small carrier type.
fib : Σ[ mm ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ fst z) fib = ∈-asFiber {a = fst z} {b = A} (subst (λ u → ⟨ fst z ∈ u ⟩) (cong fst qB) hz)
A name, assembled
For a fixed name t, Data t records four equations: the skeleton slot is its formula code, the arity slot is its numeral, the environment slot is its parameter graph, and the denotation slot is denote t. NameAt-fill uses these equations to establish the four conceptual conjuncts of NameAt: freeness from constants, membership of the arity in ω, the environment condition, and the extensional characterization of the denotation. The last conjunct is supplied by its two membership directions into and back.
NameAt-fill : (t : Name) → Data t → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ NameAt-fill t (qs , (qa , (qe , qd))) = NameAt-in B C C₀ s a e d γ hf ha he into back where module Bt = Body t qs qa qe
The first conjunct is obtained from the actual parameter-free formula carried by t. Its formula has suc (arity t) variable positions, and qs identifies its limit-stage code with the skeleton slot. With qa identifying the arity slot and q₀ identifying the empty-alphabet code set, codeFree-in turns precisely this formula and code equation into satisfaction of FreeAt.
hf : ⟨ γ ⊨ FreeAt C₀ s a ⟩
hf = codeFree-in C₀ s a γ (arity t) q₀ qa (formula t) qs
The arity conjunct requires only membership in ω. The canonical fact #∈ω (arity t) supplies membership of the numeral, and the equation qa transports it to the value stored in the arity slot. No comparison relation is used in this part of the description.
ha : ⟨ fst (lookup a γ) ∈ ω ⟩ ha = subst (λ u → ⟨ u ∈ ω ⟩) (sym qa) (#∈ω (arity t))
For the environment conjunct, the parameter vector of t is viewed as the family i ↦ lookup i (params t). Its graph equation is qe, its domain numeral equation is qa, and qB identifies its codomain carrier with Aʟ. paramSeq-in transports the standard environment property of this family to the three slots, yielding satisfaction of envOverAt.
he : ⟨ γ ⊨ envOverAt e a B ⟩ he = paramSeq-in e a B γ (arity t) (λ i → lookup i (params t)) qe qa (cong fst qB)
The forward direction of the extensional conjunct begins with an element of the denotation slot. Transport along qd makes it a member of denote t. Bt.member-fill then supplies exactly the two parts of the denotation body: membership in the carrier slot and the witness package DenoteOf.
into : (z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩ → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z into z hz = Bt.member-fill z (subst (λ u → ⟨ fst z ∈ u ⟩) qd hz)
Conversely, carrier membership together with DenoteOf is read by Bt.member-read as membership in denote t. Transport along the inverse of qd places the element back in the denotation slot. These two functions are the two directions required by the single extensional conjunct of NameAt.
back : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z → ⟨ fst z ∈ fst (lookup d γ) ⟩ back z hzB hDen = subst (λ u → ⟨ fst z ∈ u ⟩) (sym qd) (Bt.member-read z hzB hDen)
The reverse reading of NameAt returns only the propositional truncation of a name with its four data equations. The arity conjunct ha is membership in ω; its semantic presentation supplies, under propositional truncation, a natural number k and an equation identifying the arity slot with # k. PT.rec may inspect that witness because the final result is itself a propositionally truncated type.
NameAt-read : ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ → ∥ Σ[ t ∈ Name ] Data t ∥₁ NameAt-read (hf , (ha , (he , hd))) = PT.rec squash₁ atArity ha where atCode : (k : ℕ) (qa : fst (lookup a γ) ≡ # k)
Once k and the arity equation qa are fixed, codeFree-out reads the freeness conjunct. It yields, still under propositional truncation, a formula χ : Formula ⊥* (suc k) and an equation qs from the skeleton slot to its limit-stage code. Inside this branch, atCode assembles the name and returns its data: qs is the first equation and qa is the second.
→ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ] (fst (lookup s γ) ≡ fst (limitCode χ)) → Σ[ t ∈ Name ] Data t atCode k qa (χ , qs) = t , (qs , (qa , (qe , qd))) where
The parameter component is recovered directly once the arity is known. paramSeq-out reads he using qa and the carrier equation qB, producing a vector of length k in ⟪ A ⟫; together with k and χ, this vector defines the name t. This recovery is untruncated at the level of the vector, although the whole construction remains inside the truncations introduced by the arity and formula readings.
t : Name t = k , (χ , paramSeq-out e a B γ k qa (cong fst qB) he)
The recovered vector must also satisfy the environment equation recorded in Data t. The companion lemma paramSeq-graph states that the original environment slot is exactly the encoded graph env (pfam t) of this vector. This path is the third data equation qe.
qe : fst (lookup e γ) ≡ env (pfam t) qe = paramSeq-graph e a B γ k qa (cong fst qB) he
The local module Bt instantiates the denotation-body readings at the recovered name and at its first three data equations qs, qa, and qe. The remaining component of Data t is therefore the set equality between the denotation slot and denote t. It will be proved by comparing their members in both directions.
module Bt = Body t qs qa qe
For the forward inclusion, let y belong to the denotation slot. Since that slot is an element of the model, transitivity of L makes y constructible, so it can be packaged as z : S. Reading the extensional conjunct hd outward gives carrier membership and a propositionally truncated DenoteOf witness. The target y ∈ denote t is a proposition, so PT.rec may apply Bt.member-read to any representative of that witness.
fwd : (y : V ℓ) → ⟨ y ∈ fst (lookup d γ) ⟩ → ⟨ y ∈ denote t ⟩ fwd y hy = PT.rec (snd (y ∈ denote t)) (Bt.member-read z (body .fst)) (body .snd) where z : S
The value body is obtained in two semantic steps. First extAt-out turns membership in the denotation slot into satisfaction of DenoteBody; then DenoteBody-out exposes its carrier conjunct and the four existential witnesses collected in DenoteOf. Those witnesses remain propositionally truncated, as required by the semantics of the existential quantifiers, and are consumed only inside the proposition-valued membership proof above.
z = y , isL-trans hy (snd (lookup d γ)) body : ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf B C s e γ z ∥₁ body = DenoteBody-out B C s e γ z (extAt-out d (DenoteBody B C s e) γ hd z hy)
For the reverse inclusion, assume y ∈ denote t. The proof will first regard y as an element z : S, then use Bt.member-fill to construct the denotation body at z. The introduction lemmas DenoteBody-in and extAt-in rebuild the body satisfaction and finally membership in the denotation slot.
bwd : (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ fst (lookup d γ) ⟩ bwd y hy = extAt-in d (DenoteBody B C s e) γ hd z (DenoteBody-in B C s e γ z (body .fst) (body .snd)) where z : S
The constructibility proof for z comes from two containments already known: denoteMem puts every member of denote t in A, and pA says that A is constructible. With this z, Bt.member-fill produces carrier membership and an untruncated DenoteOf package. Hence the reverse inclusion does not need to eliminate any propositional truncation.
z = y , isL-trans (denoteMem t y hy) pA body : ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z body = Bt.member-fill z hy
The functions fwd y and bwd y give the two implications between the membership propositions for every set y. Since both sides are propositions, ⇔toPath turns these implications into an equality of truth values. Extensionality for V then turns the pointwise membership equality into fst (lookup d γ) ≡ denote t, the fourth equation qd.
qd : fst (lookup d γ) ≡ denote t qd = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
The branch atArity combines the two truncations without selecting global witnesses. Its input presents the arity as a lifted natural number; reversing qk gives the equation expected by atCode. Then codeFree-out supplies the formula and code equation under propositional truncation, and PT.map applies atCode within that truncation. The result is merely a name satisfying all four data equations, exactly the codomain of NameAt-read.
atArity : Σ[ lk ∈ Lift {ℓ-zero} {ℓ} ℕ ] (# (lower lk) ≡ fst (lookup a γ)) → ∥ Σ[ t ∈ Name ] Data t ∥₁ atArity (lk , qk) = PT.map (atCode (lower lk) (sym qk)) (codeFree-out C₀ s a γ (lower lk) q₀ (sym qk) hf)
Least, described and meant
The least-name formula quantifies over the three pieces that describe a competing name. The first packaged element, codeEl t, places the formula code of t in the model: codeOf t belongs to the limit stage Lset ω, and that stage is constructible, so transitivity of L proves the code constructible. The opaque definition exposes only the underlying-set equation codeEl-fst, which is all later satisfaction arguments need when instantiating the universal clause at a particular competitor.
opaque codeEl : Name → S codeEl t = fst (codeOf t) , isL-trans (snd (codeOf t)) (snd (LsetS ω ω-ord))
The element codeEl t carries the formula code of a name into the model. Its first projection is definitionally the underlying set of codeOf t, so the equation needed when the universal clause is instantiated is reflexivity. The constructibility proof stored in the second projection does not alter that code.
codeEl-fst : (t : Name) → fst (codeEl t) ≡ fst (codeOf t) codeEl-fst t = refl
The parameter data of a name are represented by a second model element. For t, the family i ↦ lookup i (params t) selects the carrier element at each of its arity t positions, and envS Aʟ turns that family into its coded environment graph. Thus envEl t has exactly the form expected by the environment slot of NameAt.
envEl : Name → S envEl t = envS Aʟ (λ i → lookup i (params t))
Unfolding the environment wrapper gives the graph env (pfam t), because pfam t is precisely the family obtained by looking up the entries of params t. Hence envEl-fst is again reflexivity. Together with codeEl-fst and the earlier equation for numAt, this supplies the three slot equations used to insert a concrete name into a quantified competitor.
envEl-fst : (t : Name) → fst (envEl t) ≡ env (pfam t) envEl-fst t = refl
The least described name is the least name
Two strict well-orders enter the name comparison. The notation _≺ˡ_ denotes limitOrder on formula codes, while _≺ₚ_ denotes the given order w on parameters from the carrier. In _≺ₙ_, codes are compared first, arities second, and parameter vectors third. Only the first and third keys need relation sets in the object language; numeral membership expresses the arity comparison.
open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ ) open SWO w using () renaming ( _<∙_ to _≺ₚ_ )
The sets Rs and Ps represent these two orders inside the model. For limits u,v, Rrep reads membership of the ordered pair in Rs as u ≺ˡ v, and Rfill proves that membership from the comparison. The laws Prep and Pfill give the analogous two directions for carrier elements and Ps. These four representation laws are hypotheses of the adequacy result.
module Least (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 ⟩)
The private module K specializes the three-key comparison adequacy to Rs, Ps, and their representation laws. Its order-in turns a proof of the meta-level name comparison into satisfaction of _≺At_; its order-out recovers the comparison under propositional truncation. The arguments below supply the code, numeral, and environment equations for the particular names being compared.
where private module K = Keys Rs Ps Rrep Rfill Prep Pfill
The module Min fixes the nine positions used by a least-name formula: the two relations R,P, the carrier B, the code sets C,C₀, the current name's code, arity, and environment s,a,e, and its denotation d. The equations qR and qP identify the underlying relation sets, while qB is an equality of model elements because later formulas depend on the carrier. The equation qC identifies the underlying set of the carrier's code set.
module Min {n : ℕ} (R P B C C₀ s a e d : Fin n) (γ : S ^ n) (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps) (qB : lookup B γ ≡ Aʟ) (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ))
The remaining equation q₀ identifies C₀ with the underlying set of codes over the empty alphabet. With qB, qC, and q₀ fixed, the private module N supplies the already proved fill and read principles for NameAt at exactly the slots used here. Least-name adequacy can therefore separate the claim that the current data form a name from the additional minimality claim.
(q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where private module N = Named B C C₀ s a e d γ qB qC q₀
For a name t, IsMin t states that no earlier name denotes the set in slot d. Given any competitor t', an equality identifying that slot with denote t' and a proof t' ≺ₙ t must produce a contradiction. Thus only names of the same displayed set are competitors, and earlier refers to the full lexicographic order on names.
IsMin : Name → Type (ℓ-suc ℓ) IsMin t = (t' : Name) → fst (lookup d γ) ≡ denote t' → t' ≺ₙ t → Empty.⊥
The predicate Least t pairs N.Data t with IsMin t. Its first component is the four-equation record identifying the code, arity numeral, parameter environment, and denotation slots with the data of t. Its second component rules out every smaller name of that same denotation. This matches the two conjuncts of LeastNameAt: naming and the universal minimality condition.
Least : Name → Type (ℓ-suc ℓ) Least t = N.Data t × IsMin t
To fill LeastNameAt, N.NameAt-fill first establishes its naming conjunct from the concrete name t and the record dt. The remaining conjunct is a function implementing the three nested universal quantifiers. For arbitrary sets s', a', and e', it assumes both that they describe a competitor naming the same d and that this competitor precedes the current name, and it must derive contradiction.
LeastAt-fill : (t : Name) → Least t → ⟨ γ ⊨ LeastNameAt R P B C C₀ s a e d ⟩ LeastAt-fill t (dt , mt) = N.NameAt-fill t dt , univ where univ : (s' a' e' : S)
After the three competitor data are added, the environment is e' ∷ a' ∷ s' ∷ γ; hence their slots are zero, one, and two, while every old slot is shifted by sh3. The first premise is satisfaction of NameAt for the competitor with the shared denotation sh3 d. The second is satisfaction of _≺At_ from that competitor to the shifted current triple. The result is Lift Empty.⊥, the universe-level form of contradiction required by the formula semantics.
→ ⟨ (e' ∷ a' ∷ s' ∷ γ) ⊨ NameAt (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero)) (suc zero) zero (sh3 d) ⟩ → ⟨ (e' ∷ a' ∷ s' ∷ γ) ⊨ ≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero (sh3 s) (sh3 a) (sh3 e) ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥
The proof first applies Named.NameAt-read to the competitor's naming satisfaction. This yields, under propositional truncation, a name t' and the four equations in its Named.Data record. Because the required result is contradiction, a proposition, PT.rec may eliminate that propositional truncation. No competitor is selected or retained beyond this proof of impossibility.
univ s' a' e' hn hlt = lift (PT.rec Empty.isProp⊥ step (Named.NameAt-read (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero)) (suc zero) zero (sh3 d) (e' ∷ a' ∷ s' ∷ γ) qB qC q₀ hn)) where step : Σ[ t' ∈ Name ] Named.Data (sh3 B) (sh3 C) (sh3 C₀)
For a recovered competitor, the four data equations are named qs', qa', qe', and qd'. The last equation says that the shared denotation slot is denote t', so mt t' qd' is ready to refute any proof that t' ≺ₙ t. That comparison is itself obtained under propositional truncation, and the second PT.rec may eliminate it because its target is again contradiction.
(suc (suc zero)) (suc zero) zero (sh3 d) (e' ∷ a' ∷ s' ∷ γ) qB qC q₀ t' → Empty.⊥ step (t' , (qs' , (qa' , (qe' , qd')))) = PT.rec Empty.isProp⊥ (mt t' qd')
The call to K.order-out supplies the truncated comparison. It uses the relation equations qR,qP, the recovered competitor's code, numeral, and environment equations, the corresponding three equations from dt for the current name, and the assumed satisfaction hlt. Its result is ∥ t' ≺ₙ t ∥₁; eliminating it into mt t' qd' completes the universal minimality clause.
(K.order-out (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero (sh3 s) (sh3 a) (sh3 e) (e' ∷ a' ∷ s' ∷ γ) t' t qR qP qs' (dt .fst) qa' (dt .snd .fst) qe' (dt .snd .snd .fst) hlt)
Conversely, satisfaction of LeastNameAt splits into naming evidence hn and the universal clause hu. Reading hn gives ∥ Σ[ t ∈ Name ] N.Data t ∥₁. The map shown here keeps that outer propositional truncation and, for each recovered t and dt, adds a proof of IsMin t. Consequently LeastAt-read proves only the propositionally truncated existence of a least name.
LeastAt-read : ⟨ γ ⊨ LeastNameAt R P B C C₀ s a e d ⟩ → ∥ Σ[ t ∈ Name ] Least t ∥₁ LeastAt-read (hn , hu) = PT.map step (N.NameAt-read hn) where step : Σ[ t ∈ Name ] N.Data t → Σ[ t ∈ Name ] Least t
To prove IsMin t, fix an explicit competitor t', an equality qd' showing that it denotes the set in slot d, and a comparison lt : t' ≺ₙ t. The universal clause hu is instantiated with codeEl t', the previously defined numAt (arity t'), and envEl t'. Thus only the code and environment wrappers are new here; the numeral wrapper is reused.
step (t , dt) = t , (dt , mt) where mt : IsMin t mt t' qd' lt = lower (hu (codeEl t') (numAt (arity t')) (envEl t') (Named.NameAt-fill (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero))
The first premise for hu is built by Named.NameAt-fill. The equations codeEl-fst, numAt-fst, and envEl-fst identify the competitor's three data slots, while the assumed qd' identifies the shared denotation slot. The second premise begins with K.order-in, which will translate the explicit comparison lt into satisfaction of the comparison formula.
(suc zero) zero (sh3 d) (envEl t' ∷ numAt (arity t') ∷ codeEl t' ∷ γ) qB qC q₀ t' (codeEl-fst t' , (numAt-fst (arity t') , (envEl-fst t' , qd')))) (K.order-in (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
The call to K.order-in also receives the current name's three equations from dt and the relation equations qR,qP. It therefore proves the exact comparison premise expected by hu in the extended environment. Applying hu yields a lifted contradiction, and lower returns it at the universe level required by IsMin. This lift and lowering concern universe placement; they do not eliminate a propositional truncation.
(sh3 s) (sh3 a) (sh3 e) (envEl t' ∷ numAt (arity t') ∷ codeEl t' ∷ γ) t' t qR qP (codeEl-fst t') (dt .fst) (numAt-fst (arity t')) (dt .snd .fst) (envEl-fst t') (dt .snd .snd .fst) lt))
One step, described and meant
The module Step keeps the same two represented relations, carrier, and code sets, and adds slots x and y for the sets to be compared. The five equations have the same roles as in Min: qR,qP interpret the two relation slots, qB identifies the carrier as a dependent model element, and qC,q₀ identify the two underlying code sets. This local statement concerns a comparison of names for x and y; the later connection to a stage order is proved outside this module.
module Step {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps) (qB : lookup B γ ≡ Aʟ) (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ))
LeastOf i t is the meta-level property needed for either endpoint of a step. Its first component says that slot i contains denote t. Its second component says that any name t' whose denotation is also that slot cannot precede t. Thus it asserts that t is a least name for the particular set in slot i; it does not itself contain a satisfaction proof for any formula.
(q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where LeastOf : Fin n → Name → Type (ℓ-suc ℓ) LeastOf i t = (fst (lookup i γ) ≡ denote t) × ((t' : Name) → fst (lookup i γ) ≡ denote t' → t' ≺ₙ t → Empty.⊥)
StepAt-fill starts with explicit names t₁,t₂, proofs that they are least for x,y, and an explicit comparison t₁ ≺ₙ t₂. It supplies six witnesses to StepAt-in in binder order: the code, arity numeral, and parameter environment of t₁, followed by the corresponding three data of t₂. The body then requires two least-name satisfactions and one comparison satisfaction. No input to this filling theorem is propositionally truncated.
StepAt-fill : (t₁ t₂ : Name) → LeastOf x t₁ → LeastOf y t₂ → t₁ ≺ₙ t₂
→ ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
StepAt-fill t₁ t₂ l₁ l₂ lt = StepAt-in R P B C C₀ x y γ
( codeEl t₁ , (numAt (arity t₁) , (envEl t₁
, ( codeEl t₂ , (numAt (arity t₂) , (envEl t₂
Existential witnesses are pushed onto the front of the environment, so the six witnesses appear there in reverse binder order: envEl t₂, its numeral and code, then envEl t₁, its numeral and code, followed by γ. In this environment s6a,a6a,e6a locate the first name's code, numeral, and environment. The proof ln₁ applies LeastAt-fill with the first name's three data equations, the denotation equation l₁ .fst, and the minimality proof l₁ .snd.
, ( ln₁ , (ln₂ , cmp) ))))))) where ln₁ = Min.LeastAt-fill (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x) (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂
The record passed to the first LeastAt-fill has exactly the expected two parts. Its N.Data component consists of codeEl-fst, numAt-fst, envEl-fst, and the equality l₁ .fst identifying slot x with the denotation of t₁; its IsMin component is l₁ .snd. Thus ln₁ proves that the first bound triple is a least name of x. The analogous construction for t₂ and the comparison proof are the remaining components needed by StepAt-in.
∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ) qR qP qB qC q₀ t₁ ( (codeEl-fst t₁ , (numAt-fst (arity t₁) , (envEl-fst t₁ , l₁ .fst))) , l₁ .snd )
The second least-name condition is filled by the same adequacy map as the first, now at the slots s6b, a6b, and e6b. The shared six-witness environment identifies these slots with the code, arity numeral, and parameter environment of t₂, while sh6 y identifies the set that t₂ must denote. The remaining argument must therefore establish both that denotation and the leastness of t₂.
ln₂ = Min.LeastAt-fill (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
s6b a6b e6b (sh6 y)
(envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂
∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ)
qR qP qB qC q₀ t₂
The nested pair has exactly the type required by LeastAt-fill: the four data equalities for t₂, followed by its leastness proof. The first three equalities come from the sealed code, numeral, and environment elements; l₂ .fst identifies the denotation with the value in slot y; and l₂ .snd rules out every t' with that same denotation and t' ≺ₙ t₂. Thus leastness has the required direction: no smaller competing name precedes t₂.
( (codeEl-fst t₂ , (numAt-fst (arity t₂) , (envEl-fst t₂ , l₂ .fst))) , l₂ .snd )
The comparison condition uses only the three ordering keys of each name. The call to order-in begins with qR and qP, which interpret the two relation slots, and then supplies the two code equalities and the two arity-numeral equalities. Together with the two environment equalities on the following line, these make the eight equalities required by the call. Denotation and leastness are absent because _≺ₙ_ compares names by those three keys alone.
cmp = K.order-in (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂ ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ) t₁ t₂ qR qP (codeEl-fst t₁) (codeEl-fst t₂) (numAt-fst (arity t₁)) (numAt-fst (arity t₂))
The two environment equalities complete the slot identifications, and the final argument lt supplies the actual comparison t₁ ≺ₙ t₂. Hence cmp is a satisfaction proof for the object-language comparison between the two triples. Together with ln₁ and ln₂, it supplies the three conjuncts packed by StepAt-in. This filling direction starts with specified names and a specified comparison, so it introduces the six existential witnesses directly.
(envEl-fst t₁) (envEl-fst t₂) lt
The converse theorem states the exact witness boundary. From satisfaction of StepAt, it returns only ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁. The outer dependent sum ranges t₁ over all names, and for each such t₁ the inner sum ranges t₂ over all names. Their payload says precisely that t₁ is least for the value in slot x, t₂ is least for the value in slot y, and t₁ ≺ₙ t₂. The first PT.rec opens the truncated six-witness payload supplied by StepAt-out, with this still-truncated conclusion as its target.
StepAt-read : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁ StepAt-read h = PT.rec squash₁ atSix (StepAt-out R P B C C₀ x y γ h) where
Goal names that codomain once so that every truncation elimination has the same target. Because Goal is itself a propositional truncation, squash₁ proves that it is a proposition. This is the precise reason that the outer six-witness truncation and the two later least-name truncations may all be eliminated while the final pair of names remains hidden by one truncation.
Goal : Type (ℓ-suc ℓ) Goal = ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁
Inside that permitted elimination, atSix receives an ordinary StepOf witness and separates it into the triples (s₁,k₁,p₁) and (s₂,k₂,p₂). Because existential witnesses are added at the head of an environment, the body is evaluated in the reverse order p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ. The first call to LeastAt-read therefore uses the first triple's fixed positions s6a, a6a, and e6a to read a least name for the value in slot x.
atSix : StepOf R P B C C₀ x y γ → Goal atSix (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , hb)))))) = PT.rec squash₁ atFirst (Min.LeastAt-read (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x)
The body proof hb contains three conjuncts. Its projections name them as h₁, the first triple's LeastNameAt satisfaction, h₂, the corresponding satisfaction for the second triple, and hc, satisfaction of ≺At from the first triple to the second. The proof first gives h₁ to LeastAt-read. The other two conjuncts are retained until both meta-level names have been recovered, since only then can hc be interpreted as a comparison of those names.
(p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ h₁) where h₁ = hb .fst h₂ = hb .snd .fst hc = hb .snd .snd
atSecond records what remains after the first least name has been read. It accepts a particular t₁ with its full Min.Least record, then a particular t₂ with the analogous record, and must produce Goal. Each record contains four data equalities together with the correctly directed leastness assertion. Thus this continuation has enough information both to recover the two LeastOf facts and to interpret the still-object-language comparison hc.
atSecond : (t₁ : Name)
→ Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
s6a a6a e6a (sh6 x)
(p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₁
→ Σ[ t₂ ∈ Name ] Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C)
Once both records are available, only a proof lt : t₁ ≺ₙ t₂ is missing from the final statement. The function mapped over that comparison keeps from each data record precisely its denotation equality, dᵢ .snd .snd .snd, and pairs it with the leastness proof mᵢ; these are exactly the two components of LeastOf. It then joins the resulting least-name facts with lt and inserts the complete pair of names into Goal without removing the surrounding truncation.
(sh6 C₀) s6b a6b e6b (sh6 y) (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₂ → Goal atSecond t₁ (d₁ , m₁) (t₂ , (d₂ , m₂)) = PT.map (λ lt → t₁ , (t₂ , ( (d₁ .snd .snd .snd , m₁)
order-out now interprets hc. Besides qR and qP, it receives from d₁ and d₂ the code, arity-numeral, and parameter-environment equalities for the two recovered names. The denotation equalities are unnecessary for this three-key comparison. The result is only ∥ t₁ ≺ₙ t₂ ∥₁; PT.map transforms each comparison inside that propositional truncation into the complete witness required by Goal.
, ( (d₂ .snd .snd .snd , m₂) , lt )))) (K.order-out (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) t₁ t₂ qR qP (d₁ .fst) (d₂ .fst) (d₁ .snd .fst) (d₂ .snd .fst) (d₁ .snd .snd .fst) (d₂ .snd .snd .fst) hc)
atFirst is the continuation for the first least-name reading. Given its recovered pair (t₁,l₁), it applies LeastAt-read to h₂ at the second triple's slots, obtaining the second pair only under propositional truncation. The following PT.rec may pass that pair to atSecond t₁ l₁ because the target is the proposition Goal. The second truncation is therefore eliminated only while constructing the final truncated existence statement.
atFirst : Σ[ t₁ ∈ Name ] Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C)
(sh6 C₀) s6a a6a e6a (sh6 x)
(p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₁
→ Goal
atFirst (t₁ , l₁) = PT.rec squash₁ (atSecond t₁ l₁)
The final invocation supplies the second triple's fixed slots, the same reversed six-witness environment, and h₂. It completes a chain of four truncated interfaces: StepAt-out, the two calls to LeastAt-read, and order-out. Their composition proves exactly that satisfaction of StepAt entails the propositionally truncated existence of names t₁,t₂ such that t₁ is least for x, t₂ is least for y, and t₁ ≺ₙ t₂. No particular pair of names is exported outside that truncation.
(Min.LeastAt-read (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y) (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ h₂)
Recap
This chapter establishes both directions of the semantic correspondence for names. In the adequacy direction, a concrete name fills NameAt from its formula code, arity, parameter environment, and denotation; a proof that it is least among the names with that denotation fills LeastNameAt; and two such least names with t₁ ≺ₙ t₂ fill StepAt. In the completeness direction, satisfaction recovers the same data in reverse. Consequently, the formula comparing the two least descriptions agrees with the meta-language comparison: formula codes are compared first, then arities when the codes agree, and finally parameter vectors when both earlier keys agree.
The completeness statements retain propositional truncation. Uniqueness lets the parameter graph determine its vector without truncation, but reading a whole name, a least name, or a pair of compared least names proves only that suitable witnesses exist. Every truncation is eliminated only into a proposition, and no particular name or pair of names is exported. No propositional resizing occurs here. This is exactly the boundary used when StepAt is connected to the host-level step order.