---
title: "Satisfaction and the recursion value"
module: L.Coding.SatisfactionBridge
lang: en
site: "Bedrock"
description: "Satisfaction and the recursion value"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 50
canonical: https://bedrock.institute/en/L.Coding.SatisfactionBridge.html
html: L.Coding.SatisfactionBridge.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionBridge.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Coding.Environment, L.Coding.Expressions, L.Coding.EnvironmentSet, L.Coding.Satisfaction]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.SatisfactionBridge.md, https://bedrock.institute/ja/L.Coding.SatisfactionBridge.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Satisfaction and the recursion value

The recursive construction `Sat` assigns to each formula a set of coded
environments, but its recursion equations acquire their intended meaning only
after those codes are compared with genuine assignments in the structure on
the members of `B`. The decisive choice is to use that restricted structure's
inner semantics. Its quantified variables already range over `B`, while a
bounded quantifier imposes the separate requirement of membership in the value
of its bounding term.

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

The sole explicit hypothesis is excluded middle at level `ℓ-suc ℓ`. The
formula induction below does not split on propositions itself; the hypothesis
enters through the already constructed environment sets and satisfaction sets,
whose separation operations are parameterized by `lem`.

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

Fix a universe level and this classical instance. The chapter will compare two
descriptions of the same truth condition. On the coded side, an environment
belongs to the recursively defined set `Sat B φ`; on the semantic side, the
corresponding assignment satisfies `φ` in the structure whose domain consists
of the members of `B`. Constants must also name members of `B`, so that both
descriptions interpret them in that restricted structure.

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

The proof follows the syntax of formulas. There are two atomic constructors,
three propositional connectives, falsity, two unbounded quantifiers, and two
quantifiers bounded by a term. Thus the semantic comparison has ten cases.
Terms and formulas may change their constant alphabet through `mapTm` and
`mapFo`, while `mapFo-comp` says that two successive changes agree with the
change along their composite. This is how a formula over members of `B` is
placed in the ambient constant alphabet without changing its syntactic shape.

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

Relabelling is semantically exact. If constants are changed along a map `f`,
then evaluating `mapFo f φ` under an interpretation `ι` gives the same truth
value as evaluating `φ` under the composite interpretation `ι ∘ f`; this is
`⊨-map`. The chapter will use that equality when it passes between small
member indices, elements of the restricted structure, and constructible sets.
The surrounding hierarchy and its ordered-pair operation provide the sets from
which coded environments are built.

```agda
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

Three earlier constructions supply the mathematical data used by the bridge.
For a set `B`, `DefOf` gives the structure restricted to membership in `B` and
the subsets definable in that structure. Environment coding represents a
finite assignment by the graph of its values and represents extension by
prefixing one value. Finally, the environment-set construction collects all
such graphs of a fixed arity. The transitivity used here belongs to the class
`L`: it lets a member of a constructible set be regarded as constructible. It
does not assert that `B` itself is transitive.

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Environment {ℓ} using ( env; cons; lookup-spec )
open import L.Coding.Expressions {ℓ} using ( consAtL; consAtL-adequate )
open import L.Coding.EnvironmentSet {ℓ} lem
```

The coded and semantic sides already have complementary interfaces. An index
family gives the canonical graph `envS`, and `envSet-in` and `envSet-out` relate
canonical graphs to arbitrary members of `envSet`. The set `Sat B φ` is then
obtained by separating from `envSet B n` those graphs satisfying the recursive
condition `cond B φ`. The formula `tmIs` expresses a term-value relation, with
readers for its variable case, while the imported readers for atoms and
unbounded quantifiers translate those clauses in both directions. All these
statements describe `cond`; the additional requirement of belonging to
`envSet` remains a separate component of `Sat-mem`.

```agda
  using ( Ix; envS; envSet; envSet-in; envSet-out )
open import L.Coding.Satisfaction {ℓ} lem
  using ( tmIs; tmIs-var-in; tmIs-var-out; cond; Sat; Sat-mem
        ; cond∈-in; cond∈-out; cond≐-in; cond≐-out
        ; cond∃-in; cond∃-out; cond∀-in; cond∀-out
```

The remaining readers treat the two bounded quantifiers. Together with the
preceding interfaces, they expose every non-propositional clause of `cond` in
both directions. A bounded clause keeps two restrictions distinct: the new
value must belong to the carrier `B`, and it must belong to the value of the
bounding term. The later induction will match these with the domain of the
restricted structure and the bound occurring in its inner semantics.

```agda
        ; cond∃∈-in; cond∃∈-out; cond∀∈-in; cond∀∈-out )
```

The proof compares proposition-valued statements by paths. `⇔toPath` turns two
implications between propositions into such a path, after which congruence can
carry the comparison through the logical constructors. In the membership atom,
`subst2` transports the relation after both candidate term values have been
identified with their semantic values. Existential clauses and environment
recovery use propositional truncation: a truncation is eliminated only when the
target is again a proposition, so no chosen witness is extracted.

```agda
open import Cubical.Foundations.Prelude using ( subst2; funExt⁻ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
```

A hierarchy set comes with a small presentation of its members. For a proof
that `a ∈ B`, the equivalence `∈-asFiber` returns an index in `⟪ B ⟫` together
with a path from the member presented by that index to `a`. The two directions
between small presentation membership and ordinary hierarchy membership let
the proof move between these views. This presentation is crucial because an
inner assignment already contains the proofs that its entries belong to `B`,
so its index family can be obtained directly.

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
```

Finite environments use von Neumann numerals as keys. Thus a position
`i : Fin n` is recorded in its graph by the set `# (toℕ i)`. Naming the numeral
constructor here connects the finite index used by a term variable with the
set-theoretic key used by the coded environment.

```agda
open InfinitySet using ( #_ )
```

Opening the constructible universe as an `hProp`-valued structure fixes the
host carrier `S`, whose elements are sets equipped with proofs of
constructibility. It also supplies the proposition-valued membership notation
`_∈ˢ_` and the brackets `⟨_⟩` for its underlying proof type. Consequently the
equalities proved below compare truth values themselves; they are neither
equalities of hierarchy sets nor untruncated equivalences carrying extra data.

```agda
open hPropStructure 𝒮ʟ
```

The object-language conditions imported above are interpreted in the
structure carried by all constructible sets. Instantiating the general
absoluteness construction with the class `isL` gives this host satisfaction
relation, written `_⊨_`, and the fixed-length environment notation `_^_`.
Its variables range over constructible sets. This host semantics reads coded
formulas such as `cond B φ` after the membership equation for `Sat` has been
opened. It is an intermediate layer on the coded side and must be kept distinct
from the still smaller structure whose domain is the members of one particular
set `B`.

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

## The restricted structure on the carrier

Now fix `B : S`. Applying `DefOf` to its underlying hierarchy set constructs
the restricted domain `DB.SM`: an element is a set together with a proof that
it belongs to `B`. The structure `DB.𝒮M` interprets membership and equality on
that domain. Opening ordinary first-order semantics there with the identity
constant interpretation yields `_⊨ᴮ_` and `⟦_⟧ᴮ`. These are exactly the inner
satisfaction and term evaluation used in the definition of `DB.defSet`, so the
semantic endpoint of the bridge and the definable subsets share one restricted
structure.

```agda
module _ (B : S) where
  module DB = DefOf (fst B)
  module SemB = FOL.Semantics DB.𝒮M
  open SemB.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```

An element `x : DB.SM` already consists of an underlying set `fst x` and a
proof `snd x` that this set belongs to `B`. Since `B` is constructible and the
class `L` is transitive, `fst x` is constructible as well. The map `intoL`
keeps the underlying set and supplies precisely this new certificate, producing
an element of the host carrier `S`. No closure of `B` under membership is used.

```agda
  intoL : DB.SM → S
  intoL x = fst x , isL-trans {x = fst B} {y = fst x} (snd x) (snd B)
```

There is one more constant alphabet to connect. An index
`m : ⟪ fst B ⟫` presents a member of `B`; `DB.ι m` packages that member with
its membership proof as an element of `DB.SM`, and `intoL` regards the same
underlying set as an element of `S`. Their composite `asConst` is therefore
the constant map used when a formula indexed by the small presentation is read
by the host semantics. The presentation map `DB.ι` and the inclusion `intoL`
play different roles, even though their composite preserves the named set.

```agda
  asConst : ⟪ fst B ⟫ → S
  asConst m = intoL (DB.ι m)
```

## Coding an inner assignment as an environment

An inner environment `δ : DB.SM ^ n` stores, at every position, both a set and
its proof of membership in `B`. The coded environment needs only the sets.
Accordingly, `values δ` projects each entry to its first component. This
underlying family is kept explicit because both term evaluation and extension
will be compared with its finite graph.

```agda
  values : ∀ {n} → DB.SM ^ n → Fin n → V ℓ
  values δ i = fst (lookup i δ)
```

The set `graph δ` is the finite graph of this family: at position `i` it records
the ordered pair whose key is the numeral for `i` and whose value is
`values δ i`. Thus the inner vector and the hierarchy set carry the same
assignment in two forms. The following lemmas establish the precise equations
needed to pass between them.

```agda
  graph : ∀ {n} → DB.SM ^ n → V ℓ
  graph δ = env (values δ)
```

Binding a variable extends an assignment by placing a new value at its front.
On underlying families this is the operation `cons (fst x) (values δ)`, whereas
on inner vectors it is `x ∷ δ`. The lemma `cons-values` identifies the two
pointwise: both give `fst x` at the new first position and the old value at
every shifted position. This single coherence equation is reused by all four
quantifier cases.

```agda
  private
    cons-values : ∀ {n} (x : DB.SM) (δ : DB.SM ^ n)
                → cons (fst x) (values δ) ≡ values (x ∷ δ)
    cons-values x δ = funExt (λ { zero → refl ; (suc i) → refl })
```

The vector itself determines an index family for the small presentation of
`B`. At position `i`, the second component of `lookup i δ` proves that the
underlying value belongs to `B`. Applying `∈-asFiber` to that proof gives the
index `index δ i`. This construction uses the membership evidence already
stored in the vector, so it involves no propositional truncation and no choice
of a representative recovered from a coded graph.

```agda
    index : ∀ {n} (δ : DB.SM ^ n) → Ix B n
    index δ i = ∈-asFiber {a = values δ i} {b = fst B} (snd (lookup i δ)) .fst
```

The fibre equivalence returns more than the index: it also identifies the
member presented by that index with the original underlying value.
`index-eq δ i` records this path at every position. Hence the family presented
by `index δ` and the family `values δ` agree pointwise, which is the exact input
needed to compare their finite graphs.

```agda
    index-eq : ∀ {n} (δ : DB.SM ^ n) (i : Fin n)
             → ⟪ fst B ⟫↪ (index δ i) ≡ values δ i
    index-eq δ i = ∈-asFiber {a = values δ i} {b = fst B} (snd (lookup i δ)) .snd
```

Using this index family in the canonical environment constructor gives
`envFor δ`, an element of the constructible host structure. It is the canonical
hierarchy code associated with the concrete vector `δ`. The next two facts
identify its underlying graph and then prove its membership in the environment
set; no arbitrary environment representative has been selected.

```agda
  envFor : ∀ {n} → DB.SM ^ n → S
  envFor δ = envS B (index δ)
```

The underlying hierarchy set of `envFor δ` is exactly `graph δ`.
Function extensionality combines the pointwise paths `index-eq δ i` into an
equality of value families, and congruence of `env` turns that equality into
`envFor-graph`. This path of underlying sets is the interface used later. In
particular, extending `δ` to `x ∷ δ` produces a new canonical environment to
which the same theorem applies, without comparing witnesses hidden inside a
truncation.

```agda
  envFor-graph : ∀ {n} (δ : DB.SM ^ n) → fst (envFor δ) ≡ graph δ
  envFor-graph δ = cong env (funExt (index-eq δ))
```

The first consequence runs from a known vector to environment-set membership.
Suppose `z : S` has underlying set `graph δ`. The canonical environment
`envFor δ` belongs to `envSet B n` by `envSet-in`, and `envFor-graph` together
with the assumed path transports that membership to `z`. This proves
`graph-envSet`. Its direction is exactly what the later membership equation
needs when it removes the common environment requirement from `Sat B φ`.
The converse direction is different: `envSet-out` recovers an index family
only under propositional truncation. A later construction turns that family
into a vector, still under truncation, and keeps the recovery outside the
formula induction.

```agda
  graph-envSet : ∀ {n} (δ : DB.SM ^ n) (z : S)
               → fst z ≡ graph δ → ⟨ z ∈ˢ envSet B n ⟩
  graph-envSet {n} δ z q = subst (λ w → ⟨ w ∈ fst (envSet B n) ⟩)
    (envFor-graph δ ∙ sym q) (envSet-in B (index δ))
```

The graph equation now removes the common environment requirement from the
membership equation. `Sat-mem` says that membership in `Sat B φ` is the
conjunction of membership in `envSet B n` and satisfaction of `cond B φ`.
Given `fst z ≡ graph δ`, the previous lemma supplies the first conjunct, so
the second conjunct is equivalent to the whole statement. `⇔toPath` turns
the two implications into a path of truth values. Thus `Sat-cond`
does not yet interpret the formula; it isolates the recursive condition that
the following induction will interpret.

```agda
  Sat-cond : ∀ {n} (φ : Formula S n) (δ : DB.SM ^ n) (z : S)
           → fst z ≡ graph δ
           → (z ∈ˢ Sat B φ) ≡ ((z ∷ []) ⊨ cond B φ)
  Sat-cond φ δ z q =
    Sat-mem B φ z ∙ ⇔toPath snd (λ h → graph-envSet δ z q , h)
```

## Reading terms and environment extension

The first reading lemma compares the object-language term predicate with
actual term evaluation. In an ambient environment `γ`, slot `ei` contains a
coded assignment and slot `vi` contains a proposed value. If the former has
underlying set `graph δ`, then satisfaction of `tmIs (mapTm intoL t) vi ei`
forces the latter to have underlying set `fst (⟦ t ⟧ᴮ δ)`. For a constant,
the predicate is already the required equation: relabelling by `intoL`
changes only the packaged carrier, while its underlying set remains the
constant's value.

```agda
  tmIs-out : ∀ {n k} (t : Term DB.SM n) (δ : DB.SM ^ n) (γ : S ^ k) (vi ei : Fin k)
           → fst (lookup ei γ) ≡ graph δ
           → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩
           → fst (lookup vi γ) ≡ fst (⟦ t ⟧ᴮ δ)
  tmIs-out (con c) δ γ vi ei qe h = h
```

For a variable, `tmIs-var-out` reads satisfaction as membership of the
pair consisting of the numeral key and the proposed value in the graph held
at `ei`. Its existential witness is propositionally truncated, but the target
membership is a proposition, so eliminating the truncation loses nothing
needed here. Transport along `qe` replaces that graph by `graph δ`, and
`lookup-spec` identifies membership at key `i` with equality to the
`i`th value of `δ`. This functionality of the coded graph is exactly the
variable case of term evaluation.

```agda
  tmIs-out (var i) δ γ vi ei qe h =
    subst ⟨_⟩ (lookup-spec (values δ) i (fst (lookup vi γ)))
      (subst (λ w → ⟨ pr (# (toℕ i)) (fst (lookup vi γ)) ∈ w ⟩) qe
        (tmIs-var-out i γ vi ei h))
```

The converse lemma constructs the term predicate from the semantic value
equation. Its constant case is again immediate: after relabelling, the
object-language equation asks precisely for the equation supplied as the
hypothesis. Together, `tmIs-out` and `tmIs-in` make term values
available in either direction. The atomic clauses will use the pair to compare
two evaluated terms, and the bounded-quantifier clauses will use it to read
the value of their bounding term.

```agda
  tmIs-in : ∀ {n k} (t : Term DB.SM n) (δ : DB.SM ^ n) (γ : S ^ k) (vi ei : Fin k)
          → fst (lookup ei γ) ≡ graph δ
          → fst (lookup vi γ) ≡ fst (⟦ t ⟧ᴮ δ)
          → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩
  tmIs-in (con c) δ γ vi ei qe q = q
```

In the variable case, the earlier argument is reversed. `lookup-spec`
turns the assumed value equation into membership of the keyed pair in
`graph δ`; transport along the symmetric graph equation moves that membership
to the graph stored at `ei`; and `tmIs-var-in` packages it as
satisfaction of the object-language predicate. The two directions therefore
express the same functional graph fact, without choosing a representative
from any truncation.

```agda
  tmIs-in (var i) δ γ vi ei qe q = tmIs-var-in i γ vi ei
    (subst (λ w → ⟨ pr (# (toℕ i)) (fst (lookup vi γ)) ∈ w ⟩) (sym qe)
      (subst ⟨_⟩ (sym (lookup-spec (values δ) i (fst (lookup vi γ)))) q))
```

The second pair of readings concerns extension of an assignment. In
`consAtL ei mi di`, slot `di` holds the old graph, slot `mi` holds the new
leading value, and slot `ei` is proposed as the extended graph. If the first
two slots agree with `δ` and `x`, satisfaction of this predicate implies that
the underlying set at `ei` is `graph (x ∷ δ)`. This is the equation needed
when a quantified formula passes from an assignment to the assignment with
one new leading entry.

```agda
  consAtL-out : ∀ {n k} (δ : DB.SM ^ n) (x : DB.SM) (γ : S ^ k) (ei mi di : Fin k)
              → fst (lookup di γ) ≡ graph δ
              → fst (lookup mi γ) ≡ fst x
              → ⟨ γ ⊨ consAtL ei mi di ⟩
              → fst (lookup ei γ) ≡ graph (x ∷ δ)
```

The proof first applies `consAtL-adequate`. Under the old-graph
hypothesis, that path identifies the proposed extension slot with
`env (cons (fst (lookup mi γ)) (values δ))`. The equation `qm` replaces its
head by `fst x`, and `cons-values` identifies the resulting family with
the underlying values of `x ∷ δ`. Congruence of `env` then gives the announced
graph equation. In particular, the adequacy law yields an equality with the
extended graph; no graph-membership statement occurs here.

```agda
  consAtL-out δ x γ ei mi di qd qm h =
      subst ⟨_⟩ (consAtL-adequate ei mi di γ (values δ) qd) h
    ∙ cong env (cong (λ w → cons w (values δ)) qm ∙ cons-values x δ)
```

The inward reading assumes all three semantic equations: the old slot contains
`graph δ`, the new-value slot contains `fst x`, and the proposed extension
slot contains `graph (x ∷ δ)`. From them it constructs satisfaction of
`consAtL`. This direction lets each quantifier clause use the canonical
environment `envFor (x ∷ δ)` as its certified extension. No untruncated
environment has to be recovered from an existential representation.

```agda
  consAtL-in : ∀ {n k} (δ : DB.SM ^ n) (x : DB.SM) (γ : S ^ k) (ei mi di : Fin k)
             → fst (lookup di γ) ≡ graph δ
             → fst (lookup mi γ) ≡ fst x
             → fst (lookup ei γ) ≡ graph (x ∷ δ)
             → ⟨ γ ⊨ consAtL ei mi di ⟩
```

The inward proof follows the path used by the outward reading in reverse.
Starting from the equation with `graph (x ∷ δ)`, the symmetric
`cons-values` equation and the head equation rewrite its right side as the
graph built from the value at `mi` and the old family. The symmetric adequacy
path then transports this equality back to satisfaction of `consAtL`. Hence
the object-language extension predicate and concrete prefixing of an
assignment are interchangeable once the relevant slots are fixed by
equalities of underlying sets.

```agda
  consAtL-in δ x γ ei mi di qd qm q =
    subst ⟨_⟩ (sym (consAtL-adequate ei mi di γ (values δ) qd))
      (q ∙ sym (cong env (cong (λ w → cons w (values δ)) qm ∙ cons-values x δ)))
```

## Induction from recursive values to inner satisfaction

Formula induction is organized by the property `Adequate`. For every
assignment `δ` in the restricted structure, every ambient constructible
element `z`, and every equation identifying its underlying set with
`graph δ`, the property gives a path from membership in the satisfaction set
of the relabelled formula to satisfaction of the original formula under `δ`.
The quantification over `z` makes the statement independent of a chosen
representative of the graph. Its conclusion compares propositions, while
`mapFo intoL φ` on the left records the necessary change from restricted
constants to ambient constructible constants.

```agda
  Adequate : ∀ {n} → Formula DB.SM n → Type (ℓ-suc (ℓ-suc ℓ))
  Adequate {n} φ = (δ : DB.SM ^ n) (z : S) → fst z ≡ graph δ
                 → (z ∈ˢ Sat B (mapFo intoL φ)) ≡ (δ ⊨ᴮ φ)
```

Falsity is the base case and needs no induction hypothesis. After
`Sat-cond` removes the environment-set conjunct, the recursive condition
for `⊥̇` is the false proposition. The inner semantics of `⊥̇` is the same
false proposition, so the remaining comparison is definitional. Both semantics
impose the identical impossible condition.

```agda
  step⊥ : ∀ {n} → Adequate {n} ⊥̇
  step⊥ δ z q = Sat-cond ⊥̇ δ z q
```

For a conjunction, `Sat-cond` exposes the conjunction of the two
recursive subconditions. The induction hypotheses give paths from each
subcondition to the corresponding inner satisfaction proposition, at the same
assignment and the same graph representative. Applying congruence for the
truth-value conjunction `_⊓_` to both paths yields the required path for
`a ∧̇ b`. No witness management is involved because the recursive clause and
the inner semantics use the same propositional connective.

```agda
  step∧ : ∀ {n} (a b : Formula DB.SM n)
        → Adequate a → Adequate b → Adequate (a ∧̇ b)
  step∧ a b ia ib δ z q = Sat-cond (mapFo intoL (a ∧̇ b)) δ z q
    ∙ cong₂ _⊓_ (ia δ z q) (ib δ z q)
```

Disjunction has the same structure. Its recursive condition combines the two
subconditions with the truth-value disjunction `_⊔_`, and congruence carries
the two induction paths through that connective. These are operations on
propositions: the proof compares the truth of the two subformulas and the
truth of their disjunction. It does not form a union of the two satisfaction
sets.

```agda
  step∨ : ∀ {n} (a b : Formula DB.SM n)
        → Adequate a → Adequate b → Adequate (a ∨̇ b)
  step∨ a b ia ib δ z q = Sat-cond (mapFo intoL (a ∨̇ b)) δ z q
    ∙ cong₂ _⊔_ (ia δ z q) (ib δ z q)
```

Implication completes the propositional cases. The recursive clause uses the
truth-value implication `_⇒_`, so congruence applied to the two induction paths
again proves the comparison immediately. Falsity and the three binary
connectives therefore require no special semantic conversion: after the
environment component has been removed, their recursive conditions already
have the same logical form as the inner semantics.

```agda
  step⇒ : ∀ {n} (a b : Formula DB.SM n)
        → Adequate a → Adequate b → Adequate (a ⇒̇ b)
  step⇒ a b ia ib δ z q = Sat-cond (mapFo intoL (a ⇒̇ b)) δ z q
    ∙ cong₂ _⇒_ (ia δ z q) (ib δ z q)
```

Atomic formulas require the term-reading lemmas because their recursive
conditions quantify over candidate term values. For membership, the condition
gives, under propositional truncation, values `v` and `w`, proofs that they
represent the evaluations of `t` and `u`, and a membership from `fst v` to
`fst w`. The inner semantics instead states membership directly between the
actual evaluations `T` and `U`. The local names for those evaluations make the
two directions of this logical equivalence explicit.

```agda
  step∈ : ∀ {n} (t u : Term DB.SM n) → Adequate (t ∈̇ u)
  step∈ t u δ z q = Sat-cond (mapFo intoL (t ∈̇ u)) δ z q ∙ ⇔toPath fwd bwd
    where
    T = ⟦ t ⟧ᴮ δ
    U = ⟦ u ⟧ᴮ δ
```

In the forward direction, `cond∈-out` exposes the truncated candidates.
The target `fst T ∈ fst U` is a proposition, so `PT.rec` may inspect each
candidate package. At the environment `w ∷ v ∷ z ∷ []`, two applications of
`tmIs-out` identify `v` with `T` and `w` with `U`. The two-variable transport
`subst2` then carries the recorded relation `fst v ∈ fst w` to
`fst T ∈ fst U`, which is exactly the inner interpretation of the atom.

```agda
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩ → ⟨ fst T ∈ fst U ⟩
    fwd h = PT.rec (snd (fst T ∈ fst U))
      (λ { (v , (w , (ht , (hu , r)))) → subst2 (λ p s → ⟨ p ∈ s ⟩)
        (tmIs-out t δ (w ∷ v ∷ z ∷ []) (suc zero) (suc (suc zero)) q ht)
        (tmIs-out u δ (w ∷ v ∷ z ∷ []) zero (suc (suc zero)) q hu)
```

For the reverse implication, the semantic term values themselves provide the
candidates. The map `intoL` packages `T` and `U` as ambient constructible
elements without changing their underlying sets, so `intoL T` and `intoL U`
may be inserted as the two witnesses expected by `cond∈-in`. This is a
direct construction from the given evaluations, not an appeal to a choice
principle or an extraction from propositional truncation.

```agda
        r })
      (cond∈-out B (mapTm intoL t) (mapTm intoL u) z h)
    bwd : ⟨ fst T ∈ fst U ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩
    bwd r = cond∈-in B (mapTm intoL t) (mapTm intoL u) z
      ∣ intoL T , (intoL U
```

With those witnesses fixed, each call to `tmIs-in` receives `refl`
because the underlying set of `intoL T` is definitionally `fst T`, and likewise
for `U`. The assumed membership between the evaluations is therefore already
the relation required between the candidates. Inserting this complete package
into the propositional truncation finishes the reverse implication and hence
the membership atom.

```agda
      , ( tmIs-in t δ (intoL U ∷ intoL T ∷ z ∷ []) (suc zero) (suc (suc zero)) q refl
        , ( tmIs-in u δ (intoL U ∷ intoL T ∷ z ∷ []) zero (suc (suc zero)) q refl
          , r ))) ∣₁
```

The equality atom follows the same plan with equality as its candidate
relation. Under propositional truncation, the recursive condition supplies
two proposed term values, their two term readings, and a path between their
underlying sets. The inner semantics asks directly for a path
`fst T ≡ fst U`. As in the membership case, `⇔toPath` reduces adequacy to a
forward transport from candidates to evaluations and a reverse construction
using the evaluations as candidates.

```agda
  step≐ : ∀ {n} (t u : Term DB.SM n) → Adequate (t ≐ u)
  step≐ t u δ z q = Sat-cond (mapFo intoL (t ≐ u)) δ z q ∙ ⇔toPath fwd bwd
    where
    T = ⟦ t ⟧ᴮ δ
    U = ⟦ u ⟧ᴮ δ
```

The forward map may eliminate the truncation because equality in the cumulative
hierarchy is a proposition. If the term readings yield paths
`ht : fst v ≡ fst T` and `hu : fst w ≡ fst U`, while the candidate relation is
`r : fst v ≡ fst w`, then the desired path has the precise orientation
`sym ht ∙ r ∙ hu`. Thus the proof first travels from the evaluation of `t`
back to its candidate, crosses the recorded candidate equality, and then
travels forward to the evaluation of `u`.

```agda
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ≐ u)) ⟩ → fst T ≡ fst U
    fwd h = PT.rec (snd (intoL T ≈ˢ intoL U))
      (λ { (v , (w , (ht , (hu , r)))) →
          sym (tmIs-out t δ (w ∷ v ∷ z ∷ []) (suc zero) (suc (suc zero)) q ht)
        ∙ r
```

The reverse map again uses `intoL T` and `intoL U` as the ambient witnesses.
They satisfy the two term predicates by the inward term reading, and the
assumed path `fst T ≡ fst U` supplies exactly the candidate equality required
by `cond≐-in`. Membership and equality atoms therefore differ only in
the relation carried between the same two evaluated terms; their treatment of
candidate values and truncation is identical.

```agda
        ∙ tmIs-out u δ (w ∷ v ∷ z ∷ []) zero (suc (suc zero)) q hu })
      (cond≐-out B (mapTm intoL t) (mapTm intoL u) z h)
    bwd : fst T ≡ fst U → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ≐ u)) ⟩
    bwd r = cond≐-in B (mapTm intoL t) (mapTm intoL u) z
      ∣ intoL T , (intoL U
```

The two value equations passed to `tmIs-in` are again `refl`, since the
witnesses were chosen to be the evaluated terms under `intoL`. The assumed
equality then completes the tuple inserted into the truncated condition.
Both atomic leaves of the formula grammar are now adequate. The remaining
cases are quantifiers, where the essential task is to relate an
object-language extension witness to prefixing an element onto the inner
assignment.

```agda
      , ( tmIs-in t δ (intoL U ∷ intoL T ∷ z ∷ []) (suc zero) (suc (suc zero)) q refl
        , ( tmIs-in u δ (intoL U ∷ intoL T ∷ z ∷ []) zero (suc (suc zero)) q refl
          , r ))) ∣₁
```

For the unbounded existential, the object-language condition contains a
propositionally truncated package: an ambient element `x` together with a
proof that its underlying set belongs to `B`, an element `e` proposed as the
extended environment, satisfaction of the extension predicate, and membership
of `e` in the subformula's satisfaction set. The inner existential ranges over
`DB.SM`, whose elements already pair a set with its membership in `B`, and is
itself propositionally truncated. The forward direction can therefore map the
outer package to an inner existential witness without retaining a chosen
representative.

```agda
  step∃ : ∀ {n} (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∃̇ a)
  step∃ a ia δ z q = Sat-cond (mapFo intoL (∃̇ a)) δ z q ∙ ⇔toPath fwd bwd
    where
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇ a)) ⟩ → ⟨ δ ⊨ᴮ (∃̇ a) ⟩
    fwd h = PT.rec squash₁
```

Inside the truncation, the ambient witness and its proof `x∈B` form the
restricted-carrier element `(fst x , x∈B)`. This is the sole domain
restriction on an unbounded quantified variable; the additional membership in
a bounding term appears only for bounded quantifiers. `consAtL-out`
then identifies `e` with the graph of the concretely extended assignment
`(fst x , x∈B) ∷ δ`. The induction hypothesis transports the recorded
subformula membership to inner satisfaction at that assignment, and the value
together with this proof is inserted into the inner existential truncation.

```agda
      (λ { (x , (x∈B , (e , (hc , he)))) → ∣ (fst x , x∈B)
         , subst ⟨_⟩ (ia ((fst x , x∈B) ∷ δ) e
             (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ z ∷ [])
               zero (suc zero) (suc (suc zero)) q refl hc)) he ∣₁ })
      (cond∃-out B (mapFo intoL a) z h)
```

For the reverse implication of the existential case, the semantic witness is
available only inside `∃[]`. We therefore map the construction over that
propositional truncation. A witness `x` is already an element of the restricted
carrier, so its first component gives the ambient set and its second component
proves membership in `B`. The condition is witnessed by `intoL x` together with
the canonical environment `envFor (x ∷ δ)` for the extended assignment.

```agda
    bwd : ⟨ δ ⊨ᴮ (∃̇ a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇ a)) ⟩
    bwd h = cond∃-in B (mapFo intoL a) z (PT.map
      (λ { (x , ha) → intoL x , (snd x , (envFor (x ∷ δ)
         , ( consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ z ∷ [])
               zero (suc zero) (suc (suc zero)) q refl (envFor-graph (x ∷ δ))
```

The inward reading of `consAtL` certifies this environment extension from three
equalities: the old environment has graph `δ`, `intoL x` has the underlying
value of `x`, and the canonical new environment has graph `x ∷ δ`. The
induction hypothesis is then read backwards, changing semantic satisfaction of
the subformula at `x ∷ δ` into membership of the canonical environment in the
recursive subvalue. All witness construction remains under `∃[]`; no choice of
a semantic witness escapes the truncation.

```agda
           , subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ))
               (envFor-graph (x ∷ δ)))) ha ))) })
      h)
```

The universal case has a different proof shape. Inner `∀[]` is a function
which, for every `x` in the restricted carrier, proves the subformula at
`x ∷ δ`; it contains no propositional truncation. After `Sat-cond` exposes the
recursive condition, the forward implication therefore takes an arbitrary
`x` and constructs the required answer directly.

```agda
  step∀ : ∀ {n} (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∀̇ a)
  step∀ a ia δ z q = Sat-cond (mapFo intoL (∀̇ a)) δ z q ∙ ⇔toPath fwd bwd
    where
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇ a)) ⟩ → ⟨ δ ⊨ᴮ (∀̇ a) ⟩
    fwd h x = subst ⟨_⟩ (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ)))
```

To query the condition's universal clause, the proof supplies the ambient
representative `intoL x`, the carrier proof `snd x`, and the canonical extended
environment. The inward `consAtL` reading verifies that this environment really
extends the old graph by the value of `x`. The clause then yields membership in
the recursive subvalue, and the induction hypothesis carries it to inner
satisfaction. The only restriction on this unbounded variable is membership in
`B`, already stored in the package `x : DB.SM`.

```agda
      (cond∀-out B (mapFo intoL a) z h (intoL x) (envFor (x ∷ δ)) (snd x)
        (consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ z ∷ [])
          zero (suc zero) (suc (suc zero)) q refl (envFor-graph (x ∷ δ))))
    bwd : ⟨ δ ⊨ᴮ (∀̇ a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇ a)) ⟩
    bwd k = cond∀-in B (mapFo intoL a) z
```

Conversely, the condition asks for a subvalue proof for every ambient `x`
known to lie in `B` and every environment certified as its extension of `z`.
The proof packages `(fst x , x∈B)` as an element of the restricted carrier and
applies the given inner universal function. The outward `consAtL` reading
identifies the certified environment with the graph of the extended assignment;
the induction hypothesis, read backwards along that equation, then produces
the required subvalue membership. This direction is pointwise throughout and
uses no truncation.

```agda
      (λ x e x∈B hc → subst ⟨_⟩
        (sym (ia ((fst x , x∈B) ∷ δ) e
          (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ z ∷ [])
            zero (suc zero) (suc (suc zero)) q refl hc)))
        (k (fst x , x∈B)))
```

A bounded existential adds the evaluated bounding term to the unbounded
argument. Let `T = ⟦ t ⟧ᴮ δ` be its genuine value in the restricted structure.
The inner semantics now seeks, under `∃[]`, an `x : DB.SM` together with both
membership of the underlying set of `x` in the underlying set of `T` and
satisfaction of the subformula at `x ∷ δ`. Thus carrier membership and bound
membership remain distinct pieces of evidence.

```agda
  step∃∈ : ∀ {n} (t : Term DB.SM n) (a : Formula DB.SM (suc n))
         → Adequate a → Adequate (∃̇∈ t a)
  step∃∈ t a ia δ z q = Sat-cond (mapFo intoL (∃̇∈ t a)) δ z q ∙ ⇔toPath fwd bwd
    where
    T = ⟦ t ⟧ᴮ δ
```

In the forward implication, the bounded condition first supplies, under an
outer truncation, a candidate `w` satisfying the term-value predicate. Its
second truncated package supplies an ambient `x`, proofs that `x` lies in `B`
and in `w`, an extended environment `e`, and the subcondition at `e`. The outer
truncation is eliminated into the propositional semantic goal, while the inner
one is mapped to the semantic existential witness `(fst x , x∈B)`.

```agda
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇∈ t a)) ⟩ → ⟨ δ ⊨ᴮ (∃̇∈ t a) ⟩
    fwd h = PT.rec squash₁
      (λ { (w , (hw , hb)) → PT.map
        (λ { (x , ((x∈B , x∈w) , (e , (hc , he)))) → (fst x , x∈B)
           , ( subst (λ s → ⟨ fst x ∈ s ⟩)
```

The term reading `tmIs-out` identifies the underlying candidate `w` with the
underlying semantic value `T`. Transport along that path changes `x∈w` into
the bound required by the inner semantics, namely `fst x ∈ fst T`. Independently,
`consAtL-out` identifies `e` with the graph of `(fst x , x∈B) ∷ δ`, so the
induction hypothesis converts the subcondition at `e` into satisfaction at the
extended assignment. These two results form the payload of the inner `∃[]`.

```agda
                 (tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w
             , subst ⟨_⟩ (ia ((fst x , x∈B) ∷ δ) e
                 (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ w ∷ z ∷ [])
                   zero (suc zero) (suc (suc (suc zero))) q refl hc)) he ) })
        hb })
```

For the reverse implication, use the genuine value `T` itself as the
condition's candidate for the bound. Its term-value predicate follows from
`tmIs-in` with the reflexive value equation. Mapping over the semantic `∃[]`
then reduces the remaining task to repackaging each semantic witness `x`; the
condition's inner existential remains propositionally truncated.

```agda
      (cond∃∈-out B (mapTm intoL t) (mapFo intoL a) z h)
    bwd : ⟨ δ ⊨ᴮ (∃̇∈ t a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇∈ t a)) ⟩
    bwd h = cond∃∈-in B (mapTm intoL t) (mapFo intoL a) z (PT.map
      (λ { (x , (hx , ha)) → intoL T
         , ( tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl
```

The semantic witness `x : DB.SM` supplies the two restrictions separately:
`snd x` proves membership in the carrier, while `hx` proves membership in the
bound `T`. The proof keeps `hx` unchanged because the chosen candidate really
is `intoL T`. It chooses `envFor (x ∷ δ)` for the extension, certifies it with
`consAtL-in`, and reads the induction hypothesis backwards to obtain membership
in the recursive subvalue.

```agda
           , ∣ intoL x , ((snd x , hx) , (envFor (x ∷ δ)
             , ( consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ intoL T ∷ z ∷ [])
                   zero (suc zero) (suc (suc (suc zero))) q refl
                   (envFor-graph (x ∷ δ))
               , subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ))
```

This completes both directions for bounded existence. Relative to unbounded
existence, the only new mathematical work is to name the value of the bounding
term and transport one membership proof between its coded candidate and its
semantic value. Both existential packages stay under propositional truncation,
so the proof introduces no choice principle. The excluded-middle parameter is
already present in the construction of `Sat`; this adequacy step adds no new
classical assumption.

```agda
                   (envFor-graph (x ∷ δ)))) ha ))) ∣₁ ) })
      h)
```

The bounded universal is the last constructor case. With
`T = ⟦ t ⟧ᴮ δ`, its inner meaning is a function which takes every
`x : DB.SM`, then a proof `fst x ∈ fst T`, and returns satisfaction of the
subformula at `x ∷ δ`. As in the unbounded universal case, neither direction
contains an existential package, so both implications are constructed
pointwise without truncation.

```agda
  step∀∈ : ∀ {n} (t : Term DB.SM n) (a : Formula DB.SM (suc n))
         → Adequate a → Adequate (∀̇∈ t a)
  step∀∈ t a ia δ z q = Sat-cond (mapFo intoL (∀̇∈ t a)) δ z q ∙ ⇔toPath fwd bwd
    where
    T = ⟦ t ⟧ᴮ δ
```

For the forward function, take `x` and its semantic bound proof `hx`. The
condition's universal clause is instantiated with the genuine bound value
`intoL T`, whose term reading follows from `tmIs-in`, and with the ambient
representative `intoL x`. The two guards are supplied from different sources:
`snd x` records `x ∈ B`, while `hx` records `fst x ∈ fst T`. The canonical
extension is certified by `consAtL-in`, and the induction hypothesis turns the
resulting subvalue membership into inner satisfaction.

```agda
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇∈ t a)) ⟩ → ⟨ δ ⊨ᴮ (∀̇∈ t a) ⟩
    fwd h x hx = subst ⟨_⟩ (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ)))
      (cond∀∈-out B (mapTm intoL t) (mapFo intoL a) z h (intoL T)
        (tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl)
        (intoL x) (envFor (x ∷ δ)) (snd x) hx
```

For the reverse function, the condition quantifies over an arbitrary candidate
bound `w`, a proof `hw` that it reads as the term value, an ambient member `x`
with proofs `x∈B` and `x∈w`, and a certified extension `e`. The outward term
reading identifies the underlying set of `w` with `fst T`; transporting `x∈w`
along this path gives exactly the bound proof needed to apply the inner
universal function to `(fst x , x∈B)`.

```agda
        (consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ intoL T ∷ z ∷ [])
          zero (suc zero) (suc (suc (suc zero))) q refl (envFor-graph (x ∷ δ))))
    bwd : ⟨ δ ⊨ᴮ (∀̇∈ t a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇∈ t a)) ⟩
    bwd k = cond∀∈-in B (mapTm intoL t) (mapFo intoL a) z
      (λ w hw x e x∈B x∈w hc → subst ⟨_⟩
```

Applying the inner universal function gives satisfaction of the subformula at
`(fst x , x∈B) ∷ δ`. The outward `consAtL` reading identifies the certified
environment `e` with the graph of precisely that assignment. Reading the
induction path backwards therefore changes semantic satisfaction into the
subvalue membership required by the condition. This closes the bounded
universal case and completes the four quantifier arguments while preserving
the separate carrier and bound restrictions.

```agda
        (sym (ia ((fst x , x∈B) ∷ δ) e
          (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ w ∷ z ∷ [])
            zero (suc zero) (suc (suc (suc zero))) q refl hc)))
        (k (fst x , x∈B) (subst (λ s → ⟨ fst x ∈ s ⟩)
          (tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w)))
```

The individual cases now assemble into `Sat-spec` by structural recursion on
the formula. Its invariant is exact: for every assignment `δ`, every ambient
element `z`, and every path from `fst z` to `graph δ`, membership of `z` in
`Sat B (mapFo intoL φ)` is the same proposition as inner satisfaction
`δ ⊨ᴮ φ`. The first four clauses select the two atomic proofs and recursively
combine the induction paths for conjunction and disjunction.

```agda
  Sat-spec : ∀ {n} (φ : Formula DB.SM n) → Adequate φ
  Sat-spec (t ∈̇ u)  = step∈ t u
  Sat-spec (t ≐ u)  = step≐ t u
  Sat-spec (a ∧̇ b)  = step∧ a b (Sat-spec a) (Sat-spec b)
  Sat-spec (a ∨̇ b)  = step∨ a b (Sat-spec a) (Sat-spec b)
```

The recursion continues with implication and falsity, then the two unbounded
quantifiers and bounded universal quantification. A compound constructor
receives precisely the adequacy proofs of its immediate subformulas; falsity
needs none. Thus every use of the induction hypothesis is local to the
syntactic branch whose recursive condition and inner semantics are being
compared.

```agda
  Sat-spec (a ⇒̇ b)  = step⇒ a b (Sat-spec a) (Sat-spec b)
  Sat-spec ⊥̇        = step⊥
  Sat-spec (∃̇ a)    = step∃ a (Sat-spec a)
  Sat-spec (∀̇ a)    = step∀ a (Sat-spec a)
  Sat-spec (∀̇∈ t a) = step∀∈ t a (Sat-spec a)
```

The bounded existential clause closes the ten-case recursion. Consequently
`Sat-spec` proves adequacy for every formula whose constants lie in the
restricted carrier, after `mapFo intoL` places those constants in the ambient
language. This theorem gives each externally constructed value `Sat B φ` its
semantic reading. It neither constructs a uniform satisfaction table nor
proves a candidate table unique. `SatisfactionGraph` formulates the candidate
graph relation, `PinnedRecursion` proves the required keywise uniqueness, and
`UniformSatisfaction` combines existence with that uniqueness to construct a
uniform table before using `Sat-spec` to interpret its values.

```agda
  Sat-spec (∃̇∈ t a) = step∃∈ t a (Sat-spec a)
```

## Recovering an assignment from an environment

The main theorem starts from a chosen assignment. To read an arbitrary member
of an environment set, we first convert the small indices used by its coding
into elements of the restricted carrier. For `m : ⟪ fst B ⟫`, the presentation
map gives the underlying set `⟪ fst B ⟫↪ m`; the two readings of presentation
membership show that this set lies in `fst B`. Pairing the set with that proof
defines `inB m : DB.SM`.

```agda
  private
    inB : (m : ⟪ fst B ⟫) → ⟨ ⟪ fst B ⟫↪ m ∈ fst B ⟩
    inB m = ∈∈ₛ {a = ⟪ fst B ⟫↪ m} {b = fst B} .snd (∈ₛ⟪ fst B ⟫↪ m)
```

An index family `g : Ix B n` contains one small member index at each finite
position. The function `tab` turns it into an assignment in `DB.SM ^ n` by
recursion on `n`: the head is the set presented by `g zero`, equipped with
`inB (g zero)`, and the tail is obtained from the shifted family
`λ i → g (suc i)`. Thus the order of entries is preserved exactly.

```agda
    tab : ∀ {n} → Ix B n → DB.SM ^ n
    tab {zero} g = []
    tab {suc n} g = (⟪ fst B ⟫↪ (g zero) , inB (g zero)) ∷ tab (λ i → g (suc i))
```

The first compatibility equation forgets the carrier proofs from `tab g` and
recovers exactly the family of sets presented by `g`. At position zero this is
reflexive; at a successor position it follows recursively from the shifted
tail. Functional extensionality combines these pointwise equations into
`tab-values`, an equality of the complete value families.

```agda
    tab-values : ∀ {n} (g : Ix B n) → values (tab g) ≡ (λ i → ⟪ fst B ⟫↪ (g i))
    tab-values {zero} g = funExt (λ ())
    tab-values {suc n} g = funExt
      (λ { zero → refl
         ; (suc i) → funExt⁻ (tab-values (λ j → g (suc j))) i })
```

Applying the graph operation `env` to `tab-values` gives the second
compatibility equation. It identifies `graph (tab g)` with the underlying set
of the canonical coded environment `envS B g`. Hence the index presentation
used by `envSet` and the restricted-carrier assignment used by inner semantics
describe the same finite graph, even though their entries carry different
auxiliary data.

```agda
    tab-graph : ∀ {n} (g : Ix B n) → graph (tab g) ≡ fst (envS B g)
    tab-graph g = cong env (tab-values g)
```

The outward specification of `envSet` recovers from a member `z`, under
propositional truncation, an index family `g` and a path from `fst z` to the
underlying set of `envS B g`. Mapping `g` to `tab g` and composing that path
with the reverse of `tab-graph` yields an assignment `δ` with
`fst z ≡ graph δ`. The result remains under truncation: it supplies neither a
globally chosen decoding nor a uniqueness claim. This restricted interface is
also what later clause-semantics arguments use when they must reason about an
arbitrary encoded environment.

```agda
  envSet-vectors : ∀ {n} (z : S) → ⟨ z ∈ˢ envSet B n ⟩
                 → ∥ Σ[ δ ∈ DB.SM ^ n ] (fst z ≡ graph δ) ∥₁
  envSet-vectors {n} z h = PT.map
    (λ { (g , qg) → tab g , qg ∙ sym (tab-graph g) }) (envSet-out B n z h)
```

`Sat-spec` starts with a particular assignment and a graph equation.
`Sat-out` gives the corresponding statement for an arbitrary member `z` of a
satisfaction value: under `∃[]`, there is an assignment `δ` whose graph is
`fst z` and which satisfies the formula in the restricted structure. The
propositional truncation is part of the conclusion, so this theorem selects no
decoding assignment and proves no such assignment unique. It asserts only the
direction from membership in `Sat` to the existence of a satisfying
representation.

```agda
  Sat-out : ∀ {n} (φ : Formula DB.SM n) (z : S)
          → ⟨ z ∈ˢ Sat B (mapFo intoL φ) ⟩
          → ∥ (Σ[ δ ∈ DB.SM ^ n ] ((fst z ≡ graph δ) × ⟨ δ ⊨ᴮ φ ⟩)) ∥₁
  Sat-out {n} φ z h = PT.map
    (λ { (g , qg) → tab g , (qg ∙ sym (tab-graph g)
```

The last two lines complete the outward reading without strengthening the
recovered data. From the original proof of membership in `Sat`, `Sat-mem`
supplies only the component asserting that `z` belongs to the environment set;
`envSet-out` then returns an index family `g` and its graph equation under
propositional truncation. Inside `PT.map`, `tab g` is the corresponding inner
assignment, and `qg ∙ sym (tab-graph g)` identifies the underlying set of `z`
with its graph. With that equation fixed, `Sat-spec` transports the original
membership proof `h` directly to inner satisfaction. The assignment and its
satisfaction proof therefore remain inside the same truncation, with no choice
or uniqueness claim.

```agda
       , subst ⟨_⟩ (Sat-spec φ (tab g) z (qg ∙ sym (tab-graph g))) h) })
    (envSet-out B n z (subst ⟨_⟩ (Sat-mem B (mapFo intoL φ) z) h .fst))
```

## Agreement with definable subsets

To compare this recursion with definable subsets, constants must pass through
three domains. A formula `ψ` begins over the small presentation
`⟪ fst B ⟫`; `DB.ι` sends its constants into the restricted carrier, and
`intoL` then sends those carrier elements into the ambient carrier `S`. By
definition their composite is `asConst`. Functoriality of constant relabelling,
expressed by `mapFo-comp`, therefore identifies the twice-relabelled formula
`mapFo intoL (mapFo DB.ι ψ)` with the directly relabelled formula
`mapFo asConst ψ`. This is an equality of formulas and will let the semantic
bridge use the constant form expected by the recursion.

```agda
  private
    mapFo-fuse : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n)
               → mapFo intoL (mapFo DB.ι ψ) ≡ mapFo asConst ψ
    mapFo-fuse = mapFo-comp DB.ι intoL
```

The second normalization concerns the one-entry assignment used by a
definable subset. The canonical environment `envS B (λ _ → m)` is built from
the constant index family with value `m`; its underlying set is the graph of
the vector `DB.ι m ∷ []`. Both graphs have the same value family, since a
length-one family has only the index `zero`. Functional extensionality checks
that index, while the successor case is impossible, and congruence carries the
result through the graph operation. Thus this concrete environment satisfies
the graph hypothesis needed by `Sat-spec`.

```agda
    graph-single : (m : ⟪ fst B ⟫)
                 → fst (envS B (λ _ → m)) ≡ graph (DB.ι m ∷ [])
    graph-single m = cong env (funExt (λ { zero → refl ; (suc ()) }))
```

These two normalizations give the bridge in the small constant alphabet.
Suppose `z` has the same underlying set as the graph of an inner assignment
`δ`. Then membership in the recursive value for `mapFo asConst ψ` is equal to
inner satisfaction of `mapFo DB.ι ψ` at `δ`. The right-hand formula has
constants in the restricted carrier and is evaluated there with the identity
interpretation; equivalently, it is the original small formula with its
constants interpreted by `DB.ι`. The proof first uses the symmetric direction
of `mapFo-fuse` to expose the two relabellings on the left, and then applies
`Sat-spec`. This gives the small-alphabet bridge at every arity before the
one-variable specialization below.

```agda
  Sat-small-spec : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (δ : DB.SM ^ n) (z : S)
                 → fst z ≡ graph δ
                 → (z ∈ˢ Sat B (mapFo asConst ψ)) ≡ (δ ⊨ᴮ mapFo DB.ι ψ)
  Sat-small-spec ψ δ z q = cong (λ χ → z ∈ˢ Sat B χ) (sym (mapFo-fuse ψ))
    ∙ Sat-spec (mapFo DB.ι ψ) δ z q
```

Now specialize to one free variable. For a small formula `ψ` and a
presentation index `m`, `defSet-Sat` compares two propositions: the set named
by `m` belongs to the definable subset `DB.defSet ψ`, and the canonical
one-entry environment for `m` belongs to the recursive satisfaction value for
`mapFo asConst ψ`. The first path in the proof is `DB.defSet-mem`. It unfolds
the meaning of the definable subset, turning its membership proposition into
inner satisfaction of `ψ` at the assignment `DB.ι m ∷ []`, with constants
interpreted by `DB.ι`.

```agda
  defSet-Sat : (ψ : Formula ⟪ fst B ⟫ 1) (m : ⟪ fst B ⟫)
             → (⟪ fst B ⟫↪ m ∈ DB.defSet ψ)
             ≡ (envS B (λ _ → m) ∈ˢ Sat B (mapFo asConst ψ))
  defSet-Sat ψ m =
      DB.defSet-mem ψ m
```

Three more paths reach the announced recursive value. First, the symmetric
direction of `⊨-map` replaces satisfaction of `ψ` with constants interpreted
by `DB.ι` by satisfaction of the relabelled formula `mapFo DB.ι ψ` under the
identity interpretation. Second, the symmetric direction of `Sat-spec`, using
`graph-single`, turns that inner satisfaction into membership in
`Sat B (mapFo intoL (mapFo DB.ι ψ))`. Finally, congruence along `mapFo-fuse`
replaces the twice-relabelled formula by `mapFo asConst ψ`. Every link is a path
between truth values. Since the assignment and its graph are given explicitly,
neither assignment recovery nor propositional truncation is involved. The
result is the one-variable interface through which definable-power-set
constructions read the recursive satisfaction value.

```agda
    ∙ sym (⊨-map DB.𝒮M DB.ι id ψ (DB.ι m ∷ []))
    ∙ sym (Sat-spec (mapFo DB.ι ψ) (DB.ι m ∷ []) (envS B (λ _ → m))
             (graph-single m))
    ∙ cong (λ χ → envS B (λ _ → m) ∈ˢ Sat B χ) (mapFo-fuse ψ)
```

## Recap

The central result `Sat-spec` identifies membership in the recursively
constructed value with inner satisfaction for every given assignment: if
`fst z ≡ graph δ`, then membership of `z` in
`Sat B (mapFo intoL φ)` is the same proposition as `δ ⊨ᴮ φ`. When the
input is instead an arbitrary coded member, `Sat-out` produces only under
`∃[]` an assignment with the required graph and satisfaction proof; it
neither selects that assignment nor proves it unique. After constants from the
small presentation are relabelled through `DB.ι` and `intoL`,
`Sat-small-spec` gives the bridge at every arity, and `defSet-Sat` specializes
it to one free variable by identifying definable-subset membership with
membership of the canonical one-entry environment. A uniform table and the
uniqueness of candidate table values require the later pinned-recursion and
uniform-satisfaction arguments.