The definable powerset, at a carrier that is a slot

This is the step the whole route exists for. Every chapter before it built a piece of the machine at a carrier the caller holds: a set of L, named in a formula as a constant. The internal hierarchy cannot hold its stage that way. Its graph binds the stage, because a graph may not name the object it defines, and a set enters a formula only by being named. So the description of the definable powerset has to be speakable under that binder, with the carrier occupying a slot of the ambient environment and nothing else.

What the description says is what the operator is. u is the definable powerset of the carrier when its members are exactly the sets carved out of the carrier by a formula: there merely is a code c over the carrier and a value v, the value is what the satisfaction recursion records at that code, and u's member is the set of members of the carrier whose one-entry environment lies in v. Three conjuncts, and each is a chapter already delivered, read at a slot rather than at a constant.

One shape correction is forced and it is worth stating before the formula appears. The code and the value are bound by adjacent existentials, with no conjunct between them. Nested through an intervening conjunct the two hypotheses land at different environments, and the route would acquire a weakening lemma it otherwise never needs: the same formula, the same conjunct count, the same depth, and a lemma's worth of difference.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.Relabelling using ( mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Axioms.Basic {ℓ} using ( 𝒟ₒ→isL; 𝒟ₒS; LsetS )
open import L.Coding.Model {ℓ}
  using ( extAt; extAt-out; extAt-in; extAt-in-both; tagAtL; tagAtL-adequate
        ; domAt; domAt-intro; domAt-out )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.Recover {ℓ} using ( keyOf; keyOf-fst )
open import L.Coding.CodeSet {ℓ} lem
  using ( keyArityAtL; keyArityAtL-in; keyArityAtL-out; hasWitnessAt
        ; codeS; keyS; witnessAt-in; witnessAt-out )
open import L.Coding.Graph {ℓ} lem
  using ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out )
open import L.Coding.Table {ℓ} lem
  using ( keyʟ; slot; satTable; total; inSlot; entry-in )
open import L.Coding.Slot {ℓ} lem using ( slotClosed )
open import L.Coding.Sound {ℓ} lem using ( soundness )
open import L.Coding.Unique {ℓ} lem using ( module Good )
open import L.Coding.Sat {ℓ} lem using ( Sat )
open import L.Coding.Bridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.Uniform {ℓ} lem using ( keyBridge )

open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.Data.Sigma using ( Σ≡Prop )
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; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber; _⊆_; extensionality )
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 renaming ( _⊨ᵐ_ to _⊨_ )

The environment with one entry

Definability at arity one asks whether a formula holds of a single member, and the satisfaction recursion answers at environments, so the two are joined by the environment that assigns that member to the only variable there is. An environment is its graph, and a graph of length one is a single pair: the numeral zero with the value.

That makes the reader one line. "The set at this slot has exactly the pairs (0, y) as members" is extAt applied to the tag reader, and the tag reader already delivers the equation between underlying sets, so nothing has to be proved about pairs here at all.

Its two directions are hand-written over the one-element index type, and that is a measurement rather than a taste. Reading a membership in a one-entry set back is a two-case split, one case impossible; through a library round trip between finite functions and vectors the same statement walled a chapter at over eight minutes, and the chapter that met it wrote its two clauses by hand instead. This one does the same.

envOne : V ℓ → V ℓ
envOne y = env {} (λ _ → y)

envOneAt : ∀ {n} → Fin n → Fin n → Formula S n
envOneAt e y = extAt e (tagAtL zero  (suc y))

module _ {n : ℕ} (e y : Fin n) (γ : S ^ n) where
  private
    E : S
    E = lookup e γ

    v : V ℓ
    v = fst (lookup y γ)

    readEntry : (z : S) → ⟨ fst z ∈ envOne v ⟩ → fst z ≡ pr (# ) v
    readEntry z = PT.rec (setIsSet (fst z) (pr (# ) v))
      (λ { (lift zero , q) → sym q ; (lift (suc ()) , _) })

    entry∈ : (z : S) → fst z ≡ pr (# ) v → ⟨ fst z ∈ envOne v ⟩
    entry∈ z q = ∣ lift zero , sym q ∣₁

  envOneAt-in : fst E ≡ envOne v → ⟨ γ ⊨ envOneAt e y ⟩
  envOneAt-in q = extAt-in-both e (tagAtL zero  (suc y)) γ fwd bwd
    where
    fwd : (z : S) → ⟨ fst z ∈ fst E ⟩ → ⟨ (z ∷ γ) ⊨ tagAtL zero  (suc y) ⟩
    fwd z z∈ = subst ⟨_⟩ (sym (tagAtL-adequate zero  (suc y) (z ∷ γ)))
      (readEntry z (subst (λ w → ⟨ fst z ∈ w ⟩) q z∈))

    bwd : (z : S) → ⟨ (z ∷ γ) ⊨ tagAtL zero  (suc y) ⟩ → ⟨ fst z ∈ fst E ⟩
    bwd z h = subst (λ w → ⟨ fst z ∈ w ⟩) (sym q)
      (entry∈ z (subst ⟨_⟩ (tagAtL-adequate zero  (suc y) (z ∷ γ)) h))

  envOneAt-out : ⟨ γ ⊨ envOneAt e y ⟩ → fst E ≡ envOne v
  envOneAt-out h = extensionality (fst E) (envOne v) (sub₁ , sub₂)
    where
    sub₁ : ⟨ fst E ⊆ envOne v ⟩
    sub₁ w w∈ₛ = ∈∈ₛ {a = w} {b = envOne v} .fst
      (entry∈ wS (subst ⟨_⟩
        (tagAtL-adequate zero  (suc y) (wS ∷ γ))
        (extAt-out e (tagAtL zero  (suc y)) γ h wS w∈)))
      where
      w∈ : ⟨ w ∈ fst E ⟩
      w∈ = ∈∈ₛ {a = w} {b = fst E} .snd w∈ₛ

      wS : S
      wS = w , isL-trans {x = fst E} {y = w} w∈ (snd E)

    sub₂ : ⟨ envOne v ⊆ fst E ⟩
    sub₂ w w∈ₛ = ∈∈ₛ {a = w} {b = fst E} .fst
      (PT.rec (snd (w ∈ fst E))
        (λ { (lift zero , q) →
               subst (λ u → ⟨ u ∈ fst E ⟩) (keyOf-fst  (lookup y γ) ∙ q) hasKey
           ; (lift (suc ()) , _) })
        (∈∈ₛ {a = w} {b = envOne v} .snd w∈ₛ))
      where
      hasKey : ⟨ fst (keyOf  (lookup y γ)) ∈ fst E ⟩
      hasKey = extAt-in e (tagAtL zero  (suc y)) γ h (keyOf  (lookup y γ))
        (subst ⟨_⟩
          (sym (tagAtL-adequate zero  (suc y) (keyOf  (lookup y γ) ∷ γ)))
          (keyOf-fst  (lookup y γ)))

What it is for a value to be what a code defines

The third conjunct, alone, at three slots: the member, the carrier and the value the satisfaction recursion recorded. It says that the member is the set of those members of the carrier whose one-entry environment lies in that value, which is the definable subset spelled out with the recursion in the place of satisfaction.

The condition is a conjunction rather than one clause because the carrier's bound is not implied by the rest. A member of the recursion's value is an environment, not a set of the carrier, so the second half alone would say nothing about where the member came from; the definable subset is cut out of the carrier and the formula has to say so.

Its two directions are extAt's own two, and the existential inside the condition is read by the previous section. Nothing here inspects the value, which is why this section knows nothing about codes.

DefinesAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
DefinesAt x w v = extAt x ( (var zero ∈̇ var (suc w))
                          ∧̇ ∃̇ ( envOneAt zero (suc zero)
                               ∧̇ (var zero ∈̇ var (suc (suc v))) ) )

module _ {n : ℕ} (x w v : Fin n) (γ : S ^ n) where
  private
    inner : Formula S (suc n)
    inner = ∃̇ (envOneAt zero (suc zero) ∧̇ (var zero ∈̇ var (suc (suc v))))

    body : Formula S (suc n)
    body = (var zero ∈̇ var (suc w)) ∧̇ inner

    Holds : S → Type (ℓ-suc ℓ)
    Holds z = ⟨ fst z ∈ fst (lookup w γ) ⟩
              × ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩

    readInner : (z : S) → ⟨ (z ∷ γ) ⊨ inner ⟩
              → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
    readInner z = PT.rec (snd (envOne (fst z) ∈ fst (lookup v γ))) step
      where
      step : Σ[ E ∈ S ] ⟨ (E ∷ z ∷ γ)
               ⊨ (envOneAt zero (suc zero) ∧̇ (var zero ∈̇ var (suc (suc v)))) ⟩
           → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
      step (E , (hE , E∈)) = subst (λ u → ⟨ u ∈ fst (lookup v γ) ⟩)
        (envOneAt-out zero (suc zero) (E ∷ z ∷ γ) hE) E∈

    fillInner : (z : S) → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
              → ⟨ (z ∷ γ) ⊨ inner ⟩
    fillInner z h =
      ∣ E , (envOneAt-in zero (suc zero) (E ∷ z ∷ γ) refl , h) ∣₁
      where
      E : S
      E = envOne (fst z)
        , isL-trans {x = fst (lookup v γ)} {y = envOne (fst z)} h
            (snd (lookup v γ))

  DefinesAt-out : ⟨ γ ⊨ DefinesAt x w v ⟩
                → (z : S) → ⟨ fst z ∈ fst (lookup x γ) ⟩ → Holds z
  DefinesAt-out h z z∈ = hz .fst , readInner z (hz .snd)
    where
    hz : ⟨ (z ∷ γ) ⊨ body ⟩
    hz = extAt-out x body γ h z z∈

  DefinesAt-in : ⟨ γ ⊨ DefinesAt x w v ⟩
               → (z : S) → Holds z → ⟨ fst z ∈ fst (lookup x γ) ⟩
  DefinesAt-in h z (hw , hv) =
    extAt-in x body γ h z (hw , fillInner z hv)

  DefinesAt-both : ((z : S) → ⟨ fst z ∈ fst (lookup x γ) ⟩ → Holds z)
                 → ((z : S) → Holds z → ⟨ fst z ∈ fst (lookup x γ) ⟩)
                 → ⟨ γ ⊨ DefinesAt x w v ⟩
  DefinesAt-both f g = extAt-in-both x body γ
    (λ z z∈ → f z z∈ .fst , fillInner z (f z z∈ .snd))
    (λ z h → g z (h .fst , readInner z (h .snd)))

Is a code over the carrier at that slot

Two conjuncts, both already proved, and this is only where they meet: the argument is a key at arity one, and it has a closed, shaped witness at the carrier the slot holds. The first is what tells the decode which arity to answer at; the second is what the decode runs on. Neither names a set, so the pair can be spoken under any binder.

The pinned predicate of the code-set chapter is this same pair with one binder on top, and that binder is the only thing separating a predicate a stage can hold from a predicate a bound variable can carry.

isCodeAt : ∀ {n} → Fin n → Fin n → Formula S n
isCodeAt c w = keyArityAtL c  ∧̇ hasWitnessAt w c

module _ (A : S) where
  codeAt-in : ∀ {n} (c w : Fin n) (γ : S ^ n)
            → fst (lookup w γ) ≡ fst A
            → (ψ : Formula ⟪ fst A ⟫ ) → fst (lookup c γ) ≡ fst (keyS A ψ)
            → ⟨ γ ⊨ isCodeAt c w ⟩
  codeAt-in c w γ qw ψ qc =
    keyArityAtL-in c  γ (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc

  codeAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n)
             → fst (lookup w γ) ≡ fst A
             → ⟨ γ ⊨ isCodeAt c w ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ]
                   (fst (lookup c γ) ≡ fst (keyS A ψ))) ∥₁
  codeAt-out c w γ qw (hk , hw) =
    PT.rec squash₁ step (keyArityAtL-out c  γ hk)
    where
    step : Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# ) (fst z))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ]
               (fst (lookup c γ) ≡ fst (keyS A ψ))) ∥₁
    step (z , qz) = witnessAt-out A w c γ qw hw  z qz

The graph, at a carrier that is a slot

The satisfaction recursion's graph was generalized to take its carrier as a slot, and its two halves are the existence and uniqueness the recursion was built from, restated at that slot and at a variable environment. Nothing is proved here that was not proved then: existence hands over the subformula slot, the table over it, and the twelve clauses, all three of which take the ambient environment as an argument already; uniqueness reads the graph's own bound index set and table back and applies the pinning theorem at the carrier the graph bound.

Both are stated with the code and the value reached by equations rather than named, which is the law the value theorems were written under: naming a key puts its construction inside a satisfaction, and the same statement then costs minutes instead of seconds.

module _ (B : S) where
  private
    Ci Ti : ∀ {k} → Fin (suc (suc (suc k)))
    Ci = suc (suc zero)
    Ti = suc zero

  graphAt-holds : ∀ {m n} (φ : Formula S m) (w c v : Fin n) (γ : S ^ n)
                → fst (lookup w γ) ≡ fst B
                → fst (lookup c γ) ≡ fst (keyʟ φ)
                → fst (lookup v γ) ≡ fst (Sat B φ)
                → ⟨ γ ⊨ satGraphAt w c v ⟩
  graphAt-holds φ w c v γ qw qc qv = graphAt-in w c v γ
    ∣ slot B φ , (satTable B φ , (B , (sym qw
    , ( slotClosed B φ γ
    , ( hdom
    , ( entry
    , soundness B φ γ )))))) ∣₁
    where
    δ : S ^ (suc (suc (suc _)))
    δ = B ∷ satTable B φ ∷ slot B φ ∷ γ

    hdom : ⟨ δ ⊨ domAt Ti Ci ⟩
    hdom = domAt-intro Ti Ci δ
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot B φ)))
                  (λ { (u , hu) → inSlot B φ (fst z) (fst u) hu }) h)
           , (λ h → total B φ (fst z) h))

    entry : ⟨ pr (fst (lookup c γ)) (fst (lookup v γ)) ∈ fst (satTable B φ) ⟩
    entry = subst2 (λ a b → ⟨ pr a b ∈ fst (satTable B φ) ⟩)
      (sym qc) (sym qv) (entry-in B φ)

  graphAt-unique : ∀ {m n} (φ : Formula S m) (w c v : Fin n) (γ : S ^ n)
                 → fst (lookup w γ) ≡ fst B
                 → fst (lookup c γ) ≡ fst (keyʟ φ)
                 → ⟨ γ ⊨ satGraphAt w c v ⟩
                 → fst (lookup v γ) ≡ fst (Sat B φ)
  graphAt-unique φ w c v γ qw qc h =
    PT.rec (setIsSet (fst (lookup v γ)) (fst (Sat B φ))) step
      (graphAt-out w c v γ h)
    where
    step : GraphWitAt w c v γ → fst (lookup v γ) ≡ fst (Sat B φ)
    step (C , (T , (b , (eb , (hc , (hd , (ha , h12)))))))
      = Good.pinned (b ∷ T ∷ C ∷ γ) Ci Ti zero hc hd h12 φ
          (lookup c γ) (lookup v γ) qc
          (domAt-out Ti Ci (b ∷ T ∷ C ∷ γ) hd (lookup c γ) (lookup v γ) ha) ha
      ∙ cong (λ u → fst (Sat u φ)) (Σ≡Prop (λ u → snd (isL u)) (eb ∙ qw))

The description, and the side condition it travels with

The three conjuncts, under two adjacent existentials, under one extension: u is the set of exactly those x for which there merely are a code c over the carrier and a value v such that the recursion records v at c and x is what v defines. That is the definable powerset, said in the object language, with the carrier at a slot throughout.

The side condition is about what an object-language quantifier can reach. Every existential in the description ranges over L, so the set the description picks out can only contain constructible sets. If some definable subset of the carrier were not constructible, the description would still be satisfied, by the set of the constructible ones, and it would then hold of something that is not the definable powerset. DefOK is exactly the absence of that gap.

A carrier the caller holds needs no such condition stated, because a caller that holds the carrier holds the theorem about it too. A carrier at a slot is whatever the ambient environment puts there, and no theorem about it is available under the binder, so the fact has to travel as a hypothesis and be discharged where the slot is filled. It is a hypothesis of the elimination only: the introduction is given that u is the definable powerset, and u is an element of L, so its members are constructible already and the condition it would have needed is implied by its own hypothesis.

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

DefBody : ∀ {n} → Fin n → Formula S (suc (suc (suc n)))
DefBody w = isCodeAt (suc zero) (sh3 w)
            ∧̇ ( satGraphAt (sh3 w) (suc zero) zero
              ∧̇ DefinesAt (suc (suc zero)) (sh3 w) zero )

DefAt : ∀ {n} → Fin n → Fin n → Formula S n
DefAt u w = extAt u (∃̇ (∃̇ (DefBody w)))

DefOK : S → Type (ℓ-suc ℓ)
DefOK A = (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (fst A) ⟩ → ⟨ isL x ⟩

One formula, both ways

The two halves of the description at a single formula, which is what the adequacy is assembled from. Supplying the three conjuncts for a formula ψ is supplying its key for the code and the recursion's value for the value; reading them back is decoding the code to a formula, pinning the value to the recursion's own, and then reading the third conjunct as a set identity.

Everything here is stated at a variable carrier reached by an equation, and that is what keeps the stage out of the proof. The instantiation at a stage is an equation the caller supplies, and neither Lset nor an ordinal appears anywhere below.

module _ (A : S) where
  private
    module DA = DefOf (fst A)

    toS : Formula ⟪ fst A ⟫  → Formula S 
    toS ψ = mapFo (asConst A) ψ

    ιA : ⟪ fst A ⟫ → V ℓ
    ιA = ⟪ fst A ⟫↪

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

    Fibre : Formula ⟪ fst A ⟫  → V ℓ → Type (ℓ-suc ℓ)
    Fibre ψ y = Σ[ p ∈ Σ[ m ∈ ⟪ fst A ⟫ ] ⟨ DA.smallSat ψ m ⟩ ]
                  (ιA (p .fst) ≡ y)

    inSat : (ψ : Formula ⟪ fst A ⟫ ) (m : ⟪ fst A ⟫)
          → ⟨ ιA m ∈ DA.defSet ψ ⟩
          → ⟨ envOne (ιA m) ∈ fst (Sat A (toS ψ)) ⟩
    inSat ψ m h = subst ⟨_⟩ (defSet-Sat A ψ m) h

    outSat : (ψ : Formula ⟪ fst A ⟫ ) (m : ⟪ fst A ⟫)
           → ⟨ envOne (ιA m) ∈ fst (Sat A (toS ψ)) ⟩
           → ⟨ ιA m ∈ DA.defSet ψ ⟩
    outSat ψ m h = subst ⟨_⟩ (sym (defSet-Sat A ψ m)) h

  fill : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z : S) (ψ : Formula ⟪ fst A ⟫ ) → DA.defSet ψ ≡ fst z
       → ⟨ (Sat A (toS ψ) ∷ keyS A ψ ∷ z ∷ γ) ⊨ DefBody w ⟩
  fill {n} w γ qw z ψ qz = hcode , (hgraph , hdef)
    where
    δ : S ^ (suc (suc (suc n)))
    δ = Sat A (toS ψ) ∷ keyS A ψ ∷ z ∷ γ

    hcode : ⟨ δ ⊨ isCodeAt (suc zero) (sh3 w) ⟩
    hcode = codeAt-in A (suc zero) (sh3 w) δ qw ψ refl

    hgraph : ⟨ δ ⊨ satGraphAt (sh3 w) (suc zero) zero ⟩
    hgraph = graphAt-holds A (toS ψ) (sh3 w) (suc zero) zero δ qw
               (keyBridge A ψ) refl

    Holds : S → Type (ℓ-suc ℓ)
    Holds y = ⟨ fst y ∈ fst (lookup w γ) ⟩
              × ⟨ envOne (fst y) ∈ fst (Sat A (toS ψ)) ⟩

    into : (y : S) → ⟨ fst y ∈ fst z ⟩ → Holds y
    into y y∈ = PT.rec
      (isProp× (snd (fst y ∈ fst (lookup w γ)))
               (snd (envOne (fst y) ∈ fst (Sat A (toS ψ)))))
      step (subst (λ X → ⟨ fst y ∈ X ⟩) (sym qz) y∈)
      where
      step : Fibre ψ (fst y) → Holds y
      step ((m , hm) , qm) =
          subst (λ u → ⟨ u ∈ fst (lookup w γ) ⟩) qm
            (subst (λ X → ⟨ ιA m ∈ X ⟩) (sym qw) (ιA∈ m))
        , subst (λ u → ⟨ envOne u ∈ fst (Sat A (toS ψ)) ⟩) qm
            (inSat ψ m ∣ (m , hm) , refl ∣₁)

    back : (y : S) → Holds y → ⟨ fst y ∈ fst z ⟩
    back y (yw , ys) = subst (λ X → ⟨ fst y ∈ X ⟩) qz
      (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
        (outSat ψ (fib .fst)
          (subst (λ u → ⟨ envOne u ∈ fst (Sat A (toS ψ)) ⟩)
            (sym (fib .snd)) ys)))
      where
      fib : Σ[ m ∈ ⟪ fst A ⟫ ] (ιA m ≡ fst y)
      fib = ∈-asFiber {a = fst y} {b = fst A}
        (subst (λ X → ⟨ fst y ∈ X ⟩) qw yw)

    hdef : ⟨ δ ⊨ DefinesAt (suc (suc zero)) (sh3 w) zero ⟩
    hdef = DefinesAt-both (suc (suc zero)) (sh3 w) zero δ into back

  read : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z c v : S) → ⟨ (v ∷ c ∷ z ∷ γ) ⊨ DefBody w ⟩
       → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (DA.defSet ψ ≡ fst z)) ∥₁
  read {n} w γ qw z c v (hcode , (hgraph , hdef)) =
    PT.rec squash₁ step (codeAt-out A (suc zero) (sh3 w) δ qw hcode)
    where
    δ : S ^ (suc (suc (suc n)))
    δ = v ∷ c ∷ z ∷ γ

    step : Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (fst c ≡ fst (keyS A ψ))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (DA.defSet ψ ≡ fst z)) ∥₁
    step (ψ , qc) = ∣ ψ , extensionality (DA.defSet ψ) (fst z) (sub₁ , sub₂) ∣₁
      where
      qv : fst v ≡ fst (Sat A (toS ψ))
      qv = graphAt-unique A (toS ψ) (sh3 w) (suc zero) zero δ qw
             (qc ∙ keyBridge A ψ) hgraph

      sub₁ : ⟨ DA.defSet ψ ⊆ fst z ⟩
      sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = fst z} .fst
        (PT.rec (snd (y ∈ fst z)) place
          (∈∈ₛ {a = y} {b = DA.defSet ψ} .snd y∈ₛ))
        where
        place : Fibre ψ y → ⟨ y ∈ fst z ⟩
        place ((m , hm) , qm) =
          DefinesAt-in (suc (suc zero)) (sh3 w) zero δ hdef
            (y , isL-trans {x = fst A} {y = y}
                   (subst (λ u → ⟨ u ∈ fst A ⟩) qm (ιA∈ m)) (snd A))
            ( subst (λ X → ⟨ y ∈ X ⟩) (sym qw)
                (subst (λ u → ⟨ u ∈ fst A ⟩) qm (ιA∈ m))
            , subst (λ X → ⟨ envOne y ∈ X ⟩) (sym qv)
                (subst (λ u → ⟨ envOne u ∈ fst (Sat A (toS ψ)) ⟩) qm
                  (inSat ψ m ∣ (m , hm) , refl ∣₁)) )

      sub₂ : ⟨ fst z ⊆ DA.defSet ψ ⟩
      sub₂ y y∈ₛ = ∈∈ₛ {a = y} {b = DA.defSet ψ} .fst
        (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
          (outSat ψ (fib .fst)
            (subst (λ u → ⟨ envOne u ∈ fst (Sat A (toS ψ)) ⟩) (sym (fib .snd))
              (subst (λ X → ⟨ envOne y ∈ X ⟩) qv (cond .snd)))))
        where
        y∈ : ⟨ y ∈ fst z ⟩
        y∈ = ∈∈ₛ {a = y} {b = fst z} .snd y∈ₛ

        yS : S
        yS = y , isL-trans {x = fst z} {y = y} y∈ (snd z)

        cond : ⟨ y ∈ fst (lookup w γ) ⟩ × ⟨ envOne y ∈ fst v ⟩
        cond = DefinesAt-out (suc (suc zero)) (sh3 w) zero δ hdef yS y∈

        fib : Σ[ m ∈ ⟪ fst A ⟫ ] (ιA m ≡ y)
        fib = ∈-asFiber {a = y} {b = fst A}
          (subst (λ X → ⟨ y ∈ X ⟩) qw (cond .fst))

Both readings of the description

Assembling and describing are the per-member halves, and the two readings are those under extAt's own two directions. The introduction says that the definable powerset satisfies the description: every member of it is a definable subset, and the three conjuncts are supplied for the formula that defines it. The elimination says that nothing else does, and it is the direction the side condition is for, since a set the description holds of has to be re-entered member by member and a member arrives as an element of L or not at all.

  private
    describe : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S) → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (DA.defSet ψ ≡ fst z)) ∥₁
    describe w γ qw z = PT.rec squash₁ viaCode
      where
      Target : Type (ℓ-suc ℓ)
      Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (DA.defSet ψ ≡ fst z)) ∥₁

      viaValue : (c : S)
               → Σ[ v ∈ S ] ⟨ (v ∷ c ∷ z ∷ γ) ⊨ DefBody w ⟩ → Target
      viaValue c (v , hv) = read w γ qw z c v hv

      viaCode : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (DefBody w) ⟩ → Target
      viaCode (c , hc) = PT.rec squash₁ (viaValue c) hc

    assemble : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S)
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (DA.defSet ψ ≡ fst z)) ∥₁
             → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
    assemble w γ qw z = PT.rec (snd ((z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)))) step
      where
      step : Σ[ ψ ∈ Formula ⟪ fst A ⟫  ] (DA.defSet ψ ≡ fst z)
           → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
      step (ψ , qψ) = ∣ keyS A ψ , ∣ Sat A (toS ψ) , fill w γ qw z ψ qψ ∣₁ ∣₁

  DefAt-in : ∀ {n} (u w : Fin n) (γ : S ^ n)
           → fst (lookup w γ) ≡ fst A
           → fst (lookup u γ) ≡ 𝒟ₒ (fst A)
           → ⟨ γ ⊨ DefAt u w ⟩
  DefAt-in {n} u w γ qw qu = extAt-in-both u Φ γ f g
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    f : (z : S) → ⟨ fst z ∈ fst (lookup u γ) ⟩ → ⟨ (z ∷ γ) ⊨ Φ ⟩
    f z z∈ = assemble w γ qw z
      (𝒟ₒ-inv (fst A) (fst z) (subst (λ X → ⟨ fst z ∈ X ⟩) qu z∈))

    g : (z : S) → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ⟨ fst z ∈ fst (lookup u γ) ⟩
    g z hz = subst (λ X → ⟨ fst z ∈ X ⟩) (sym qu)
      (𝒟ₒ-intro (fst A) (fst z) (describe w γ qw z hz))

  DefAt-out : ∀ {n} (u w : Fin n) (γ : S ^ n) → DefOK A
            → fst (lookup w γ) ≡ fst A
            → ⟨ γ ⊨ DefAt u w ⟩
            → fst (lookup u γ) ≡ 𝒟ₒ (fst A)
  DefAt-out {n} u w γ ok qw h =
    extensionality (fst (lookup u γ)) (𝒟ₒ (fst A)) (sub₁ , sub₂)
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    sub₁ : ⟨ fst (lookup u γ) ⊆ 𝒟ₒ (fst A) ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = 𝒟ₒ (fst A)} .fst
      (𝒟ₒ-intro (fst A) y (describe w γ qw yS (extAt-out u Φ γ h yS y∈)))
      where
      y∈ : ⟨ y ∈ fst (lookup u γ) ⟩
      y∈ = ∈∈ₛ {a = y} {b = fst (lookup u γ)} .snd y∈ₛ

      yS : S
      yS = y , isL-trans {x = fst (lookup u γ)} {y = y} y∈ (snd (lookup u γ))

    sub₂ : ⟨ 𝒟ₒ (fst A) ⊆ fst (lookup u γ) ⟩
    sub₂ y y∈ₛ = ∈∈ₛ {a = y} {b = fst (lookup u γ)} .fst
      (extAt-in u Φ γ h yS
        (assemble w γ qw yS (𝒟ₒ-inv (fst A) y y∈)))
      where
      y∈ : ⟨ y ∈ 𝒟ₒ (fst A) ⟩
      y∈ = ∈∈ₛ {a = y} {b = 𝒟ₒ (fst A)} .snd y∈ₛ

      yS : S
      yS = y , ok y y∈

At a stage, and the side condition is gone

The instantiation, and the whole of it is one equation. A stage is an element of L, its definable subsets are constructible because a stage is constructible one stage later, and those two facts are what the successor identity delivers at every stage at once. So the side condition is discharged for good, and what is left is an equivalence of truth values: at a carrier holding a stage, the description holds of a set exactly when that set is the definable powerset of that stage. It holds of 𝒟ₒS and of nothing else.

Neither statement mentions the stage as anything but the value of a slot, which is what the internal hierarchy needs: the description will be spoken under a binder, and the equation the caller supplies is the only thing that connects it to a stage at all.

DefAt-stage : (β : V ℓ) (oβ : IsOrd β) → ∀ {n} (u w : Fin n) (γ : S ^ n)
            → fst (lookup w γ) ≡ Lset β
            → (γ ⊨ DefAt u w)
              ≡ ( (fst (lookup u γ) ≡ 𝒟ₒ (Lset β))
                , setIsSet (fst (lookup u γ)) (𝒟ₒ (Lset β)) )
DefAt-stage β oβ u w γ qw = ⇔toPath
  (DefAt-out (LsetS β oβ) u w γ (𝒟ₒ→isL β oβ) qw)
  (DefAt-in (LsetS β oβ) u w γ qw)

DefAt-𝒟ₒS : (β : V ℓ) (oβ : IsOrd β) → ∀ {n} (u w : Fin n) (γ : S ^ n)
          → lookup w γ ≡ LsetS β oβ → lookup u γ ≡ 𝒟ₒS β oβ
          → ⟨ γ ⊨ DefAt u w ⟩
DefAt-𝒟ₒS β oβ u w γ qw qu =
  DefAt-in (LsetS β oβ) u w γ (cong fst qw) (cong fst qu)

Recap

DefAt is the definable powerset described in the object language at a carrier that is a slot, and DefAt-in and DefAt-out are its two readings: the operator satisfies the description, and under DefOK nothing else does. DefAt-stage spends both at a stage, where the side condition is discharged once and for all and the description becomes an equation between truth values.

Three chapters meet here and not one of them is re-proved. The code predicate is read at a slot, the satisfaction graph is read at a slot, and the definable subset is read through the bridge that says the recursion's value is satisfaction over the carrier. What is new is only the joining: envOneAt, one line, because an environment of length one is a single pair, and DefinesAt, which is extAt over a two-part condition.

Two measurements are worth keeping. The adjacency correction was adopted before the first line was written and it cost nothing, so no weakening lemma exists anywhere on this route. And the one wall met while writing was not in the mathematics at all: the code predicate's elimination at a pinned carrier, with the truncation's payload left to inference, ran past 140 seconds and was killed there, while the same two lines with the payload type written out check in two. Every PT.rec here names its payload, and that is why this chapter checks in half a minute rather than not at all.