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.

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

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.

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.

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.

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.

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.

  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.

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

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.

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.

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.

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.

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.

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.

  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.

  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.

  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.

  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.

  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.

    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.

    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.

  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.

  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.

  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.

  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.

  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 ith value of δ. This functionality of the coded graph is exactly the variable case of term evaluation.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

    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.

        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.

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

  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.

    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.

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

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

  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.

      (λ { (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.

    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.

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

  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.

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

      (λ 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.

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

    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 ∃[].

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

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

           , ∣ 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.

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

  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.

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

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

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

  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.

  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.

  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.

  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.

    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.

    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.

    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.

  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.

  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.

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

  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.

    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.

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

  defSet-Sat : (ψ : Formula ⟪ fst B ⟫ ) (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.

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