What the recursion's value is

The previous chapter built the value and characterized it by one membership equation per constructor. That is enough to check the internal clauses against it, and it is enough for nothing else: a recursion on formulas satisfying twelve equations of its own devising is an arbitrary recursion, and an internal Def read off one would provably agree with nothing. This chapter says what the value is. For an environment over the carrier, membership in Sat B φ is satisfaction of φ in the world (B, ∈), which is exactly the notion the definable powerset is defined by.

The right-hand side is the inner semantics of the restricted structure, not the ambient reading of the relativized formula, and the difference sits exactly where the previous chapter's audit already looked. Relativization leaves a bounded quantifier alone, so it guards the bound variable once, by the bounding term. The condition guards it twice, by the carrier and by the term. The inner semantics also guards it twice, once by its own carrier and once by the clause, so it matches the condition constructor for constructor: no side condition on the bound, no transitivity of the carrier, and no Δ₀ anywhere. The relativized reading would have needed the bound contained in the carrier at every bounded quantifier, threaded through the whole induction. Reading inner also lands the theorem on the definable powerset's own notion instead of one step short of it.

One consequence of that choice is a restriction, and it is the same restriction the code chapters already ruled: the formula's constants must be members of the carrier. A constant outside the carrier has no value in the inner world, so there is nothing for the two sides to agree about. The bridge therefore reads a formula over the carrier's members and relabels it into the meta-language, which is the alphabet the definable powerset indexes by anyway.

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

open import Base.Prelude
open import Base.Truth
open import Base.Classical using ( LEM )

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.Relabelling
  using ( mapTm; mapFo; mapFo-comp; ⊨-map )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
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.Model {ℓ} using ( consAtL; consAtL-adequate )
open import L.Coding.EnvSet {ℓ} lem
  using ( Ix; envS; envSet; envSet-in; envSet-out )
open import L.Coding.Sat {ℓ} 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
        ; cond∃∈-in; cond∃∈-out; cond∀∈-in; cond∀∈-out )

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₁ )
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 )
open InfinitySet using ( #_ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

The world the definable powerset means

The carrier is an element of L, so it is a set of the hierarchy, and the definable powerset chapter takes exactly such a set. Instantiating it here is what makes the two sides speak of the same world rather than of two worlds that happen to be described alike: the restricted structure below, the satisfaction opened over it, and the defSet this chapter ends at are all the same module application, not a re-derivation.

The satisfaction is opened at the restricted carrier itself as constant domain, because the bridge quantifies over formulas whose constants are members. Two inclusions cross the layers. A member of a set of L is an element of L, since the class is transitive, which is how a member becomes a constant of the meta-language; and the definable powerset's own constant interpretation composes with it, which is how one of its formulas becomes one of ours.

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

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

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

The environment an inner assignment codes

The two sides hold an environment in two forms. The inner semantics holds a vector of members; the recursion's value holds an element of L whose underlying set is a graph. So the bridge is stated with the vector as a parameter and with the equation saying the element is that vector's graph, and everything else in the chapter is arranged so that this equation is the only thing that travels.

That is the choice that dissolves the risk this chapter was written to measure. The ambient environment set recovers only some function whose graph a member is, truncated, while the four quantifier clauses need the same function extended by one entry. Indexed by the vector instead, extension is consing on the underlying family, and consing a member onto the vector agrees with it index by index, by refl in each of the two cases. The recovery is needed exactly once, in the corollary saying every member is an environment, and it never enters the induction at all.

Three small consequences follow at once. The element for a vector is the environment set's own construction at the indices the members give, which reads the fibres off the carrier untruncated. Its graph is the vector's graph. And anything whose underlying set is a vector's graph already lies in the ambient environment set, which is why membership in the value reduces to the condition alone.

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

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

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

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

    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

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

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

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

  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)

Two readings at variable arguments

The condition reads a term's value and an environment's extension through two formulas of the model's language, and the clauses below have to read them back. Both readings are stated the way the environment set chapter's own recovery was, and for the recorded reason: an adequacy substitution has to be discharged where its arguments are variables, because at a concrete environment it drags the absoluteness bridge through normalization. So the environment vector and the three slots are parameters constrained by equations, and a clause supplies its own frame's slots at the call site, where nothing substitutes any longer.

The term reading has one case per term constructor and the meta-language decides which, so each is one line of bookkeeping. A constant's reading is the equation itself. A variable's reading is the graph's functionality, which is the lemma the environment chapter exists for.

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

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

  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 ∷ δ)
  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 δ)

  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 ⟩
  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 δ)))

The bridge

The statement, once, as a named property of a formula: at every inner environment, and at every element of L whose underlying set is that environment's graph, membership in the value is satisfaction. It is a path of truth values, not an equivalence of types and not an identity of sets. A path is the currency both sides are already stated in, so this one composes with the value's membership equation on the left and with the definable powerset's specification on the right by nothing but transitivity. A set identity is not available as the primitive, because the set on the other side is not built independently: constructing it is what the recursion does.

The twelve clauses are then one step each, and taking each as a lemma over the subformulas' properties rather than as a clause of the induction costs nothing and lets each be measured on its own. The propositional five are congruences: the condition names the subvalues as constants, and the object language's connective is the truth algebra's, so there is no translation layer to cross.

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

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

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

  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)

  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)

  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)

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

The atoms

An atom's condition binds the two values and then relates them, so reading it back is the term reading twice and a transport. The other direction has to produce the two witnesses, and it produces the term's own value carried across the class inclusion, which is why its two term obligations are refl: the witness was chosen to have the value the reading asks for.

  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 ⟧ᴮ δ
    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)
        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
      , ( 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 ))) ∣₁

  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 ⟧ᴮ δ
    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
        ∙ 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
      , ( 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 two unbounded quantifiers

Here is where the two sides could have failed to meet, and where they meet for free. The condition draws its witness from the carrier and asserts that the subvalue holds at the extended environment; the inner semantics quantifies over the restricted carrier, whose elements are exactly a member paired with its membership. So each direction repackages one pair and applies the extension reading, and the environment the subformula is evaluated in is the one this chapter built for the extended vector. Nothing is truncated that was not already, and no arity carries a side condition.

  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₁
      (λ { (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)
    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 ∷ δ))
           , subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ))
               (envFor-graph (x ∷ δ)))) ha ))) })
      h)

  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 ∷ δ)))
      (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
      (λ 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)))

The two bounded quantifiers

These two are the reason the right-hand side is the inner semantics. The condition binds the bounding term's value and then guards the bound variable twice, by the carrier and by that value. The inner semantics guards it twice as well, and for the same two reasons, so the guards line up one for one and the clause is the unbounded one plus a term reading. Against the relativized reading there would be one guard on the left and two on the right, and closing that gap needs the bound contained in the carrier: a hypothesis at every bounded quantifier, at every arity, all the way down.

  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 ⟧ᴮ δ
    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 ⟩)
                 (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 })
      (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
           , ∣ 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 ∷ δ))
                   (envFor-graph (x ∷ δ)))) ha ))) ∣₁ ) })
      h)

  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 ⟧ᴮ δ
    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
        (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 ⟨_⟩
        (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 induction

Twelve steps, one line each, and the recursion is the formula's own.

  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)
  Sat-spec (a ⇒̇ b)  = step⇒ a b (Sat-spec a) (Sat-spec b)
  Sat-spec (¬̇ a)    = step¬ a (Sat-spec a)
  Sat-spec ⊤̇        = step⊤
  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)
  Sat-spec (∃̇∈ t a) = step∃∈ t a (Sat-spec a)

And every member is one

The bridge above reads membership at an environment named in advance. The other half of "is the set of the environments satisfying it" is that a member is nothing else: the value sits inside the ambient environment set, so any member is the graph of some function into the carrier's members, and turning that function into a vector puts it back in the bridge's hands. The recovery is truncated and stays so, which costs nothing here because the conclusion is an existence statement anyway.

The vector is built by a recursion of two lines rather than by the library's conversion between finite functions and vectors. That is a measurement, not a preference: the library's round-trip identity walled the chapter at over eight minutes, and the same statement written by hand costs no measurable time.

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

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

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

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

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

Against the definable powerset

And the statement the goal exists for. A subset definable in the world (B, ∈) by a formula with parameters from B collects exactly the members whose one-entry environment lies in the recursion's value at the same formula, relabelled into the meta-language. The proof is the three-step chain the definable powerset chapter already runs for absoluteness, with this chapter's bridge in the place absoluteness held: the specification of defSet, then the relabelling, which moves meaning not at all, then the bridge.

Two pieces of bookkeeping, both syntactic. Relabelling twice in a row is relabelling along the composite, which the relabelling chapter proves once for every domain; and the one-entry environment named by a member is the graph of the one-entry vector, which is the same equation at length one.

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

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

  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
    ∙ sym (⊨-map (hPropAlgebra (ℓ-suc ℓ)) 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

Sat-spec is the adequacy the recursion was missing: at every environment over the carrier, membership in the value is satisfaction in the world (B, ∈), as a path of truth values, and Sat-out adds that a member is nothing else. defSet-Sat spends both on the definable powerset, which is why the statement was owed: an internal definable powerset read off this recursion now has something it provably agrees with.

Three measurements are worth keeping. The registered risk, the coherence between the truncated recovery of an environment and the extension four clauses perform, did not fire, and the reason is a change of statement: indexing the bridge by the inner environment vector makes extension consing on the underlying family, so the coherence is two refl branches under one funExt, shared by all four quantifier clauses and paid at no arity. The recovery is confined to the corollary. The whole chapter, twelve steps and both corollaries, checks in about two seconds. And the one wall this chapter met came from neither the recursion nor the model: converting a finite function into a vector through the library's round-trip identity ran past eight minutes, while the same two statements written as a two-line recursion cost nothing at all.

What the bridge does not say, and which goal owes it: it is stated for formulas whose constants are members of the carrier, so it does not compare the value at a formula naming an arbitrary element of L. That is not a gap in the proof but the shape of the statement, because a constant outside the carrier has no value in the inner world; reading such a formula requires the ambient relativized semantics instead, where the two bounded-quantifier clauses acquire the hypothesis that the bound lies inside the carrier. No consumer wants that reading today.