---
title: "Formulas for name comparison"
module: L.Choice.NameComparison
lang: en
site: "Bedrock"
description: "Formulas for name comparison"
stage: "The canonical well-order and Choice"
reading_order: 77
canonical: https://bedrock.institute/en/L.Choice.NameComparison.html
html: L.Choice.NameComparison.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/NameComparison.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.Axioms.Infinity, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.Satisfaction, L.Coding.SatisfactionTable, L.Coding.SlotClosure, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.SatisfactionGraph, L.Coding.EnvironmentTower, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.PinnedRecursion, L.Choice.CanonicalNames, L.Choice.FiniteStageOrders, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/zh/L.Choice.NameComparison.md, https://bedrock.institute/ja/L.Choice.NameComparison.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Formulas for name comparison

A definable subset can have many names. At the meta-level, a name consists of an arity `k`, a parameter-free formula with `suc k` variable slots, and a vector of `k` parameters from the carrier. Its denotation is then derived from these three pieces: the extra variable ranges over the candidate member, and the remaining variables receive the parameter vector. The denotation is therefore not a fourth component of the name.

To express this data inside `L`, the chapter represents the parameter vector by a finite environment graph and represents evaluation by the satisfaction graph. At a genuine formula key, `satGraphAt` relates that key to the set of environments satisfying the formula. Its output is exactly this satisfaction-environment set. `NameAt` combines the arity, parameter-free formula code, and parameter environment with the derived denotation that will later be shared by all competing names.

Names are compared lexicographically: first by the formula code under the limit-stage order, then by arity, and finally by the parameter vectors under the given order on the carrier. The formula `≺At` expresses these three cases. `LeastNameAt` only states that the displayed name has no smaller name with the same denotation; the actual choice of a least name is the earlier construction `CanonicalNames.leastName`. `StepAt` locally quantifies two least names and compares them. The adequacy proved in this chapter reaches exactly `≺At` versus the meta-level relation `_≺ₙ_`; the full adequacy of `NameAt`, `LeastNameAt`, and `StepAt` is established in the following development.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

The underlying language supplies universe levels, finite indices, vectors, and proposition-valued statements. Classical reasoning enters through one explicit hypothesis, `LEM (ℓ-suc ℓ)`, whose level is large enough for the satisfaction constructions and well-orders used below. Keeping that hypothesis visible will let us distinguish descriptions that merely state a property from earlier constructions that actually choose a witness.

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

Fix a universe level `ℓ` and a law of excluded middle at the required higher level. This is the classical interface carried by the chapter. The formula constructors below only assemble syntax, but the natural-number object, satisfaction graph, limit-stage code order, and canonical-name theory that they use were constructed under the same hypothesis. The module therefore records these semantic dependencies without performing another choice. `LeastNameAt` expresses minimality; `CanonicalNames.leastName` remains the construction that selects a least name.

```agda
module L.Choice.NameComparison {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The object language can speak about membership and equality, combine propositions, and quantify both over the whole carrier and over a set. Its semantics is read in a proposition-valued structure. Constant mappings connect three presentations needed later: genuinely parameter-free formulas, formulas over the empty alphabet, and the same syntax interpreted over a constructible carrier. Because these mappings preserve the formula, they will allow the code of a parameter-free skeleton to be recognized internally.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed )
```

Formula codes, ordered pairs, and numerals are themselves sets in the cumulative hierarchy. The constructible substructure supplies the carrier in which the formulas are read, while transitivity lets membership in a constructible code set provide the constructibility facts needed for its components. Injectivity of pair and numeral coding later recovers arities and skeleton codes from equal keys. The stages `Lset` provide the setting for the limit-stage code order.

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset )
open import L.Ordinal {ℓ} using ( ∈#-elim; #∈#-elim )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ; extensionalL )
```

An arity is represented by a numeral in the internal natural-number set, and a parameter vector is represented by the graph of a finite environment. The object-language formulas can inspect ordered pairs, applications, and domains, extend an environment by a candidate element, and define a subset extensionally. For a formula over a carrier, `Sat` is the set of environments satisfying that formula. This set-valued reading is the semantic value later recovered from the satisfaction graph.

```agda
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro; envOverAt )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in-both; numL; sucAtL; sucAtL-adequate; consAtL )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
```

Satisfaction has already been organized into a table whose entries pair each subformula key with its recursively determined set of satisfying environments. Slot closure and totality ensure that every genuine key needed in the recursion receives an entry, and the satisfaction bridge identifies its constants with elements of the chosen carrier. The present chapter can therefore read a stored value at a key without running the satisfaction recursion again.

```agda
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.CodeSet {ℓ} lem
```

For each carrier, `AllCodes` collects exactly the genuine formula keys over that carrier, and its two directions connect membership with an underlying formula. The uniform bridge then supports the relational formula `satGraphAt B x y`: when `x` is a genuine key over the carrier in slot `B`, `y` is the corresponding set of satisfying environments. `GraphWitAt` and the two graph readings expose this set-valued relation without starting a fresh recursion.

```agda
  using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge )
open import L.Coding.SatisfactionGraph {ℓ} lem using
  ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
  ; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )
```

The environment tower and the tagged recursion data justify the satisfaction-graph reading at every syntactic constructor. Against this internal machinery, the canonical-name theory supplies the meta-level standard used for comparison. A meta-level `Name` stores an arity, a parameter-free formula, and a parameter vector; `limitCode` derives the first comparison key from the formula, while the denotation is separately derived by satisfaction. This distinction is what the later slot formula must preserve.

```agda
open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )
```

The code of a name is a member of the limit stage and is compared by `limitOrder`. The third key comes from an arbitrary strict well-order on the carrier. Canonical naming has already combined these with natural-number arity into `_≺ₙ_`, proved that relation well-founded, and used it in `leastName`. Here the two non-numerical orders appear through relation slots with representation laws, so the chapter describes their comparison rather than reconstructing either order.

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
```

Natural-number order supplies the second comparison key: for numeral arities, membership of one numeral in another expresses strict inequality. Finite indices locate entries of parameter vectors and the earliest position at which two vectors differ. The adequacy argument later proves, by induction on their common length, that this first-difference description agrees with the recursive vector order used in `_≺ₙ_`.

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
```

The proof data follow the lexicographic shape. Dependent pairs carry a position together with its evidence, while coproducts separate the code, arity, and parameter cases. Equalities of earlier keys permit dependent formulas and vectors to be transported to a common arity before the next key is compared. The empty type supplies the unique interpretation of constants for a formula that has no constants.

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2 )
```

Existential and disjunctive satisfaction is propositionally truncated: it preserves that a witness exists while forgetting which witness was supplied. Consequently, outward readings such as those for formula codes and name comparison return truncated existence, and elimination is used only into propositions. This is propositional truncation; propositional resizing does not occur here. The cumulative hierarchy supplies set-valued membership and the extensional equality principles needed after such readings.

```agda
open import Cubical.Foundations.Transport using ( constSubstCommSlice )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

Small members of a hierarchy set embed into the ambient hierarchy, and injectivity of that embedding later turns equality of represented parameters back into equality in the carrier. The empty set serves as the empty alphabet: it has no constants, so every map out of it is uniquely determined and a parameter-free formula keeps the same code under the required relabellings. The von Neumann numerals `# k`, their successor, and `ω` provide the internal arities used by environment domains and name comparison.

```agda
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω; sucV )
```

The formulas ahead are interpreted in the constructible universe. Opening
`hPropStructure 𝒮ʟ` fixes their carrier `S`: an element is an ambient set
together with evidence that it is constructible. It also brings the
proposition-valued equality and membership relations of this structure into
scope. Thus a free variable or constant ranges over constructible sets, while
`⟨_⟩` exposes the type of evidence carried by an equality or membership
proposition when a proof uses it.

```agda
open hPropStructure 𝒮ʟ
```

There are two compatible readings of the same syntax. The absoluteness
instance starts with the ambient universe structure `𝒮ᵥ` and restricts it to
the transitive class `isL`. In the outer reading, a constructible set is
viewed through its underlying ambient set; in the inner reading, a constant
denotes the constructible set that names it and the restricted structure
supplies equality and membership. This chapter renames the inner satisfaction
relation to `⊨`. Consequently, for `γ : S ^ n`, the judgement `γ ⊨ F` says
that `F` holds inside `L` under the finite environment `γ`. This is the
reading needed for formulas that `L` itself will use to recognize and compare
names.

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

The formulas refer to earlier data by positions in an environment. Under a
new binder, every such position must move past the newly bound value; after
two binders, position `i` therefore becomes `suc (suc i)`. The abbreviation
`sh2` records this move. It is used when `FreeAt` has bound the successor
arity and its code key before consulting the skeleton and empty-alphabet code
set, and when the denotation condition has bound a candidate element and its
extended environment before consulting the original parameter environment.

```agda
private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)
```

Inside the denotation condition, the skeleton and the carrier's code set are
consulted only after four values have entered the environment: the candidate
element `z`, the extended environment `c`, its domain `k`, and the key under
consideration. Their original positions must therefore be raised four times.
`sh4` performs exactly that shift, so the key can be required both to belong
to the carrier's code set and to equal the pair formed from `k` and the
skeleton.

```agda
  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))
```

One more existential binds the value `v` associated with the key, so the
carrier is five places away when `satGraphAt` is invoked. Here `v` is the set
of environments satisfying the encoded formula, rather than a truth value;
the following membership atom asks whether the extended environment belongs
to that set. The same shift reappears in `LexAt`: after binding an index, the
two values at that index, an earlier index, and their proposed common value,
the original parameter environments are again five places away. `sh5`
records the common index calculation for both formulas.

```agda
  sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n)))))
  sh5 i = suc (suc (suc (suc (suc i))))
```

## The same code at the empty alphabet

The empty alphabet is the small presentation `⟪ ∅ ⟫` of members of the empty
set. If `m` were one of its symbols, the embedding `⟪ ∅ ⟫↪` would produce an
ambient set, while the presentation law would say that this set belongs to
`∅`. The theorem `∅-empty` rules out precisely such evidence, giving
`noAlpha m`. Thus formulas over this alphabet cannot contain a constant node.
They form one syntactic presentation of parameter-free formulas. Comparing it
with the empty constant domain `⊥*` used by meta-level names amounts to
relating two empty types.

```agda
private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)
```

`Fo∅ n` names the family `Formula ⟪ ∅ ⟫ n`: formulas over the empty alphabet
with `n` available variable positions. Their lack of constants follows from
the type of their constant symbols, rather than from an extra predicate on a
formula. Meta-level names use the parallel family `Formula ⊥* n`. More
precisely, a `Name` stores an arity, a formula from that family with one extra
variable position, and a parameter vector of the stated arity; its denotation
is derived from those three pieces and is not another stored component.

```agda
  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫
```

The map `ε` changes from the empty alphabet `⟪ ∅ ⟫` to the empty constant
domain `⊥*`. Given a supposed source symbol `m`, `noAlpha m` yields a
contradiction, and empty elimination supplies the requested target. Hence
`mapFo ε` relabels a formula over `⟪ ∅ ⟫` as a formula over `⊥*`; in the other
direction, `embed` may be specialized to relabel from `⊥*` into `⟪ ∅ ⟫`.
Neither operation changes a constant occurrence, since there is none. The
composition law for relabelling then yields the precise equalities of formula
codes needed for the empty-alphabet characterization.

```agda
  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = Empty.rec (noAlpha m)
```

To recognize parameter-free formula codes inside the model, we must first relate
two presentations of having no constants. A formula `ψ` over `⟪ ∅ ⟫` uses as its
constant domain the members of the empty set, while `mapFo ε ψ` presents the same
syntax over the empty type `⊥*`. The map `ε` exists because an alleged member of
the empty set yields a contradiction. Reading `ψ` directly into the universe and
first relabelling it by `ε` and then embedding it therefore differ only by maps
out of an empty type. Function extensionality identifies those maps, and
`mapFo-comp` identifies the composite relabelling. Thus `sameCode` proves an
equality of the resulting universe-formulas themselves; applying the coding map
to this equality will later give equality of their codes.

```agda
  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m)))
             ∙ sym (mapFo-comp ε Empty.rec* ψ)
```

The converse comparison begins with a parameter-free formula
`χ : Formula ⊥* n`. It may be embedded first into formulas over `⟪ ∅ ⟫` and
then relabelled by the inclusion of that alphabet into the universe, or embedded
directly into formulas over the universe. By `mapFo-comp`, the first route is a
single relabelling from `⊥*`; since every two functions from `⊥*` agree, that
relabelling is the one used by the direct embedding. The equality `sameCode'`
is exactly the orientation needed to pass from the key that `AllCodes ∅ʟ`
assigns to the embedded formula to the usual universe-code of `χ`.

```agda
  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))
```

There is one further dependent-type issue. The arity is part of the type of a
formula, so an equality `e : i ≡ j` moves `ψ : Fo∅ i` to
`subst Fo∅ e ψ : Fo∅ j`. The key, however, should retain the same formula code
after this move. The codomain of the function that reads and codes a formula is
the fixed universe `V ℓ`, independent of the arity index. The general
substitution computation `constSubstCommSlice` therefore says that transporting
the formula does not change its code. `codeShift` records the equality in the
direction from the transported formula's code back to the original one, ready
for the arity adjustment in the decoding argument.

```agda
  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift e ψ = sym (constSubstCommSlice
    Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)
```

We can now prove the easy direction of the code-set bridge. For a
parameter-free `k`-ary formula `χ`, embedding it over `⟪ ∅ ⟫` produces a
formula whose key belongs to `AllCodes ∅ʟ` by `key∈AllCodes`. That key consists
of the numeral `# k` and the code obtained by reading the embedded formula
through the empty alphabet. The equality `sameCode'` identifies this formula
with the direct universe embedding of `χ`; the latter code is precisely
`fst (limitCode χ)`. Transporting membership along that equality proves
`freeCode-in`: the code set contains the arity-and-code key of every
parameter-free formula.

```agda
freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))
```

For the reverse direction, suppose `pr (# k) c` belongs to `AllCodes ∅ʟ`.
The elimination theorem `AllCodes-out` decodes a member only under
propositional truncation, and it takes an element of `S`, namely a set together
with a proof that it is constructible. The underlying set of the desired input
is already `pr (# k) c`; it remains to supply that constructibility proof. Once
this is done, `PT.map read` transforms each possible decoded payload into the
desired `k`-ary parameter-free payload without ever removing the truncation.

```agda
freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩
             → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁
freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩
```

That missing certificate follows from transitivity of constructibility.
`AllCodes ∅ʟ .snd` says that the code set is constructible, while `h` says that
the key belongs to it. Hence `isL-trans h (AllCodes ∅ʟ .snd)` proves that the
key itself is constructible. Pairing this certificate with `pr (# k) c` gives
the element of `S` required by `AllCodes-out`; no additional decoding or choice
occurs here.

```agda
  cL = isL-trans h (AllCodes ∅ʟ .snd)
```

Inside the truncation, `AllCodes-out` supplies an arity `n`, a formula
`ψ : Fo∅ n`, and an equality saying that the given key is the key of `ψ`.
The local function `read` turns each such payload into a parameter-free formula
of the requested arity `k` together with an equality between `c` and its code.
It does so by first transporting `ψ` to a formula `ψ' : Fo∅ k` and then
relabelling its impossible constants along `ε`. Thus the proposed witness is
`mapFo ε ψ'`. The pair equality provides both the arity equality needed for the
transport and the code equality used in the returned dependent pair.

```agda
  read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ))
       → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ))
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k
```

The two components of the key equality finish the construction. Its first
component has type `# k ≡ # n`; injectivity of numerals and symmetry yield
`e : n ≡ k`, along which `ψ` is transported to `ψ'`. Its second component says
that `c` is the universe-code obtained from the original `ψ`. By `codeShift`,
that code agrees with the code of the transported `ψ'`; by `sameCode`, the
latter agrees with the code of `embed (mapFo ε ψ')`. Composing these equalities
gives exactly the certificate paired with the witness. Since `read` is applied
only through `PT.map`, `freeCode-out` concludes merely that such a
parameter-free formula exists under propositional truncation. It does not
select a formula from the code set.

```agda
    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')
```

## Constant-freeness, said as one atom

The code set stores a formula under a key made from its arity and its skeleton.
To express this with one membership atom, `FreeAt` first binds the successor of
the value in the arity slot, then binds its pair with the skeleton, and finally
asks whether that pair belongs to the code-set slot. Thus, in meta-level
notation, its shape is `∃[ z ] ∃[ y ]`: `z` is the successor arity, while `y`
is the key. The shifts record exactly which earlier slot remains visible beneath
one or two binders. At this stage the formula only describes membership in the
set supplied at `C₀`; its parameter-free meaning will follow when that slot is
identified with the code set for the empty alphabet.

```agda
FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )
```

The first pair of readings works over an arbitrary environment `γ`. The
external equality `qa` identifies the value at the arity slot with the numeral
`# k`; it is a hypothesis of the semantic reading, not another clause inside
`FreeAt`. The skeleton and code-set slots remain arbitrary, so these lemmas
isolate the logical content of the two binders before the particular code set
is chosen.

```agda
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) where
```

For the forward construction, suppose the intended key
`pr (# (suc k)) (fst (lookup s γ))` already belongs to the set at `C₀`.
This key supplies the two existential witnesses required by `FreeAt`: first the
numeral `# (suc k)`, then its pair with the skeleton. What remains is to verify
the successor and pairing descriptions of these witnesses; the final atom is
exactly the assumed membership.

```agda
  FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
    where
    numAt : S
```

An existential witness for the internal language is an element of `S`, so its
underlying set must come with a proof of constructibility. The first witness
`numAt` has this proof because every numeral belongs to `L`. For the second
witness `keyAt`, the membership hypothesis places the key inside the
constructible set held at `C₀`; transitivity of `L` then makes the key itself
constructible. These proofs justify using the numeral and the key as bound
values, rather than adding any mathematical condition to `FreeAt`.

```agda
    numAt = # (suc k) , numL (suc k)
    keyAt : S
    keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd)
    hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
    hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
```

The adequacy equations for the two auxiliary formulas now perform the promised
checks. For `hsuc`, the equality `qa` changes the value at the arity slot into
`# k`, and the successor of that numeral is `# (suc k)`. For `hpr`, adequacy of
`prAtL` reduces satisfaction to equality with the ordered pair specified by its
two component slots; `keyAt` was defined to be precisely that pair. Hence the
two semantic facts connect the chosen witnesses to the one membership atom.

```agda
      (cong sucV (sym qa))
    hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
    hpr = subst ⟨_⟩
      (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl
```

The reverse reading extracts membership from a satisfaction of `FreeAt`.
Satisfaction of an existential formula provides its witness only under
propositional truncation, so the proof eliminates the outer truncation into the
desired membership proposition. A representative of the outer existential
contains the successor witness and a satisfaction of the inner existential;
the latter still has its own propositional truncation and will be eliminated in
turn.

```agda
  FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
  FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                            ∈ fst (lookup C₀ γ))) atNum
    where
```

Both truncation eliminations have the same codomain, so the proof names it
`Target`: the intended key belongs to the set at `C₀`. This type is a
proposition because membership in a set is proposition-valued. That fact is
the precise license required by each truncation eliminator; no choice of a
distinguished existential witness is being made.

```agda
    Target : Type (ℓ-suc ℓ)
    Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
```

The branch `atKey` handles one representative of the inner existential. It is
given the outer witness `z` together with the equation saying that `z` is the
successor of the arity value, and it receives an inner witness `y` with two
facts: `y` satisfies the pairing formula and its underlying set belongs to the
set at `C₀`. The inner existential was truncated, but inside this elimination
branch its representative may be used to prove the proposition `Target`.

```agda
    atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ))
          → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                       × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ )
          → Target
    atKey z qz (y , (hp , hy)) =
```

Adequacy of `prAtL` identifies the underlying set of `y` with the pair whose
first component is the underlying set of `z` and whose second component is the
skeleton. The equation for `z`, followed by `qa`, identifies that first
component with `# (suc k)`. Consequently `y` is the intended key. Transporting
the given membership of `y` along this equality proves membership of
`pr (# (suc k)) (fst (lookup s γ))`, which is `Target`.

```agda
      subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
         ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy
```

The outer elimination branch `atNum` receives a representative `z` together
with two pieces of evidence. The first says that `z` satisfies the successor
formula. The second, `hk`, is the still-truncated satisfaction of the inner
existential. Thus `atNum` has enough information to determine the intended
first component of the key, while postponing the inner witness until it can be
eliminated into `Target`.

```agda
    atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                       × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                       ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
          → Target
    atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
```

Adequacy of `sucAtL` decodes the first fact into the equality required by
`atKey`: `z` is the successor of the value at the arity slot. The proof then
eliminates `hk` into the proposition `Target` and applies `atKey` to each
representative. Together with the outer elimination already built into
`FreeAt-out`, this accounts for both existential layers while preserving the
propositional-truncation boundary.

```agda
                                         ∈ fst (lookup C₀ γ)))
      (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk
```

The next readings specialize the two previously arbitrary slots. The equality
`q₀` identifies the set at `C₀` with `AllCodes ∅ʟ`, whose elements are keys for
formulas over the empty alphabet, while `qa` again identifies the arity value
with `# k`. Under these hypotheses, the membership characterized by
`FreeAt-in` and `FreeAt-out` can be converted into an actual statement about
parameter-free formulas of arity `suc k`.

```agda
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ))
         (qa : fst (lookup a γ) ≡ # k) where
```

Starting from a satisfaction of `FreeAt`, `FreeAt-out` yields membership of the
key in the set currently held at `C₀`. Transport along `q₀` moves this
membership into `AllCodes ∅ʟ`. The earlier decoding lemma `freeCode-out` then
returns, under propositional truncation, a parameter-free formula `χ` of arity
`suc k` whose limit-stage code is the value in the skeleton slot. This is the
outward semantic reading of the one membership atom.

```agda
  codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
               → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                     (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁
  codeFree-out h = freeCode-out (suc k) (fst (lookup s γ))
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀
```

The arity is `suc k` because a name for a definable subset uses one variable
for the candidate element in addition to its `k` parameter positions. The
formula witness in `codeFree-out` remains propositionally truncated. Although
`FreeAt-out` may eliminate its bound witnesses locally because membership is a
proposition, `freeCode-out` introduces a truncated formula witness at the final
decoding step. The result therefore asserts that such a formula exists without
selecting one.

```agda
      (FreeAt-out C₀ s a γ k qa h))
```

Conversely, `codeFree-in` begins with a specific parameter-free formula `χ` of
arity `suc k` and an equality identifying its limit-stage code with the
skeleton slot. The lemma `freeCode-in` places the corresponding key in
`AllCodes ∅ʟ`; transport along the code equality and then along the reverse of
`q₀` moves that membership to the actual skeleton and code-set slots.
`FreeAt-in` packages the resulting membership with the two existential
witnesses. This direction needs no truncated formula witness because `χ` is
part of the input.

```agda
  codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
              → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  codeFree-in χ q = FreeAt-in C₀ s a γ k qa
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀)
      (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)
```

Together, `codeFree-out` and `codeFree-in` give the promised reading of
`FreeAt` once the arity and empty-alphabet code-set slots are identified. The
outward direction says, under propositional truncation, that the skeleton is
the code of a parameter-free formula with `suc k` variables. The inward
direction starts with a specified formula and needs no such truncation. This
finishes the recognition of a name's formula; the next question is how its
finite parameter environment records the number `k`.

```agda
        (freeCode-in (suc k) χ)))
```

## How long a sequence is

We first characterize arbitrary membership in the set-coded graph. If
`pr x y` belongs to `env g`, where `g` is indexed by `Fin k`, then merely there
is an index `i` for which `x ≡ # (toℕ i)` and `y ≡ g i`. The result remains
under propositional truncation because membership in a hierarchy set records
only the mere existence of a generating entry. Thus `memberOf` exposes every
possible index without choosing one.

```agda
private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = PT.map
    (λ { (li , e) → lower li
```

The membership witness contains an equality between a stored graph entry and
the queried pair. Injectivity of the ordered-pair constructor splits that one
equality into equalities of the two components. The stored entry is written
first in the witness, so both component paths are reversed to obtain the
orientation required by `memberOf`: from `x` and `y` to the numeral key and
the value supplied by `g`.

```agda
       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })
```

Conversely, every prescribed index supplies an entry. For `i : Fin k`, the
pair `pr (# (toℕ i)) (g i)` belongs to `env g`; the lifted index is the
membership witness and the entry equation is reflexivity. Hence `memberOf`
and `entryOf` give the two directions needed to recognize the horizontal
coordinates of this finite graph.

```agda
  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁
```

The forward domain inclusion begins with the mere existence of a model element
`y` such that `pr x (fst y)` lies in the graph. Its goal is the membership
proposition `x ∈ # k`, so the outer propositional truncation may be eliminated
into that goal. After fixing one representative `y`, it remains to recover an
index from the graph membership and prove that its numeral belongs to `# k`.

```agda
  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))
```

For an explicit index `i`, only the first component equality matters to the
domain. Since `toℕ i < k`, the numeral lemma `#mono` places
`# (toℕ i)` in `# k`; transport along `x ≡ # (toℕ i)` then places `x` there.
The second component equality identifies the graph value but is irrelevant to
this inclusion. The helper `atEntry` fixes the value `y` before eliminating
the remaining truncated index information.

```agda
            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))
```

Applying `memberOf` supplies precisely that index information, still under
propositional truncation. Because `x ∈ # k` is a proposition, `PT.rec` may feed
each representative to `atIndex`. This closes the forward inclusion without
extracting an index as ordinary data.

```agda
      (memberOf k g x (fst y) p)
```

For the reverse inclusion, suppose `x ∈ # k`. Elimination for von Neumann
numerals says, under propositional truncation, that `x ≡ # m` for some natural
number `m < k`. Such an `m` determines an index in `Fin k`. The conclusion is
itself a propositionally truncated existence of a graph value, so `PT.map` can
transform each numeral witness without choosing one. The hypothesis `cg` will
supply the constructibility certificate needed to present that value as an
element of the model.

```agda
  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩
  dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))
```

For a representative `m < k`, let `i` be the corresponding finite index. The
witness for the existential is the model element `(g i , cg i)`, namely the
value at that index together with its constructibility proof. The graph fact
comes from `entryOf`: the pair with canonical first component
`# (toℕ i)` is an entry. Transporting that first component to `x` gives the
required membership of `pr x (g i)` in the graph.

```agda
              → Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k
```

The conversion `fromℕ' k m p` turns the bound `p : m < k` into the index `i`.
Its round-trip law `toFromId'` proves `toℕ i ≡ m`. Composing `x ≡ # m` with
the numeral image of the symmetric round-trip equality gives
`qi : x ≡ # (toℕ i)`, exactly the path used to move the canonical entry to the
queried first component. This completes the reverse domain inclusion.

```agda
      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))
```

We can now compare these two set-level inclusions with the object-language
domain formula. Fix an environment `γ`, a family `g : Fin k → V ℓ`, and an
equation `qe` identifying the underlying set in slot `e` with `env g`; slot
`d` remains the proposed domain. Each `cg i` certifies that `g i` is an element
of the constructible model, exactly what the reverse inclusion needs when it
builds an existential witness. In this context the next two lemmas read and
fill `domAt e d`.

```agda
module _ {n : ℕ} (e d : Fin n) (γ : S ^ n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : fst (lookup e γ) ≡ env g) where
```

Suppose `γ` satisfies `domAt e d`. To prove that the underlying set in slot
`d` is `# k`, `domAt-numeral` applies extensionality inside `L` to the two
model elements `lookup d γ` and `(# k , numL k)`, then projects their equality
to the underlying sets. It therefore suffices to prove, for every constructible
test element `x`, that membership in the proposed domain and membership in the
numeral are the same proposition. The forward implication begins by reading
domain membership through `domAt-in`.

```agda
  domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k
  domAt-numeral h = cong fst (extensionalL {a = lookup d γ} {b = # k , numL k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ fst x ∈ # k ⟩
    fwd x hx = dom-into k g (fst x)
```

In the forward implication, `domAt-in` turns membership in slot `d` into the
mere existence of a value paired with `x` in the set at slot `e`. Transport
along `qe` places that entry in `env g`, and `dom-into` yields `x ∈ # k`.
Conversely, `dom-from` turns `x ∈ # k` into the mere existence of an entry in
`env g`. Since membership in the proposed domain is a proposition, that
truncation may be eliminated; the local function `put` handles each displayed
entry.

```agda
      (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe
        (domAt-in e d γ h x hx))
    bwd : (x : S) → ⟨ fst x ∈ # k ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup d γ))) put (dom-from k g cg (fst x) hx)
      where
```

For one displayed entry, `put` transports its membership back along `qe` to
the graph stored at slot `e`; `domAt-out` then gives membership in slot `d`.
Thus the two implications form, by `⇔toPath`, a path between the two
membership propositions at every `x`. Extensionality assembles those pointwise
paths into the equality of the proposed domain with `# k`. The truncated graph
witness is used only to prove membership, so no value is selected from it.

```agda
      put : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ env g ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
      put (y , p) = domAt-out e d γ h x y
        (subst (λ u → ⟨ pr (fst x) (fst y) ∈ u ⟩) (sym qe) p)
    pt : (x : S) → (fst x ∈ fst (lookup d γ)) ≡ (fst x ∈ # k)
    pt x = ⇔toPath (fwd x) (bwd x)
```

The converse starts from an equality saying that the set in slot `d` really is
`# k`. To establish `domAt e d`, `domAt-intro` asks pointwise for the two
implications that define a domain: mere existence of a value in the graph
implies membership in `d`, and membership in `d` implies the mere existence of
a value. The equations `qe` and `qd` reduce these to `dom-into` and `dom-from`,
respectively. Thus filling the formula uses the same two set-level inclusions
as reading it, in the opposite direction.

```agda
  domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩
  domAt-fill qd = domAt-intro e d γ step
    where
    step : (x : S)
         → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩
```

To fill the domain formula, it remains to prove its two pointwise implications.
For the first, suppose some value is paired with `fst x` in the graph stored at
slot `e`. Transport along `qe` puts this entry in `env g`, where `dom-into`
shows that `fst x` belongs to the numeral `# k`. Transporting back along `qd`
then places it in the proposed domain at slot `d`.

```agda
            → ⟨ fst x ∈ fst (lookup d γ) ⟩)
         × (⟨ fst x ∈ fst (lookup d γ) ⟩
            → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩)
    step x =
        (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)
```

The reverse implication follows the same path in reverse. Membership in slot
`d` is transported by `qd` to membership in `# k`; `dom-from` then supplies,
under propositional truncation, a value paired with `fst x` in `env g`; and
transport along the inverse of `qe` returns that entry to slot `e`. These two
directions complete `domAt-fill` without choosing a value from the finite graph.

```agda
          (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe hy)))
      , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) (sym qe)
          (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))
```

## What the satisfaction graph assigns

We now ask what the satisfaction graph assigns at a genuine formula key. Fix
an ambient environment `γ`: slot `B` supplies the carrier, while `x` and `y`
supply the proposed key and value. The abbreviation `Bs = lookup B γ` keeps
the proof uniform in all three slots. Formulas considered below therefore have
constants indexed by the members of the underlying set `fst Bs`.

```agda
module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where
  private
    Bs : S
    Bs = lookup B γ
```

The graph formula packages a satisfaction recursion through fourteen bound
slots. For a model-language formula `φ`, `fr φ` supplies those slots with the
carrier `Bs`, its canonical satisfaction table, the subformula-key slot, the
environment tower, and the ten constructor-tag numerals, followed by the
ambient environment `γ`. Each component is the canonical one already
constructed for this carrier and formula.

```agda
    fr : ∀ {m} (φ : Formula S m) → S ^ (14 + n)
    fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
```

The ten numerals do not index the code domain. They label the ten constructor
clauses of the table specification, from zero through nine. `tgs φ` records
that every designated tag slot in `fr φ` contains the numeral matching its
constructor. This alignment lets the packaged table formula select the right
clause for each syntactic form.

```agda
    tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN
    tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
```

The table also needs the correct family of environments for every arity.
`htow φ` applies the established tower theorem to the components of `fr φ`:
the value in the tower slot is `Tower.tower Bs`, the carrier slot is `Bs`, and
the zero-tag slot contains the required numeral. Thus `towerAt` holds in the
extended environment, with no new tower argument needed here.

```agda
    htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩
    htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl
```

The domain of the canonical table is exactly the slot of formula keys. One
direction starts with a table entry and uses `inSlot` to put its key in
`slot Bs φ`; because the entry is obtained under propositional truncation,
elimination is into the membership proposition. The other direction uses
`total` to give, merely, a table value for every key in the slot.
`domAt-intro` combines these implications into `hdom φ`.

```agda
    hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩
    hdom φ = domAt-intro Ti Ci (fr φ)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ)))
                 (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h)
           , (λ h → total Bs φ (fst z) h))
```

The forward reading can now be stated precisely. Let `ψ` be a formula whose
constants are members of `fst Bs`. If slot `x` contains its genuine key
`keyS Bs ψ`, and slot `y` contains the satisfaction set of the translated
model-language formula `mapFo (asConst Bs) ψ`, then `satGraphAt B x y` holds.
The value is a set of satisfying environments, rather than a single truth
value. `graphAt-value` proves the claim by supplying the canonical recursion
witness to `graphAt-in`.

```agda
  graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
                → fst (lookup x γ) ≡ fst (keyS Bs ψ)
                → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
                → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-value {m} ψ qx qy = graphAt-in B x y γ
```

The existential witness is assembled from the five canonical components in
the order expected by `GraphWitAt`: the numeral assignment `numν`, the tower,
the slot, the satisfaction table, and the carrier. It is then wrapped in
propositional truncation, matching the existential semantics of the graph
formula. What remains is to certify that these chosen components satisfy the
carrier, tag, tower, closure, domain, entry, and table requirements.

```agda
    ∣ numν
    , (Tower.tower Bs
    , (slot Bs φ
    , (satTable Bs φ
    , (Bs
```

The carrier equation is reflexivity. The next three certificates say that the
ten tag slots contain the intended numerals, that the environment slot is the
tower over `Bs`, and that `slot Bs φ` is closed under the formula constructors
with immediate subformulas. This last property is what allows the recursive
table clauses at a compound formula key to consult entries at its immediate
subformula keys.

```agda
    , (refl
    , (tgs φ
    , (htow φ
    , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
```

The final requirements identify the table's domain, its selected entry, and
its clause specification. The previously proved `hdom φ` gives the domain
formula. For the entry, `keyBridge Bs ψ` relates the key of the carrier-language
formula to that of `φ`, while `qx` and `qy` transport the canonical entry to
slots `x` and `y`. Finally, `SlotHolds.holds` proves that the canonical table
satisfies `tableAt` from the same carrier, tags, tower, slot, and table. The
assembled witness therefore establishes the graph formula.

```agda
    , (hdom φ
    , (subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩)
         (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
    , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁
    where
```

Here `φ` is the model-language version of `ψ`. A constant of `ψ` is a member
of the underlying carrier, and `asConst Bs` equips that member with the
constructibility evidence needed to regard it as an element of `S`; `mapFo`
applies this constant map throughout the formula. The separate `keyBridge`
used above ensures that direct coding before this translation and internal
coding after it produce the same underlying key.

```agda
    φ : Formula S m
    φ = mapFo (asConst Bs) ψ
```

For the reverse reading, suppose `satGraphAt B x y` holds and slot `x` is the
genuine key of `ψ`. `graphAt-out` exposes the fourteen existential components
only under propositional truncation. The desired conclusion is an equality in
the cumulative hierarchy `V`, and `setIsSet` says that this equality type is a
proposition. Hence `PT.rec` may inspect each displayed graph witness locally
without choosing one globally.

```agda
  graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
               → fst (lookup x γ) ≡ fst (keyS Bs ψ)
               → ⟨ γ ⊨ satGraphAt B x y ⟩
               → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
  graphAt-only {m} ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)
```

Unpacking one graph witness gives a proposed table `T`, a code domain `C`, an
environment tower `E`, a carrier `b`, and all their certificates. The domain
`C` need not be the canonical slot; what matters is that it is subcode-closed,
that `T` satisfies the packaged table clauses, and that the genuine key lies
in `C`. The last fact follows by applying `domAt-out` to the displayed table
entry `ha`. With that membership and the same entry, `SatSoundC.pinned` applies
to `ψ` and forces its recorded value to be the canonical satisfaction set.

```agda
    where
    read : GraphWitAt B x y γ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
    read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) =
      SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12
        ψ (subst (λ u → ⟨ u ∈ fst C ⟩) qx
```

Both premises for pinning are read at the ambient key in slot `x`.
Transporting by `qx` turns the domain membership obtained from `hd` and `ha`
into membership of `keyS Bs ψ` in `C`, and turns `ha` itself into an entry of
`T` at that key and the value in slot `y`. The pinned theorem then returns
exactly the required equality: at a genuine formula key, any value admitted by
the graph is the satisfaction set of the translated formula.

```agda
             (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha))
        (lookup y γ)
        (subst (λ u → ⟨ pr u (fst (lookup y γ)) ∈ fst T ⟩) qx ha)
```

## A name, described at slots

The denotation body tests one candidate `z` at a time. Its first conjunct,
`z ∈ B`, restricts the set being described to the carrier. It then binds an
environment `c` and requires `c` to be the coded environment obtained by
putting `z` in front of the parameter environment `e`. At that point `c` and
`z` precede the ambient assignment, so the reference to `e` is shifted through
two binders.

```agda
DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero
```

The remaining three witnesses determine how the skeleton is evaluated. First
`k` is required to be the domain of the extended environment `c`. Next `key`
must belong to the code set in slot `C` and equal the pair of `k` with the
skeleton code `s`. Finally `v` is a value admitted by the satisfaction graph
for the carrier `B` at that key, and the last membership says `c ∈ v`. When
`C` is the carrier's genuine code set, these clauses say that the extended
environment satisfies the skeleton rather than merely consulting the graph at
an arbitrary key.

```agda
            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )
```

A meta-level name consists of an arity, a parameter-free formula, and a
parameter vector. `NameAt` represents these by an arity slot `a`, a skeleton
code slot `s`, and an environment slot `e`; its denotation slot `d` records the
set derived from those data. The first conjunct checks that the pair formed
from the successor of `a` and `s` belongs to the empty-alphabet code set. The
successor is essential: a name with `a` parameters needs one further variable
for the candidate member. The next conjunct requires `a` to be a member of the
model's natural numbers.

```agda
NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  FreeAt C₀ s a
  ∧̇ ( (var a ∈̇ con ωʟ)
```

The third conjunct makes `e` an environment with exact domain `a` and values
in `B`; in particular, it ties the parameter vector to the arity recorded in
the preceding slot. The last conjunct characterizes `d` extensionally. For
every candidate, membership in `d` is equivalent to satisfaction of
`DenoteBody`, whose first conjunct already restricts the candidate to `B`.
Thus `d` is derived from the three pieces of a name rather than stored as an
additional piece of the meta-level name.

```agda
    ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )
```

`DenoteOf z` is the meta-level payload corresponding to the four existential
layers of `DenoteBody`. It records an extended environment `c`, its proposed
domain `k`, a formula key, and a graph value `v`, together with all the
conditions connecting them. Keeping this data in one dependent tuple exposes
the witnesses needed to assemble the object-language formula while retaining
the dependencies of each later condition on the earlier choices.

```agda
module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where
  DenoteOf : (z : S) → Type (ℓ-suc ℓ)
  DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
```

The payload follows the semantic chain exactly. The first two satisfaction
proofs say that `c` extends the old environment and that `k` is its domain.
Membership of `key` in `C` certifies that the following graph lookup is made
at a genuine code when `C` is instantiated by `AllCodes B`. The explicit
equation then identifies that key with the pair of `k` and `s`. The last two
proofs say that `v` is the graph value at this key and that `c` belongs to
`v`. Here `v` is a set of satisfying environments, not a Boolean truth value.

```agda
      × ( ⟨ fst key ∈ fst (lookup C γ) ⟩
        × ( (fst key ≡ pr (fst k) (fst (lookup s γ)))
          × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
            × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )
```

`DenoteBody-in` turns this explicit payload into satisfaction of the body.
The carrier membership remains the outer conjunct, while the witnesses
`c`, `k`, `key`, and `v` are introduced in the same order as the four
existential binders. Most conditions are already stated as satisfaction
proofs. The exception is the equation defining `key`: the pairing formula's
adequacy path converts that set-theoretic equation into satisfaction of
`prAtL`.

```agda
  DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z
                → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
  DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp
```

Each object-language existential is interpreted by propositional truncation,
so the construction wraps every one of the four witnesses before closing the
proof. The final line closes these four layers from the graph value out to the
extended environment. Consequently the resulting satisfaction records that
suitable data exist, while the untruncated witnesses remain available only in
the input `DenoteOf z` used to build it.

```agda
      , ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁
```

`DenoteBody-out` preserves the same boundary in the reverse direction. The
outer carrier membership is available directly because it lies outside every
existential. The four witnesses, however, are exposed only within nested
propositional truncations. Each use of truncation elimination targets
`∥ DenoteOf z ∥₁`, again a proposition, so the proof may transform each local
choice of witnesses without selecting a tuple globally.

```agda
  DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
                 → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁
  DenoteBody-out z (hz , hc) = hz , PT.rec squash₁
    (λ { (c , (hc , hk)) → PT.rec squash₁
      (λ { (k , (hk , hkey)) → PT.rec squash₁
```

At the key layer, the body supplies satisfaction of the pairing formula,
whereas `DenoteOf` requires the decoded equation
`fst key ≡ pr (fst k) (fst (lookup s γ))`. Reading the pairing formula's
adequacy path in the forward direction produces precisely this equation. The
innermost map then retains the graph and membership proofs with the witness
`v`, and the surrounding eliminations rebuild the whole payload under one
propositional truncation.

```agda
        (λ { (key , (hi , (hp , hv))) → PT.map
          (λ { (v , (hg , hm)) → c , (k , (key , (v , (hc , (hk , (hi
            , ( subst ⟨_⟩
                  (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp
              , (hg , hm) ))))))) }) hv }) hkey }) hk }) hc
```

`NameAt-in` takes five inputs. The first three establish the fixed conjuncts:
the skeleton is parameter-free at the stated arity, the arity lies in the
model's natural numbers, and the parameter graph is an environment over the
carrier. The remaining two inputs give the two pointwise directions needed to
characterize the denotation. From `z ∈ d`, the first returns `z ∈ B` together
with an explicit `DenoteOf z`; conversely, the second turns `z ∈ B` and an
explicit `DenoteOf z` into `z ∈ d`.

```agda
module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where
  NameAt-in : ⟨ γ ⊨ FreeAt C₀ s a ⟩
            → ⟨ fst (lookup a γ) ∈ ω ⟩
            → ⟨ γ ⊨ envOverAt e a B ⟩
            → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
```

Both directions are stated separately for every candidate because `extAt`
expresses equality of sets by pointwise membership. They deliberately use an
untruncated `DenoteOf z`: this lemma is an introduction rule, so its caller
supplies the concrete data from which satisfaction of the body can be built.
Recovering such data from an arbitrary satisfaction of `NameAt` is a separate
adequacy argument, and its result in the following chapter remains under
propositional truncation.

```agda
               → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z)
            → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
               → ⟨ fst z ∈ fst (lookup d γ) ⟩)
            → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
  NameAt-in hf ha he into back =
```

The proof feeds these two directions to the introduction rule for `extAt`.
For `z ∈ d`, the first direction supplies carrier membership and a payload,
which `DenoteBody-in` converts into satisfaction of the body. Conversely,
satisfaction of the body is read by `DenoteBody-out` as carrier membership and
a propositionally truncated payload. Truncation elimination may then apply
the second input because its target, `z ∈ d`, is a proposition. Combining
this extensional characterization with the first three inputs establishes the
whole name formula.

```agda
    hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ
      (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd))
      (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ)))
                 (back z (DenoteBody-out B C s e γ z h .fst))
                 (DenoteBody-out B C s e γ z h .snd))))
```

## The order, with no recursion of its own

The comparison formulas next bind data in blocks, so references to the ambient
assignment must be shifted uniformly. `sh3` moves an ambient slot past three
new binders. In `LexAt` these binders hold an index `i` and the two values read
from the parameter environments at `i`, allowing the original slots for the
two environments and the parameter order to remain in scope. The same shift
later carries ambient slots past the skeleton, arity, and environment of a
competing name in `LeastNameAt`.

```agda
private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))
```

`sh6` performs the corresponding move past six binders. It is used when
`StepBody` binds two names, each represented by a skeleton, an arity, and a
parameter environment. The fully extended assignment therefore has the six
new values before the original one, while the carrier, the two order
relations, the two code sets, and the denotations being compared remain
ambient slots. These shifts preserve the intended references; they add no
ordering assumption and perform no comparison themselves.

```agda
  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = suc (suc (suc (suc (suc (suc i)))))
```

The parameter key asks for the first position at which two parameter
environments differ. `LexAt` begins by binding an element `i` of the set in the
arity slot. When that slot contains the numeral for an arity, its members are
exactly the numerals for smaller positions, so this bounded existential ranges
over the possible indices without introducing a separate order on indices.

```agda
LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
LexAt P a e₁ e₂ =
  ∃̇∈ (var a) (
    ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero)
           ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero
```

After choosing `i`, two existential witnesses give values `u` and `v` with
`e₁(i)=u` and `e₂(i)=v`, and a third application asserts that the ordered pair
of `u` and `v` belongs to the parameter relation `P`. The bounded universal
then considers every `j ∈ i`; for each such `j`, an existential witness `x`
must be a value of both environment graphs at `j`. Thus the formula says
"strictly ordered here, with a common value at every earlier position." Only
after the two environments are identified as single-valued graphs does a
common value imply equality of the corresponding parameters. In the later
adequacy argument, graph lookup and injectivity of the carrier embedding supply
precisely that implication. The formula itself performs no recursion.

```agda
             ∧̇ ( appAt (sh3 P) (suc zero) zero
               ∧̇ ∀̇∈ (var (suc (suc zero))) (
                    ∃̇ ( appAt (sh5 e₁) (suc zero) zero
                      ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )
```

The full name comparison now combines the three keys in their lexicographic
priority: skeleton code, arity, and parameter environment. Its first disjunct
applies the relation in slot `R` to `s₁` and `s₂`. By the adequacy of
application, this says that the ordered pair of the two skeleton codes belongs
to `R`. Keeping `R` as a slot makes the formula uniform; the later adequacy
theorem instantiates it with a relation representing the limit-stage code
order.

```agda
≺At : ∀ {n} → Fin n → Fin n
    → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n
≺At R P s₁ a₁ e₁ s₂ a₂ e₂ =
      appAt R s₁ s₂
  ∨̇ ( (var s₂ ≐ var s₁)
```

The second disjunct handles equal skeleton codes. It records the equality in
the direction `s₂ = s₁` and then offers the remaining two lexicographic cases:
either `a₁ ∈ a₂`, which means that the first arity is smaller when both slots
contain numerals, or `a₂ = a₁` and `LexAt P a₁ e₁ e₂` settles the comparison at
the first differing parameter. The orientations `s₂ = s₁` and `a₂ = a₁` match
the later transports that move the second name's code and parameter vector to
the first name's data.

```agda
    ∧̇ ( (var a₁ ∈̇ var a₂)
      ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )
```

To prove a reusable reading of `LexAt`, we isolate the formula occurring under
the agreement existential. At a previously considered position `j`, `Body`
requires one value `x` to satisfy both applications, hence to occur in both
environment graphs at `j`. In the extended assignment the five new entries are
`x`, `j`, `v`, `u`, and `i`, so each reference to an ambient environment is
shifted past five binders.

```agda
module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where
  private
    Body : Formula S (suc (suc (suc (suc (suc n)))))
    Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero
```

With `i`, `u`, and `v` fixed, `Inner i u v` records the body left by the first
three existential binders. Its first two components say that the graphs `e₁`
and `e₂` contain the pairs `(i,u)` and `(i,v)`. The third says that the pair
`(u,v)` belongs to the relation `P`. These are still satisfaction statements
for `appAt`; their decoded membership form will be recorded separately so that
the two presentations can be related explicitly.

```agda
    Inner : (i u v : S) → Type (ℓ-suc ℓ)
    Inner i u v =
      ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩
      × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩
        × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩
```

The fourth component of `Inner` is agreement below `i`. For every model element
`j` belonging to `i`, it supplies the semantic existential
`∃[ x ∶ S ]` saying that one `x` satisfies `Body`. This existential is a
propositional truncation: it retains the existence of a common value at `j`
without exposing a chosen value as data. The bounded universal is therefore
read as a function that supplies one such truncated existence for each
`j ∈ i`.

```agda
          × ((j : S) → ⟨ fst j ∈ fst i ⟩
             → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩) ) )
```

`Agrees i` states the same agreement after decoding the two applications. For
every `j ∈ i`, merely there is an element `x : S` such that the pair formed
from the underlying sets of `j` and `x` belongs to both graphs `e₁` and `e₂`.
When `i` is an arity numeral, its members represent precisely the earlier
positions. This definition records only a common graph value. Equality of the
corresponding meta-level parameters is derived later from the known environment
graphs and the injectivity of the carrier embedding.

```agda
  Agrees : (i : S) → Type (ℓ-suc ℓ)
  Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩
           → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                          × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁
```

`Differs` collects the complete decoded witness for a first difference. It
contains an index `i`, values `u` and `v`, membership of `i` in the set stored
at the arity slot, graph memberships for `(i,u)` and `(i,v)`, the strict
parameter comparison at that position, and `Agrees i`. When the arity slot is
a numeral and the two graph slots are parameter environments of that arity,
these fields are exactly the data needed for a lexicographic first difference.

```agda
  Differs : Type (ℓ-suc ℓ)
  Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ]
    ( ⟨ fst i ∈ fst (lookup a γ) ⟩
    × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩
      × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩
```

The strict comparison field has the same relational form as the code case of
`≺At`: the ordered pair of the underlying values of `u` and `v` belongs to the
set in slot `P`. The final field `Agrees i` records a common value at every
earlier position; for the intended single-valued environment graphs, this
certifies that no earlier parameters differ. Thus `Differs` separates the
mathematical content of the first-difference witness from the object-language
binders used to express it.

```agda
        × ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )
```

The map `pack` converts only the agreement component of `Inner` into
`Agrees`; the first three components are irrelevant to this local conversion.
For a fixed `j ∈ i`, a witness `x` for the semantic existential comes with two
satisfactions of `appAt`. Applying `appAt-adequate` to each turns them into the
two graph memberships required by `Agrees`, while preserving the same witness
`x`.

```agda
  private
    pack : (i u v : S) → Inner i u v → Agrees i
    pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩
```

This conversion is performed inside the existing propositional truncation.
`PT.map` sends every possible witness and its two application proofs to the
same witness with two membership proofs. Since the target is again a truncated
existence, no representative is extracted and no choice principle is used.
Pointwise mapping is enough to obtain `Agrees i` for every earlier position.

```agda
               (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁
           , subst ⟨_⟩
               (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) })
      (hj j hj')
```

`unpack` provides the converse conversion needed to satisfy the formula. From
`Agrees i` and a position `j ∈ i`, it receives a truncated common-value
witness. For each representative `x`, it keeps that witness and prepares to
turn the two graph memberships back into satisfactions of the two applications
in `Body`.

```agda
    unpack : (i u v : S) → Agrees i
           → (j : S) → ⟨ fst j ∈ fst i ⟩
           → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩
    unpack i u v hj j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
```

The same adequacy paths are now used in the reverse direction. Each membership
proof is transported along the symmetric path of `appAt-adequate`, producing
the corresponding conjunct of `Body`. Again `PT.map` keeps the construction
inside the truncated existential, so `unpack` proves the required semantic
existence without selecting a common value globally.

```agda
         , ( subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁
           , subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) })
      (hj j hj')
```

`LexAt-in` starts from the explicit data in `Differs`. The index `i` and the
values `u` and `v` become the witnesses for the bounded existential and the two
following existentials, with `hi` certifying the bound. In the extended
assignment `γ₃ = v ∷ u ∷ i ∷ γ`, the first two graph memberships are
transported backward along `appAt-adequate` to satisfy the applications for
`e₁(i)=u` and `e₂(i)=v`. The remaining relation and agreement fields fit the
same conjunction, with `unpack` supplying its bounded-universal component.

```agda
  LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩
  LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj)))))))
    = ∣ i , (hi , ∣ u , ∣ v
    , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁
      , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂
```

The final field of `Differs` completes the introduction proof. The membership
of `(u,v)` in `P` is transported backward along `appAt-adequate` to satisfy the
third application, while `unpack` turns agreement below `i` into the bounded
universal's semantic form. The assignment `γ₃ = v ∷ u ∷ i ∷ γ` makes the
binder order explicit; the surrounding constructors then close the
existentials for `v`, `u`, and `i`, from the inside out.

```agda
        , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp
          , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁
    where
    γ₃ : S ^ (suc (suc (suc n)))
    γ₃ = v ∷ u ∷ i ∷ γ
```

Reading `LexAt` outward must preserve the witness boundary created by its
existentials. Accordingly, `LexAt-out` targets `∥ Differs ∥₁`, a proposition,
and eliminates the outer truncation only into that target. The local function
`atValue` performs the mathematical decoding: once particular `i`, `u`, and
`v`, the bound proof, and the remaining satisfaction data are available inside
the eliminations, it builds an untruncated `Differs` record. No such record is
chosen outside those local scopes.

```agda
  LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁
  LexAt-out = PT.rec squash₁ atIndex
    where
    atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs
    atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v
```

The first half of `atValue` recovers the index and the two graph lookups. The
bound proof `hi` already has the form required by `Differs`. Reading the two
adequacy paths forward converts satisfaction of the applications into
membership of `(i,u)` in `e₁` and membership of `(i,v)` in `e₂`. Thus the two
values remain attached to the same index at which the formula found them.

```agda
      , ( hi
        , ( subst ⟨_⟩
              (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁
          , ( subst ⟨_⟩
                (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂
```

The third application is decoded in the same way, yielding membership of
`(u,v)` in the parameter relation `P`. The function `pack` supplies the final
field by translating the bounded agreement from application form to the two
graph memberships required by `Agrees i`. These pieces form one explicit
`Differs` record inside `atValue`; the surrounding eliminations will retain
only its propositional truncation.

```agda
            , ( subst ⟨_⟩
                  (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp
              , pack i u v h ) ) ) ) ))
```

The innermost existential supplies the second value `v` together with
`Inner i u v`, but only within its truncation. The handler `atSecond` uses each
locally available pair `(v,h)` to build `Differs` by `atValue` and immediately
places the result in `∥ Differs ∥₁`. This is exactly the permitted elimination:
the witness is used to prove a proposition and is not exposed by the result.

```agda
    atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
             → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁
    atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁
```

One layer farther out, `atFirst` receives a particular first value `u` and a
truncated existence of the second value. It eliminates that inner truncation
with `atSecond`, whose result is again `∥ Differs ∥₁`. The argument therefore
passes from the first value to the completed first-difference record without
ever requiring a globally available `v`.

```agda
    atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
            → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁
    atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h
```

Finally `atIndex` receives an index `i`, its proof `hi` of lying below the
arity, and the truncated remainder beginning with `u`. Eliminating that
remainder with `atFirst` completes the outward reading. Taken together, the
three handlers follow the existential nesting from `i` to `u` to `v`, while
every elimination has the same propositional target. Hence `LexAt-out`
establishes that a first-difference record merely exists, with no choice of its
index or values.

```agda
    atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩
                         × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ )
            → ∥ Differs ∥₁
    atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h
```

## Reading the comparison, and one step of the family

The meta-level payload `Below` now arranges the three comparison keys in the
same priority as `≺At`. Its outer sum says either that the ordered pair of
skeleton codes `(s₁,s₂)` belongs to the relation in slot `R`, or that the codes
are equal and a later key decides. A value of this sum explicitly identifies a
branch and carries its evidence; the definition does not assert that such a
branch can be decided for arbitrary slot values. This distinction matters
because object-language disjunction is interpreted by propositional
truncation.

```agda
module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where
  Below : Type (ℓ-suc ℓ)
  Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩
        ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
```

Under equal skeleton codes, the inner sum first offers the arity comparison
`a₁ ∈ a₂`. When the slots contain arity numerals, this membership says that
the first arity is smaller. If the arities are equal instead, `Differs`
supplies the first-difference evidence for the parameter key. The equalities
are deliberately oriented as `s₂ = s₁` and `a₂ = a₁`, matching the later
transport of the second name's data to the first name's types.

```agda
            ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
              × Differs P a₁ e₁ e₂ γ ) ) )
```

`≺At-in` translates an explicit value of `Below` into satisfaction of the
comparison formula. In the code branch, the relation membership is transported
backward along `appAt-adequate` and introduced as the outer left disjunct. In
the arity branch, the code equality accompanies the outer right disjunct, and
the arity membership enters the inner left disjunct. These are introduction
steps only: the supplied branch evidence is packaged into the truncated
semantics of each object-language disjunction.

```agda
  ≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
  ≺At-in (inl h) =
    ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁
  ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁
  ≺At-in (inr (q , inr (q' , h))) =
```

The parameter branch takes the remaining route through both disjunctions. It
carries the code and arity equalities into their right branches, then invokes
`LexAt-in` on the supplied `Differs` record. Thus the same first-difference
data already decoded above becomes satisfaction of the parameter clause. All
three cases of `Below` are therefore inserted into `≺At` without searching for
a branch or extracting any existential witness.

```agda
    ∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁
```

The reverse direction has a necessarily weaker target:
`≺At-out` returns `∥ Below ∥₁`. Satisfaction of the outer object-language
disjunction is itself truncated, so `PT.rec` may inspect a branch only while
constructing this proposition. The local function `outer` separates the code
case from the equal-code case. In the latter it retains the equality
`s₂ = s₁` and passes the still-unsorted inner disjunction to `inner`.

```agda
  ≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁
  ≺At-out = PT.rec squash₁ outer
    where
    inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
```

Given the code equality, `inner` reads the two remaining keys. An arity
membership immediately yields the middle case of `Below`. Otherwise the
payload contains the arity equality `a₂ = a₁` and satisfaction of `LexAt`, so
only the first-difference component remains to be decoded. The signature keeps
these alternatives explicit while fixing the code equality shared by both.

```agda
          ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
            × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ )
          → ∥ Below ∥₁
    inner q (inl h) = ∣ inr (q , inl h) ∣₁
    inner q (inr (q' , h)) =
```

In the parameter case, `LexAt-out` supplies only `∥ Differs ∥₁`, exactly as the
existential semantics requires. `PT.map` sends each locally represented
`Differs` record to the third case of `Below`, adjoining the already known code
and arity equalities. The result remains under one propositional truncation, so
the conversion carries existence to existence and never asks for a chosen
first-difference witness.

```agda
      PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)
```

The type of `outer` is the semantic split at the first comparison key. Its left
side is satisfaction of the application of `R` to the two skeleton slots; its
right side retains the equality `s₂ = s₁` together with satisfaction of the
remaining arity-or-parameter disjunction. Decoding the left side yields the
code case of `Below`, while eliminating the inner disjunction uses `inner`.
This two-stage reading mirrors the nesting of `≺At` and keeps the final result
at `∥ Below ∥₁`, where neither disjunction is turned into a chosen branch.

```agda
    outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩
          ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
            × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂)
                    ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ )
          → ∥ Below ∥₁
```

The last two clauses finish the outward reading of the comparison. In the code
branch, `appAt-adequate` converts satisfaction of the relation application into
membership of the ordered pair of skeleton codes in `R`, producing the first
case of `Below`. In the equal-code branch, the inner object-language
disjunction is still propositionally truncated, so it is eliminated only into
`∥ Below ∥₁`. Thus every one of the three comparison keys can be recovered, but
the formula does not reveal which key decided the comparison outside the
truncation.

```agda
    outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁
    outer (inr (q , h)) = PT.rec squash₁ (inner q) h
```

To describe the comparison of two least names, the body of the step needs six
fresh slots. The first three indices are fixed here: `s6a`, `a6a`, and `e6a`
refer respectively to the first name's skeleton code, arity numeral, and
parameter environment. After all six binders have been entered, these data lie
at de Bruijn positions five, four, and three. Giving the positions names keeps
the later formulas about leastness and comparison readable while leaving the
binder arithmetic in one place.

```agda
private
  s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n))))))
  s6a = suc (suc (suc (suc (suc zero))))
  a6a = suc (suc (suc (suc zero)))
  e6a = suc (suc (suc zero))
```

The remaining indices `s6b`, `a6b`, and `e6b` point to positions two, one,
and zero, where the second name's data will be found. This reversal is the
usual de Bruijn effect: the witnesses are bound in the order
`s₁,a₁,e₁,s₂,a₂,e₂`, while each new witness is prepended to the environment.
Consequently the fully extended environment is
`e₂ ∷ a₂ ∷ s₂ ∷ e₁ ∷ a₁ ∷ s₁ ∷ γ`, and the six indices select precisely the
two intended triples.

```agda
  s6b = suc (suc zero)
  a6b = suc zero
  e6b = zero
```

A least name is expressed as a property of name data already occupying the
slots `s`, `a`, and `e`. Its first conjunct requires those data to satisfy
`NameAt` and hence to denote `d`. The second conjunct universally quantifies
over a competing skeleton code, arity numeral, and parameter environment. The
three nested universals place that competitor at positions two, one, and zero,
while `sh3` keeps the carrier, both code sets, and the denotation `d` referring
to their original slots.

```agda
LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n
            → Fin n → Fin n → Fin n → Fin n → Formula S n
LeastNameAt R P B C C₀ s a e d =
  NameAt B C C₀ s a e d
  ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)
```

The implication restricts attention to competitors that are also names of the
same `d`; names denoting other sets are irrelevant to this minimum. Its
conclusion negates `≺At competitor current`, so no competing name of `d`
strictly precedes the current one in the three-key order. This formula only
states leastness. It neither searches for a name nor removes a propositional
truncation to select one. The explicit least-name construction belongs to the
meta-language naming development and uses its excluded-middle hypothesis.

```agda
                      (suc (suc zero)) (suc zero) zero (sh3 d)
             ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                        (sh3 s) (sh3 a) (sh3 e)) )))
```

Repeated existential elimination will need to change the property carried by a
witness without choosing that witness globally. The helper `exists-map`
captures exactly this operation. If each `B x` gives merely a `C x`, then mere
existence of a pair `(x , B x)` gives mere existence of `(x , C x)`. The outer
`PT.rec` eliminates the original propositional truncation into another
propositionally truncated type, and the inner `PT.map` retains the same `x`
while transforming its second component. At no point does the result expose a
particular witness of `A`.

```agda
private
  exists-map : {A : Type (ℓ-suc ℓ)} {B C : A → Type (ℓ-suc ℓ)}
             → ((x : A) → B x → ∥ C x ∥₁)
             → ∥ Σ A B ∥₁ → ∥ Σ A C ∥₁
  exists-map f = PT.rec squash₁ (λ { (x , h) → PT.map (x ,_) (f x h) })
```

The operator `∃₆` binds six object-language variables around an arbitrary
body. Its intended use is to supply the two triples of data needed for two
names, but the operator itself does not mention names, leastness, or an order.
Keeping this binder frame separate lets its semantic introduction and
elimination rules be proved once for any formula with six additional free
positions; the mathematical conditions on the witnesses will be supplied by
`StepBody`.

```agda
∃₆ : ∀ {n} → Formula S (suc (suc (suc (suc (suc (suc n)))))) → Formula S n
∃₆ φ = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ φ)))))
```

For a body `φ` and an environment `γ`, `Six` records the untruncated data that
can introduce the six existentials: witnesses `s₁,k₁,p₁,s₂,k₂,p₂` together
with satisfaction of `φ`. The names `k` and `p` anticipate their later roles
as arity numerals and parameter environments; at this generic stage they are
simply elements of the carrier `S`. Since successive binders prepend their
witnesses, the satisfaction environment lists them in reverse order as
`p₂,k₂,s₂,p₁,k₁,s₁` before the original `γ`.

```agda
module _ {n : ℕ} (φ : Formula S (suc (suc (suc (suc (suc (suc n))))))) (γ : S ^ n)
         where
  Six : Type (ℓ-suc ℓ)
  Six = Σ[ s₁ ∈ S ] Σ[ k₁ ∈ S ] Σ[ p₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ k₂ ∈ S ] Σ[ p₂ ∈ S ]
          ⟨ (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) ⊨ φ ⟩
```

The introduction rule starts with all six witnesses explicitly available in a
value of `Six`. It supplies them to the six existential binders in their
binding order, wrapping the remaining satisfaction proof in the propositional
truncation contributed by each existential. No search or choice is involved:
the witnesses are input data. The nested constructors also explain why the
environment seen by the body has the reverse order recorded in the definition
of `Six`.

```agda
  ∃₆-in : Six → ⟨ γ ⊨ ∃₆ φ ⟩
  ∃₆-in (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , h)))))) =
    ∣ s₁ , ∣ k₁ , ∣ p₁ , ∣ s₂ , ∣ k₂ , ∣ p₂ , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
```

The outward rule begins with satisfaction of the six-fold existential and
must end in `∥ Six ∥₁`, rather than in an exposed six-tuple. Each use of
`exists-map` crosses one existential layer while retaining its locally
available witness inside the common propositional target. The chain handles
`s₁`, `k₁`, `p₁`, `s₂`, and `k₂` in turn. At the innermost layer, `PT.map`
passes the pair consisting of `p₂` and the body's satisfaction proof into the
same final truncated payload.

```agda
  ∃₆-out : ⟨ γ ⊨ ∃₆ φ ⟩ → ∥ Six ∥₁
  ∃₆-out = exists-map (λ s₁ →
    exists-map (λ k₁ →
      exists-map (λ p₁ →
        exists-map (λ s₂ →
```

After the fifth application of `exists-map`, the innermost existential already
has the shape needed for the last component, so the identity map suffices.
Together, `∃₆-in` and `∃₆-out` express the semantic content of the binder frame
with the correct asymmetry: explicit six-witness data introduces the formula,
whereas satisfaction of the formula yields only the mere existence of such
data. This generic result can now be specialized without reopening any of the
six truncations.

```agda
          exists-map (λ k₂ → PT.map (λ p → p))))))
```

The concrete body places three conditions on the two triples selected by the
six indices. The first triple must satisfy `LeastNameAt` for `x`, and the
second must satisfy it for `y`. Both use the same carrier and the same code
sets, while `R` and `P` provide the two relation slots used by name comparison.
All seven surrounding slots are shifted by `sh6`, since the body reads them
through the six newly bound witnesses.

```agda
StepBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
         → Formula S (suc (suc (suc (suc (suc (suc n))))))
StepBody R P B C C₀ x y =
    LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x)
  ∧̇ ( LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y)
```

The third condition compares the two triples with `≺At`, placing the name of
`x` strictly before the name of `y`. Hence `StepBody` says precisely that two
least names over one carrier have been supplied and that the first precedes
the second in the three-key name order. It contains no comparison of the
stages at which `x` and `y` are born, no outer recursive table, and no claim
that the represented relation is well-founded. Those belong to the larger
construction in which this one-step description is used.

```agda
    ∧̇ ≺At (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b )
```

`StepAt` closes `StepBody` with the six existential binders. As an
object-language formula, it asserts merely that there are data for a least
name of `x`, data for a least name of `y`, and a comparison placing the first
before the second. The formula describes this single comparison branch; it
does not itself produce either least name, perform the surrounding stage
recursion, or prove well-foundedness. Its existential semantics also means
that reading a satisfied `StepAt` outward must preserve propositional
truncation.

```agda
StepAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
StepAt R P B C C₀ x y = ∃₆ (StepBody R P B C C₀ x y)
```

For fixed slots and environment, `StepOf` specializes the generic type `Six`
to `StepBody`. An element therefore contains six explicit carrier elements and
a proof that, in the reversed extended environment, they satisfy the two
least-name conditions and the name comparison. Naming this untruncated payload
separates it from the proposition expressed by `StepAt`: the following
introduction rule can consume a `StepOf` directly, while the outward rule can
return only `∥ StepOf ∥₁`. This is the precise witness boundary of the
six-binder step formula.

```agda
module _ {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) where
  StepOf : Type (ℓ-suc ℓ)
  StepOf = Six (StepBody R P B C C₀ x y) γ
```

With the six witnesses and the proof of the body already present in `StepOf`,
the introduction direction is immediate. Each witness is placed under its
existential quantifier in binding order, so the resulting assignment satisfies
`StepAt`. This step uses the supplied proofs of the two least-name conditions
and of the comparison; it does not construct any name.

```agda
  StepAt-in : StepOf → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
  StepAt-in = ∃₆-in (StepBody R P B C C₀ x y) γ
```

In the converse direction, satisfaction of `StepAt` can be unpacked only as
`∥ StepOf ∥₁`. Thus there merely exist two triples satisfying the two
least-name formulas, together with satisfaction of the comparison formula
from the first triple to the second. The
propositional truncation preserves this existence while withholding the six
particular witnesses, exactly as required by the semantics of existential
quantification.

```agda
  StepAt-out : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ StepOf ∥₁
  StepAt-out = ∃₆-out (StepBody R P B C C₀ x y) γ
```

## Against the names the meta-language built

To compare the formula with the intended meta-level relation, fix a
constructible set `A` and a strict well-order `w` on its carrier `⟪ A ⟫`.
Names over `A` take every parameter from this carrier, so `w` supplies exactly
the order needed for their parameter vectors. The resulting adequacy argument
is relative to these data and therefore applies to any constructible set
equipped with such an order on its carrier.

```agda
module Adequacy (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where
  private
    module NM = Naming A w
```

The naming construction now provides the type `Name` and the comparisons to be
matched. A name of arity `k` contains a parameter-free formula with `suc k`
variable positions and a vector of exactly `k` parameters. Its formula code is
derived from that formula, and `_≺ₙ_` compares names by code first, arity
second, and parameter vector last. Renaming the relation of `w` to `_≺ₚ_`
simply records its role as the parameter order.

```agda
  open NM using ( Name; arity; params; codeOf; _≺ᵥ_; _≺ₙ_ )
  open SWO w using () renaming ( _<∙_ to _≺ₚ_ )
```

The recursive vector order is compared with an explicit first-difference
relation `Lex`. For two vectors of the same length, `Lex p q` chooses an index
`i`, requires the entry of `p` there to precede the entry of `q` under
`_≺ₚ_`, and requires equality of the entries at every `j` with `j<i`. Unlike
the object-language agreement formula, this meta-level relation can state
entry equality directly and needs no common graph value as an intermediary.

```agda
  Lex : ∀ {k} → Vec ⟪ A ⟫ k → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ)
  Lex {k} p q = Σ[ i ∈ Fin k ]
    ( (lookup i p ≺ₚ lookup i q)
    × ((j : Fin k) → toℕ j < toℕ i → lookup j p ≡ lookup j q) )
```

The map from `Lex` to the recursive order follows the location of the first
difference. At index zero, the strict comparison of the heads is already the
first clause of `_≺ᵥ_`. At a successor index, agreement below that index makes
the two heads equal, while the same witness with its index decreased compares
the tails. This is structural recursion on the vectors and uses no classical
principle.

```agda
  lex-vec : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Lex p q → p ≺ᵥ q
  lex-vec (x ∷ p) (y ∷ q) (zero  , (h , _)) = inl h
  lex-vec (x ∷ p) (y ∷ q) (suc i , (h , ag)) =
    inr (ag zero (suc-≤-suc zero-≤) , lex-vec p q (i , (h , λ j hj → ag (suc j) (suc-≤-suc hj))))
```

For the reverse map, follow the two clauses of `_≺ᵥ_`. An order proof for two
empty vectors is impossible. If the nonempty vectors are ordered because their
heads are strictly ordered, index zero witnesses `Lex`; no smaller index
exists, so the agreement condition is vacuous.

```agda
  vec-lex : ∀ {k} (p q : Vec ⟪ A ⟫ k) → p ≺ᵥ q → Lex p q
  vec-lex []      []      h = Empty.rec* h
  vec-lex (x ∷ p) (y ∷ q) (inl h) = zero , (h , λ j hj → Empty.rec (¬-<-zero hj))
  vec-lex (x ∷ p) (y ∷ q) (inr (e , h)) = suc (vec-lex p q h .fst)
    , ( vec-lex p q h .snd .fst
```

In the remaining clause, the heads are equal and the tails are recursively
ordered. Applying the induction hypothesis to the tails yields their first
differing index; shifting it to a successor gives the corresponding index in
the original vectors. The supplied head equality proves agreement at position
zero, the first position below that shifted index.

```agda
      , step )
    where
    step : (j : Fin (suc _)) → toℕ j < suc (toℕ (vec-lex p q h .fst))
         → lookup j (x ∷ p) ≡ lookup j (y ∷ q)
    step zero    _  = e
```

At every other position below the shifted index, removing one successor from
the numerical inequality reduces the claim to the tails' own agreement. This
completes the reverse direction. Hence the explicit first-difference relation
and the recursive vector order coincide, allowing the parameter argument to
pass between their two presentations without changing the comparison.

```agda
    step (suc j) hj = vec-lex p q h .snd .snd j (pred-≤-pred hj)
```

## The parameters, on both sides

Formula codes are compared by a second pre-existing order. Each `codeOf t`
lies in the limit stage, whose strict well-order is `limitOrder`; writing its
relation as `_≺ˡ_` makes the code key explicit alongside the parameter key
`_≺ₚ_`. No new ordering is defined here: these are precisely the two orders
whose internal representations enter the three-key name comparison.

```agda
  open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )
```

A parameter is an element of the small carrier `⟪ A ⟫`, so it includes both an
underlying set and evidence that the set belongs to `A`. The map `ix` forgets
the membership evidence and retains the underlying set in `V`. This canonical
embedding is the common representation used when parameter values occur in
environment graphs and in ordered pairs belonging to the represented relation.

```agda
  ix : ⟪ A ⟫ → V ℓ
  ix m = ⟪ A ⟫↪ m
```

The same underlying set can also be regarded as an element of the constructible
model. Since `A` is constructible and `ix m` belongs to `A`, transitivity of
constructibility shows that `ix m` is constructible. Pairing the set with this
proof gives `ixL m : S`, the form required when a parameter is used as an
object-language value.

```agda
  ixL : ⟪ A ⟫ → S
  ixL m = ix m , isL-trans (∈∈ₛ {a = ix m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) pA
```

For a name `t`, the family `pfam t` reads its parameter vector pointwise. Its
domain is `Fin (arity t)`, and its value at `i` is the underlying `V`-set of
the parameter stored at that index. Thus the arity fixes the domain
definitionally, and the graph `env (pfam t)` gives the internal environment
representation of exactly that parameter vector.

```agda
  pfam : (t : Name) → Fin (arity t) → V ℓ
  pfam t i = ix (lookup i (params t))
```

No information about a carrier element is lost by passing to its underlying
set. The canonical map `⟪ A ⟫↪` is an embedding, hence `ix u ≡ ix v` implies
`u ≡ v`. This injectivity is essential in the reverse parameter argument:
when two environment graphs share a value at an earlier index, equality of
their underlying `V`-sets can be read back as equality of the corresponding
entries of the parameter vectors.

```agda
  ix-inj : (u v : ⟪ A ⟫) → ix u ≡ ix v → u ≡ v
  ix-inj u v = isEmbedding→Inj isEmb⟪ A ⟫↪ u v
```

It remains to state what the two internal relation sets must represent. For
codes, `Rrep` reads membership of the ordered pair of `u` and `v` in `Rs` as
`u ≺ˡ v`, while `Rfill` proves that membership from the comparison. For
parameters, `Prep` and `Pfill` give the same two directions between membership
of the pair of their `ix`-images in `Ps` and `u ≺ₚ v`. These four laws are
hypotheses. Under them, the three-key formula is adequate for any two
constructible relation sets with these representations; neither relation is
constructed here.

```agda
  module Keys (Rs Ps : S)
              (Rrep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩ → u ≺ˡ v)
              (Rfill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩)
              (Prep : (u v : ⟪ A ⟫) → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩ → u ≺ₚ v)
              (Pfill : (u v : ⟪ A ⟫) → u ≺ₚ v → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩)
```

To apply the four representation laws to a particular parameter comparison,
fix two names together with the object-language slots in which their data are
read. The local argument is governed by five identifications: one for the
parameter relation, one for the first arity, one between the two arities, and
one for each parameter environment. Under these hypotheses, it will translate
between the explicit first difference `Lex` and the graph-based record
`Differs` in both directions.

```agda
              where
```

The first four identifications establish the common frame. The slot `P` holds
the relation set `Ps`; the slot `a₁` holds the numeral for `t₁`'s arity; and
`qk : arity t₂ ≡ arity t₁` makes the two parameter vectors comparable at one
length. Finally, `e₁` holds the graph of `pfam t₁`, whose value at an index is
the embedded parameter of the first name. Notice that `qk` is an equality of
natural-number arities, rather than an equation for an object-language slot.

```agda
    module _ {n : ℕ} (P a₁ e₁ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name)
             (qP : fst (lookup P γ) ≡ fst Ps)
             (qa : fst (lookup a₁ γ) ≡ # (arity t₁))
             (qk : arity t₂ ≡ arity t₁)
             (q₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
```

The fifth identification gives the second environment the same domain. First
transport `params t₂` along `qk` from length `arity t₂` to length `arity t₁`;
then embed each transported entry into `V` and take the resulting graph. Thus
both environments can be queried by an index in `Fin (arity t₁)`. The private
families introduced next name their entries before and after this transport,
beginning with `pr₁` for the first vector.

```agda
             (q₂ : fst (lookup e₂ γ)
                 ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) qk (params t₂)))))
             where
      private
        pr₁ : Fin (arity t₁) → ⟪ A ⟫
```

At an index `i` of the common length, `pr₁ i` is simply the entry found in
`t₁`'s parameter vector. It remains an element of the small carrier `⟪ A ⟫`;
the embedding `ix` is applied only when this parameter is placed into an
environment graph or an ordered pair in the model. Keeping these two levels
separate lets the parameter order act on carrier elements themselves.

```agda
        pr₁ i = lookup i (params t₁)
```

The companion family `pr₂` reads the transported vector of `t₂`. It has the
same domain as `pr₁`, but its values are still carrier elements belonging to
the second name. Consequently `pr₁ i ≺ₚ pr₂ i` and `pr₁ j ≡ pr₂ j` are
well-typed statements at every common index, precisely the strict comparison
and prior agreement required by `Lex`.

```agda
        pr₂ : Fin (arity t₁) → ⟪ A ⟫
        pr₂ i = lookup i (subst (Vec ⟪ A ⟫) qk (params t₂))
```

The first graph can now be read at an exact index. Suppose the pair with key
`# (toℕ i)` and value `fst u` belongs to the set in slot `e₁`. Transporting
this membership along `q₁` places it in `env (pfam t₁)`, and `lookup-spec`
identifies its second component with that graph's unique value. Since this
value is `ix (pr₁ i)`, `at₁` recovers the equality
`fst u ≡ ix (pr₁ i)`.

```agda
        at₁ : (i : Fin (arity t₁)) (u : S)
            → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₁ γ) ⟩ → fst u ≡ ix (pr₁ i)
        at₁ i u h = subst ⟨_⟩ (lookup-spec (pfam t₁) i (fst u))
          (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₁ h)
```

The same reading applies to the second graph, with the transported family in
place of `pfam t₁`. Membership of the pair at key `# (toℕ i)` is first moved
along `q₂`; `lookup-spec` then yields `fst u ≡ ix (pr₂ i)`. Hence `at₁` and
`at₂` give the functional consequence needed here: they identify every value
found at a valid index with the particular parameter entry represented there.

```agda
        at₂ : (i : Fin (arity t₁)) (u : S)
            → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₂ γ) ⟩ → fst u ≡ ix (pr₂ i)
        at₂ i u h = subst ⟨_⟩ (lookup-spec (λ j → ix (pr₂ j)) i (fst u))
          (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₂ h)
```

The reverse use of `lookup-spec` supplies the canonical entry of the first
graph. Reflexivity says that `ix (pr₁ i)` is the value prescribed by
`pfam t₁` at `i`; reading the lookup equation backward turns this equality
into membership in `env (pfam t₁)`. Transport along the reverse of `q₁` then
places the same pair in the set actually stored at `e₁`. This is the witness
`put₁ i`.

```agda
        put₁ : (i : Fin (arity t₁))
             → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ fst (lookup e₁ γ) ⟩
        put₁ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ z ⟩) (sym q₁)
          (subst ⟨_⟩ (sym (lookup-spec (pfam t₁) i (ix (pr₁ i)))) refl)
```

The witness `put₂ i` is constructed in exactly the same way for the
transported second family and the slot `e₂`. Together, the four lemmas give
both directions of graph lookup for the two names: `at₁` and `at₂` identify
any alleged values, while `put₁` and `put₂` exhibit the prescribed ones. The
forward translation will use the latter pair to build `Differs`; the reverse
translation will use the former pair to recover `Lex`.

```agda
        put₂ : (i : Fin (arity t₁))
             → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ fst (lookup e₂ γ) ⟩
        put₂ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ z ⟩) (sym q₂)
          (subst ⟨_⟩ (sym (lookup-spec (λ j → ix (pr₂ j)) i (ix (pr₂ i)))) refl)
```

An index used by `Lex` is a finite number, whereas an index carried by
`Differs` must be an element of the constructible model. The helper `numAt`
crosses this small boundary: it pairs the von Neumann numeral `# m` with its
constructibility proof `numL m`. It does not by itself assert that the numeral
lies below an arity; that membership will be supplied separately from the
finite-index bound.

```agda
        numAt : (m : ℕ) → S
        numAt m = # m , numL m
```

For the forward translation, an element of `Lex` supplies a finite index `i`,
a strict comparison `hlt` at that index, and equality `agree` at every earlier
index. The record `Differs` begins with the model element
`numAt (toℕ i)` and the two values `ixL (pr₁ i)` and `ixL (pr₂ i)`. Because a
finite index is smaller than its length, `#mono` turns `toℕ<n i` into
membership of its numeral in the arity numeral; transport along `qa` places
that membership in the arity slot.

```agda
      lex-fill : Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂))
               → Differs P a₁ e₁ e₂ γ
      lex-fill (i , (hlt , agree)) = numAt (toℕ i)
        , ( ixL (pr₁ i) , ( ixL (pr₂ i)
        , ( subst (λ z → ⟨ # (toℕ i) ∈ z ⟩) (sym qa)
```

The next fields certify what happens at the differing index. The witnesses
`put₁ i` and `put₂ i` put the two embedded parameter values into their
respective environment graphs. The representation law `Pfill` turns
`hlt : pr₁ i ≺ₚ pr₂ i` into membership of their ordered pair in `Ps`; transport
along the reverse of `qP` moves that membership to the relation set stored in
slot `P`. Thus the three membership fields of `Differs` express exactly the two
lookups and the strict parameter comparison.

```agda
              (#mono (toℕ i) (arity t₁) (toℕ<n i))
          , ( put₁ i
            , ( put₂ i
              , ( subst (λ z → ⟨ pr (ix (pr₁ i)) (ix (pr₂ i)) ∈ z ⟩) (sym qP)
                    (Pfill (pr₁ i) (pr₂ i) hlt)
```

It remains to build `Agrees` below the chosen index. Given a model element `j`
with `fst j ∈ # (toℕ i)`, the numeral elimination theorem says, under
propositional truncation, that `fst j` is `# m` for some `m < toℕ i`. Mapping
the local construction `step` over this result will provide one shared value
for the two graphs at that earlier position. The truncation is preserved: the
particular natural number recovered from numeral membership is never exposed
outside the proposition required by `Agrees`.

```agda
                , agrees ) ) ) ) ) )
        where
        agrees : Agrees P a₁ e₁ e₂ γ (numAt (toℕ i))
        agrees j hj = PT.map step (∈#-elim (toℕ i) (fst j) hj)
          where
```

The function `step` makes the shared-value claim precise. From a number
`m < toℕ i` and an equality identifying `fst j` with `# m`, it must return a
model element `x` whose pair with the key `fst j` belongs to both environment
graphs. The supplied value is the first family's entry at the corresponding
finite index, packaged as `ixL (pr₁ jx)`. For the first graph, `put₁ jx`
already gives the required membership at the canonical numeral key; the
equality of the two presentations of that key transports it to `fst j`.

```agda
          step : Σ[ m ∈ ℕ ] ((m < toℕ i) × (fst j ≡ # m))
               → Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                            × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
          step (m , (hm , qj)) = ixL (pr₁ jx)
            , ( subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₁ γ) ⟩)
```

For the second graph, the earlier-index hypothesis `agree` identifies
`pr₁ jx` with `pr₂ jx`. Transporting `put₂ jx` along the reverse of this
equality changes its value from `ix (pr₂ jx)` to the shared value
`ix (pr₁ jx)`; transporting the key as before then gives membership at
`fst j`. Hence both graphs contain the very same value at every position below
`i`, completing one result of `step` and therefore the `Agrees` field of
`Differs`.

```agda
                  (sym qjx) (put₁ jx)
              , subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₂ γ) ⟩) (sym qjx)
                  (subst (λ y → ⟨ pr (# (toℕ jx)) (ix y) ∈ fst (lookup e₂ γ) ⟩)
                    (sym (agree jx (subst (_< toℕ i) (sym qm) hm))) (put₂ jx)) )
            where
```

The remaining identification concerns the key of the shared entry. From
`m < toℕ i` and the fact that `i` is itself below `arity t₁`, transitivity
makes `m` a valid element `jx : Fin (arity t₁)`. Converting `jx` back to a
natural number returns `m`; the path `qm` records this round trip and will let
the graph memberships use their canonical numeral key.

```agda
            jx : Fin (arity t₁)
            jx = fromℕ' (arity t₁) m (<-trans hm (toℕ<n i))
            qm : toℕ jx ≡ m
            qm = toFromId' (arity t₁) m (<-trans hm (toℕ<n i))
            qjx : fst j ≡ # (toℕ jx)
```

The equality `qj` identifies the original model key with `# m`, while `qm`
identifies `m` with the number of `jx`. Their composite is
`qjx : fst j ≡ # (toℕ jx)`. This is the precise change of key used above to
transport both canonical graph entries to the position named by `j`; it
completes the construction of `Agrees`, and hence the forward bridge
`lex-fill`.

```agda
            qjx = qj ∙ cong #_ (sym qm)
```

The reverse bridge starts from a `Differs` record and must recover an explicit
first difference. Its recorded index `i` belongs to the arity numeral, but the
numeral-membership elimination theorem recovers the corresponding smaller
natural number only under propositional truncation. Accordingly `lex-read` returns the
propositional truncation of `Lex`: numeral elimination hides the chosen
number, and `PT.map`
performs the otherwise explicit reconstruction without removing that
truncation.

```agda
      lex-read : Differs P a₁ e₁ e₂ γ
               → ∥ Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂)) ∥₁
      lex-read (i , (u , (v , (hi , (h₁ , (h₂ , (hp , ag))))))) =
        PT.map atIndex (∈#-elim (arity t₁) (fst i)
          (subst (λ z → ⟨ fst i ∈ z ⟩) qa hi))
```

Inside the mapped construction, the hidden witness is available as a concrete
number `m`, together with `m < arity t₁` and an equation identifying the model
index with `# m`. The function `atIndex` must now produce `Lex` itself. It
chooses the corresponding finite index and will prove the two obligations of
a first difference there: strict comparison at that index and agreement at
every smaller one.

```agda
        where
        atIndex : Σ[ m ∈ ℕ ] ((m < arity t₁) × (fst i ≡ # m))
                → Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂))
        atIndex (m , (hm , qi)) = ι , (below , agrees)
          where
```

The bound on `m` gives `ι : Fin (arity t₁)`. As before, the numeral round trip
changes the equation for `# m` into
`qι : fst i ≡ # (toℕ ι)`, so the recorded membership in the first environment
can be queried at the canonical key for `ι`. The lookup lemma `at₁` then
identifies the recorded value `fst u` with the embedded first parameter
`ix (pr₁ ι)`.

```agda
          ι : Fin (arity t₁)
          ι = fromℕ' (arity t₁) m hm
          qι : fst i ≡ # (toℕ ι)
          qι = qi ∙ cong #_ (sym (toFromId' (arity t₁) m hm))
          qu : fst u ≡ ix (pr₁ ι)
```

Applying `at₂` to the second graph likewise gives
`fst v ≡ ix (pr₂ ι)`. The relation atom in `Differs` says that the ordered pair
of the recorded values belongs to the set in slot `P`; after rewriting that
set to `Ps` and the two values to their embedded parameters, the representation
law `Prep` reads the atom as the required strict comparison
`pr₁ ι ≺ₚ pr₂ ι`.

```agda
          qu = at₁ ι u (subst (λ z → ⟨ pr z (fst u) ∈ fst (lookup e₁ γ) ⟩) qι h₁)
          qv : fst v ≡ ix (pr₂ ι)
          qv = at₂ ι v (subst (λ z → ⟨ pr z (fst v) ∈ fst (lookup e₂ γ) ⟩) qι h₂)
          below : pr₁ ι ≺ₚ pr₂ ι
          below = Prep (pr₁ ι) (pr₂ ι)
```

The transports just described finish the proof named `below`. It remains to
recover agreement before `ι`. For any `j` with `toℕ j < toℕ ι`, the bounded
clause `ag` supplies, merely, one model element whose value occurs in both
environment graphs at that position. Since the desired equality of the two
embedded parameter sets is a proposition, this propositional truncation may be
eliminated directly into it.

```agda
            (subst2 (λ y z → ⟨ pr y z ∈ fst Ps ⟩) qu qv
              (subst (λ z → ⟨ pr (fst u) (fst v) ∈ z ⟩) qP hp))
          agrees : (j : Fin (arity t₁)) → toℕ j < toℕ ι → pr₁ j ≡ pr₂ j
          agrees j hj = ix-inj (pr₁ j) (pr₂ j)
            (PT.rec (setIsSet (ix (pr₁ j)) (ix (pr₂ j))) same
```

To invoke `ag`, the finite inequality is first converted by `#mono` into
membership of `# (toℕ j)` in `# (toℕ ι)`, then transported along `qι` to the
recorded bound. The resulting truncated witness has exactly the shape handled
by `same`: an element `x` together with membership of the pair
`(# (toℕ j), fst x)` in each environment graph. Thus the truncation contains
all the data needed for the equality, while none of that witness data escapes.

```agda
              (ag (numAt (toℕ j))
                (subst (λ z → ⟨ # (toℕ j) ∈ z ⟩) (sym qι) (#mono (toℕ j) (toℕ ι) hj))))
            where
            same : Σ[ x ∈ S ] ( ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₁ γ) ⟩
                              × ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
```

For a chosen shared value `x`, `at₁` identifies `fst x` with
`ix (pr₁ j)` and `at₂` identifies the same set with `ix (pr₂ j)`. Reversing
the first path and composing it with the second gives equality of the two
embedded parameters. Injectivity of `ix` then reflects that equality back to
`pr₁ j ≡ pr₂ j`, which is precisely the earlier-index condition of `Lex`.
The reverse bridge is now complete.

```agda
                 → ix (pr₁ j) ≡ ix (pr₂ j)
            same (x , (k₁ , k₂)) = sym (at₁ j x k₁) ∙ at₂ j x k₂
```

## Both halves

Under the four representation laws supplied to `Keys`, the two relation slots stand for `limitOrder` on formula codes and the given order on carrier parameters. The two halves now compare the same three keys. `order-in` sends a concrete proof of `t₁ ≺ₙ t₂` to satisfaction of `≺At`; `order-out` reads such a satisfaction only as `∥ t₁ ≺ₙ t₂ ∥₁`. The outward half retains the propositional truncation contributed by disjunction and existential satisfaction. This completes the adequacy of the comparison formula `≺At` itself, and no stronger result about the other formulas is proved here.

The remaining boundary is precise. A meta-level `Name` stores an arity, a parameter-free formula, and a parameter vector; its denotation is derived. Internally, `NameAt` adds slots for those data and the derived denotation, which it checks using the set of satisfying environments returned by `satGraphAt`. `LeastNameAt` states that no smaller name has the same denotation, but does not choose a name. The complete adequacy of `NameAt`, `LeastNameAt`, and `StepAt`, including recovery of their witnesses, belongs to `L.Choice.NameComparisonAdequacy`; the actual least-name choice remains `CanonicalNames.leastName`.

## Recap

Two path-induction lemmas now remove a type-level obstacle from the full
three-key comparison. The first, `envShift`, concerns an arity equality
`e : arity t ≡ k`. Transporting `params t` along `e`, reading its entries, and
forming their environment graph yields the same graph as reading `params t`
at its original length. When `e` is reflexivity the claim reduces immediately,
and path induction handles every equality.

```agda
    private
      envShift : (t : Name) {k : ℕ} (e : arity t ≡ k)
               → env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) e (params t))))
               ≡ env (pfam t)
      envShift t e = sym (constSubstCommSlice
```

The equation is oriented from the graph of the transported vector to the
original graph `env (pfam t)`. This orientation is useful in the final proof:
the hypothesis for the second environment identifies its slot with the
original graph, and the reverse of `envShift` then identifies that same slot
with the graph at the first name's arity, exactly the form expected by the
first-difference bridge.

```agda
        (Vec ⟪ A ⟫) (V ℓ) (λ _ v → env (λ i → ix (lookup i v))) e (params t))
```

The second lemma, `vecShift`, performs the parallel simplification for the
vector order. Comparing `p` with `q` after transporting `q` along an equality
of lengths gives the same proposition as comparing the original vectors.
Again the equality proof contributes no mathematical case: path induction
reduces it to reflexivity. Together, `envShift` and `vecShift` keep the graph
presentation and the vector comparison synchronized when the arities are
identified.

```agda
      vecShift : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i)
               → (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q)
      vecShift e p q = sym (constSubstCommSlice
        (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)
```

The final comparison is carried out at arbitrary slots of an arbitrary
environment. Two slots hold the represented relations `Rs` and `Ps`; for each
name, three more hold its formula code, arity numeral, and parameter graph.
The eight equations `qR`, `qP`, `qs₁`, `qs₂`, `qa₁`, `qa₂`, `qe₁`, and `qe₂`
pin those readings to two concrete names `t₁` and `t₂`. Under precisely these
hypotheses, the internal formula can be compared with `_≺ₙ_`.

```agda
    module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name)
             (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps)
             (qs₁ : fst (lookup s₁ γ) ≡ fst (codeOf t₁))
             (qs₂ : fst (lookup s₂ γ) ≡ fst (codeOf t₂))
             (qa₁ : fst (lookup a₁ γ) ≡ # (arity t₁))
```

The last four slot equations pin the two arities and the two environment
graphs; in particular, no chosen coordinates are built into the theorem. To
read the second and third keys, equality found between slot values must be
lifted back to equality of the dependent data carried by names. The first
helper, `codeSame`, addresses the code key: from equality of the two skeleton
slots it reconstructs an equality `codeOf t₂ ≡ codeOf t₁` in the type
`Limit`.

```agda
             (qa₂ : fst (lookup a₂ γ) ≡ # (arity t₂))
             (qe₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
             (qe₂ : fst (lookup e₂ γ) ≡ env (pfam t₂)) where
      private
        codeSame : fst (lookup s₂ γ) ≡ fst (lookup s₁ γ) → codeOf t₂ ≡ codeOf t₁
```

An element of `Limit` is an underlying set together with evidence that it
belongs to `Lset ω`. That evidence is proposition-valued, so `Σ≡Prop` says
that a path between the underlying sets determines a path between the complete
codes. The required underlying path is the composite
`sym qs₂ ∙ q ∙ qs₁`: from the second code to its slot, across the recorded
skeleton equality, and on to the first code. This explains both why the proof
component needs no separate comparison and why the resulting equality has the
orientation required by the second branch of the name order.

```agda
        codeSame q = Σ≡Prop (λ x → snd (x ∈ Lset ω)) (sym qs₂ ∙ q ∙ qs₁)
```

The reverse conversion starts with equality in `Limit`, where a code consists of
an underlying set together with its proof of membership in the limit stage.
Projecting with `fst` gives equality of the underlying code sets. Composing it
with the two slot identifications yields the orientation required by the later
branches of the formula: the second skeleton slot equals the first.

```agda
        codeBack : codeOf t₂ ≡ codeOf t₁ → fst (lookup s₂ γ) ≡ fst (lookup s₁ γ)
        codeBack ec = qs₂ ∙ cong fst ec ∙ sym qs₁
```

The parameter branch must read the second environment at the first name's
arity. Given `ek : arity t₂ ≡ arity t₁`, path induction identifies the graph of
`params t₂` with the graph obtained after transporting that vector to the new
length. Reversing this graph equality and composing it with the identification
of slot `e₂` gives exactly the transported environment expected by the
first-difference bridge.

```agda
        shiftEnv : (ek : arity t₂ ≡ arity t₁)
                 → fst (lookup e₂ γ)
                 ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) ek (params t₂))))
        shiftEnv ek = qe₂ ∙ sym (envShift t₂ ek)
```

The forward theorem now follows the three possible reasons why one name
precedes another. In the code branch, `Rfill` turns the strict comparison of
the two formula codes by the limit order into membership of their ordered pair
in `Rs`. The equations for `R`, `s₁`, and `s₂` transport that membership to the
three slots of the formula, and `≺At-in` places the resulting witness in the
first branch of `≺At`.

```agda
      order-in : t₁ ≺ₙ t₂ → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
      order-in (inl h) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inl (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩)
                (sym qR)
                (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) (sym qs₁) (sym qs₂)
```

In the arity branch, equality of codes first supplies the required equality of
the two skeleton slots through `codeBack`. The strict inequality
`arity t₁ < arity t₂` becomes membership
`# (arity t₁) ∈ # (arity t₂)` by the von Neumann numeral law `#mono`; the two
arity-slot equations then carry this membership to the formula. Thus the
second key is used only after the first key has been shown equal.

```agda
                  (Rfill (codeOf t₁) (codeOf t₂) h))))
      order-in (inr (ec , inl h)) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inr (codeBack ec , inl
          (subst2 (λ y z → ⟨ y ∈ z ⟩) (sym qa₁) (sym qa₂)
            (#mono (arity t₁) (arity t₂) h))))
```

The parameter branch begins with equal codes and equal arities. The arity path
transports the second parameter vector to the first vector's length; `vec-lex`
then turns their recursive vector comparison into an explicit first differing
index. The map `lex-fill` then turns that witness into the `Differs` payload
used to satisfy `LexAt`: it records the index, the strict comparison there,
and all earlier agreements, using `shiftEnv` to identify the transported
second graph. This constructs the third branch of `≺At` directly from the
comparison evidence, without extracting any witness from a propositional
truncation.

```agda
      order-in (inr (ec , inr (ek , hv))) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inr (codeBack ec , inr (qa₂ ∙ cong #_ ek ∙ sym qa₁
          , lex-fill P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek)
              (vec-lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂))
                (transport (sym (vecShift ek (params t₁) (params t₂))) hv)))))
```

The reverse theorem retains the propositional truncation carried by the
object-language disjunctions and existentials. Accordingly, `≺At-out` exposes
the three cases only inside a truncation, and `PT.rec` may analyze them because
the target is itself the proposition `∥ t₁ ≺ₙ t₂ ∥₁`. In the code case, the
slot equations move the recorded pair membership back to `Rs`; `Rrep` then
reads it as the strict limit-order comparison of the two genuine codes and
supplies the first branch of the naming comparison.

```agda
      order-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ t₁ ≺ₙ t₂ ∥₁
      order-out h = PT.rec squash₁ read (≺At-out R P s₁ a₁ e₁ s₂ a₂ e₂ γ h)
        where
        read : Below R P s₁ a₁ e₁ s₂ a₂ e₂ γ → ∥ t₁ ≺ₙ t₂ ∥₁
        read (inl k) = ∣ inl (Rrep (codeOf t₁) (codeOf t₂)
```

In the arity case, the formula first says that the second skeleton slot equals
the first; `codeSame` lifts this underlying equality to equality of the two
codes in `Limit`. The other premise, transported through the arity-slot
equations, is membership of the first arity numeral in the second. Numeral
elimination converts that membership into `arity t₁ < arity t₂`, so equality
at the first key and strict comparison at the second assemble the arity branch
of `_≺ₙ_`.

```agda
          (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) qs₁ qs₂
            (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩)
              qR k))) ∣₁
        read (inr (q , inl k)) = ∣ inr (codeSame q , inl
          (#∈#-elim (arity t₁) (arity t₂)
```

The parameter case must first recover a common length. The formula gives an
equality from the second arity slot to the first; composing it with the two
slot equations yields equality of the corresponding von Neumann numerals, and
`#-inj′` recovers `ek : arity t₂ ≡ arity t₁`. With this path fixing the type of
the second vector, `lex-read` interprets the `LexAt` record against the two
environment graphs. Its result is an explicit first difference `Lex` still
inside propositional truncation, exactly preserving the existential boundary
of the formula.

```agda
            (subst2 (λ y z → ⟨ y ∈ z ⟩) qa₁ qa₂ k))) ∣₁
        read (inr (q , inr (q' , dif))) = PT.map atLex
          (lex-read P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek) dif)
          where
          ek : arity t₂ ≡ arity t₁
```

Inside that truncation, `atLex` completes the third case. The induction
`lex-vec` turns the explicit first difference into the recursive vector order
against the transported second vector, and `vecShift` removes the transport
from the resulting proposition. Together with `codeSame q` and the recovered
arity path `ek`, this is the parameter branch of `_≺ₙ_`; `PT.map` keeps the
whole result truncated. Thus, under the two representation laws and the slot
identifications, `order-in` constructs satisfaction of `≺At` from a naming
comparison, while `order-out` recovers only `∥ t₁ ≺ₙ t₂ ∥₁`. This theorem is
the adequacy of the comparison formula itself; the corresponding readings of
`NameAt`, `LeastNameAt`, and `StepAt` require additional arguments.

```agda
          ek = #-inj′ (sym qa₂ ∙ q' ∙ qa₁)
          atLex : Lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) → t₁ ≺ₙ t₂
          atLex lx = inr (codeSame q , inr (ek
            , transport (vecShift ek (params t₁) (params t₂))
                (lex-vec (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) lx)))
```