---
title: "Adequacy of name comparison"
module: L.Choice.NameComparisonAdequacy
lang: en
site: "Bedrock"
description: "Adequacy of name comparison"
stage: "The canonical well-order and Choice"
reading_order: 80
canonical: https://bedrock.institute/en/L.Choice.NameComparisonAdequacy.html
html: L.Choice.NameComparisonAdequacy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/NameComparisonAdequacy.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.EnvironmentSet, L.Coding.SatisfactionGraph, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Choice.CanonicalNames, L.Choice.FiniteStageOrders, L.Choice.NameComparison, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/zh/L.Choice.NameComparisonAdequacy.md, https://bedrock.institute/ja/L.Choice.NameComparisonAdequacy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Adequacy of name comparison

Many 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
  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.

```agda
        ; 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
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.

```agda
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.

```agda
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.

```agda
    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`.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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`.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
    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.

```agda
    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.

```agda
    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`.

```agda
    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`.

```agda
    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`.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
           → ⟨ 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₀`.

```agda
  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.

```agda
      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.

```agda
      ψ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ʟ`.

```agda
      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.

```agda
      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.

```agda
        (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.

```agda
    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.

```agda
    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.

```agda
        δ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.

```agda
        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.

```agda
        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.

```agda
                 (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.

```agda
      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.

```agda
        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`.

```agda
        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.

```agda
                 (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.

```agda
        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`.

```agda
        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.

```agda
                   (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.

```agda
        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.

```agda
          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.

```agda
      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`.

```agda
        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))`.

```agda
        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.

```agda
        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.

```agda
        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.

```agda
        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.

```agda
        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`.

```agda
        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`.

```agda
      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.

```agda
        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`.

```agda
      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.

```agda
        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`.

```agda
    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`.

```agda
      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.

```agda
      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`.

```agda
      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`.

```agda
      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`.

```agda
      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.

```agda
    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.

```agda
             → Σ[ χ ∈ 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.

```agda
        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`.

```agda
        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.

```agda
        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.

```agda
        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.

```agda
          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.

```agda
        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.

```agda
          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`.

```agda
        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`.

```agda
      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.

```agda
  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.

```agda
    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`.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
  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.

```agda
               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.

```agda
    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.

```agda
               (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.

```agda
      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.

```agda
      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.

```agda
      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.

```agda
             → ⟨ (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.

```agda
        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.

```agda
                   (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.

```agda
              (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.

```agda
      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.

```agda
        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.

```agda
               (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.

```agda
               (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.

```agda
    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.

```agda
                (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.

```agda
      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`.

```agda
        , ( 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`.

```agda
                 ∷ 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₂`.

```agda
        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₂`.

```agda
                ( (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.

```agda
        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.

```agda
                (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.

```agda
      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.

```agda
        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`.

```agda
        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.

```agda
               (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`.

```agda
          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.

```agda
                       (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`.

```agda
                                      , ( (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.

```agda
          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.

```agda
            (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.