---
title: "A formula for the definable power set"
module: L.Coding.DefinablePowerSet
lang: en
site: "Bedrock"
description: "A formula for the definable power set"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 69
canonical: https://bedrock.institute/en/L.Coding.DefinablePowerSet.html
html: L.Coding.DefinablePowerSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/DefinablePowerSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Axioms.Basic, L.Coding.Model, L.Coding.Expressions, L.Coding.Environment, L.Coding.FormulaRecovery, L.Coding.CodeSet, L.Coding.SatisfactionGraph, L.Coding.EnvironmentTower, L.Coding.Quantification, L.Coding.PinnedRecursion, L.Coding.SatisfactionTable, L.Coding.SlotClosure, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.UniformSatisfaction]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.DefinablePowerSet.md, https://bedrock.institute/ja/L.Coding.DefinablePowerSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# A formula for the definable power set

This chapter combines formula codes with uniform satisfaction to define a first-order predicate for membership in a carrier’s definable power set, and proves that the predicate selects exactly the subsets defined by one-variable formulas.

This is the step the whole route exists for. Every chapter before it built a
component 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.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
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; LsetS )
open import L.Coding.Model {ℓ} using ( domAt-out )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both; tagAtL; tagAtL-adequate )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.FormulaRecovery {ℓ} 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.SatisfactionGraph {ℓ} lem
  using ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
        ; Bi; Ti; Ci; Ei; NN; ev; numν )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( keyʟ; slot; satTable; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge; fr; frTags; frTow; frDom )

open import Cubical.Foundations.Prelude using ( subst2 )
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 )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropStructure 𝒮ʟ

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

## The environment with one entry

`envOne v` is the graph assigning the sole free variable to `v`. The formula `envOneAt e y` recognizes exactly this graph, with `envOneAt-in` and `envOneAt-out` proving both directions.

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.

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

envOneAt : ∀ {n} → Fin n → Fin n → Formula S n
envOneAt e y = extAt e (tagAtL zero 0 (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 (# 0) v
    readEntry z = PT.rec (setIsSet (fst z) (pr (# 0) v))
      (λ { (lift zero , q) → sym q ; (lift (suc ()) , _) })

    entry∈ : (z : S) → fst z ≡ pr (# 0) 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 0 (suc y)) γ fwd bwd
    where
    fwd : (z : S) → ⟨ fst z ∈ fst E ⟩ → ⟨ (z ∷ γ) ⊨ tagAtL zero 0 (suc y) ⟩
    fwd z z∈ = subst ⟨_⟩ (sym (tagAtL-adequate zero 0 (suc y) (z ∷ γ)))
      (readEntry z (subst (λ w → ⟨ fst z ∈ w ⟩) q z∈))

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

  envOneAt-out : ⟨ γ ⊨ envOneAt e y ⟩ → fst E ≡ envOne v
  envOneAt-out h = extensionalV (λ w → ⇔toPath (sub₁ w) (sub₂ w))
    where
    sub₁ : (w : V ℓ) → ⟨ w ∈ fst E ⟩ → ⟨ w ∈ envOne v ⟩
    sub₁ w w∈ = entry∈ wS (subst ⟨_⟩
        (tagAtL-adequate zero 0 (suc y) (wS ∷ γ))
        (extAt-out e (tagAtL zero 0 (suc y)) γ h wS w∈))
      where
      wS : S
      wS = w , isL-trans {x = fst E} {y = w} w∈ (snd E)

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

## Recognizing the subset defined by a code

`DefinesAt x w v` says that `x` contains exactly those elements whose one-entry environments occur in the satisfaction value `v` attached to code `w`. Its three reading lemmas expose each direction and their equivalence.

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.

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

## Recognizing codes over a variable carrier

`isCodeAt c w` recognizes when `c` is the key of a one-variable formula whose constants are members of the carrier at slot `w`. The introduction and elimination lemmas translate this formula to an explicit coded formula.

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

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

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

## Satisfaction over a variable carrier

Given a formula over members of the carrier stored at `w`, `graphAt-holds` supplies its formula key and uniform satisfaction value in the graph, while `graphAt-unique` proves that this value is unique.

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

```agda
module _ (B : S) where
  private
    toB : ∀ {n} → Formula ⟪ fst B ⟫ n → Formula S n
    toB = mapFo (asConst B)

  graphAt-holds : ∀ {m n} (ψ : Formula ⟪ fst B ⟫ m) (w c v : Fin n) (γ : S ^ n)
                → fst (lookup w γ) ≡ fst B
                → fst (lookup c γ) ≡ fst (keyʟ (toB ψ))
                → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
                → ⟨ γ ⊨ satGraphAt w c v ⟩
  graphAt-holds {m} {n} ψ w c v γ qw qc qv = graphAt-in w c v γ
    ∣ numν
    , (Tower.tower B
    , (slot B φ
    , (satTable B φ
    , (B
    , (sym qw
    , (frTags B φ γ
    , (frTow B φ γ
    , (slotClosed B φ (Tower.tower B ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
    , (frDom B φ γ
    , (entry
    , SlotHolds.holds B Ti Bi Ci Ei NN (fr B φ γ) refl
        (frTags B φ γ) (frTow B φ γ) ψ refl refl)))))))))) ∣₁
    where
    φ : Formula S m
    φ = toB ψ

    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 ⟪ fst B ⟫ m) (w c v : Fin n) (γ : S ^ n)
                 → fst (lookup w γ) ≡ fst B
                 → fst (lookup c γ) ≡ fst (keyʟ (toB ψ))
                 → ⟨ γ ⊨ satGraphAt w c v ⟩
                 → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
  graphAt-unique {m} {n} ψ w c v γ qw qc h =
    PT.rec (setIsSet (fst (lookup v γ)) (fst (Sat B (toB ψ)))) step
      (graphAt-out w c v γ h)
    where
    step : GraphWitAt w c v γ → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
    step (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12)))))))))))
      = SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) B (eb ∙ qw) tg hE hc h12
          ψ (subst (λ u → ⟨ u ∈ fst C ⟩) (qc ∙ sym (keyBridge B ψ))
               (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup c γ) (lookup v γ) ha))
          (lookup v γ)
          (subst (λ u → ⟨ pr u (fst (lookup v γ)) ∈ fst T ⟩)
             (qc ∙ sym (keyBridge B ψ)) ha)
```

## The definable-power-set description

`DefAt u w` says that every member of `u` is defined over the carrier at `w` by some one-variable code and its graph value. `DefOK` records the constructibility condition required to interpret this description for a general carrier.

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.

```agda
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 defining formula in both directions

For a fixed one-variable formula, `fill` builds witnesses showing that its definable subset satisfies `DefAt`, and `read` recovers from such witnesses equality with the corresponding definable subset.

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.

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

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

    defined-membership : (ψ : Formula ⟪ fst A ⟫ 1) (y : V ℓ)
                       → (y ∈ DA.defSet ψ)
                       ≡ ((y ∈ fst A) ⊓ (envOne y ∈ fst (Sat A (toS ψ))))
    defined-membership ψ y = ⇔toPath out inn
      where
      at : ⟨ y ∈ fst A ⟩ → (y ∈ DA.defSet ψ) ≡ (envOne y ∈ fst (Sat A (toS ψ)))
      at hy = cong (λ u → u ∈ DA.defSet ψ) (sym e)
        ∙ defSet-Sat A ψ m ∙ cong (λ u → envOne u ∈ fst (Sat A (toS ψ))) e
        where
        m = ∈-asFiber {a = y} {b = fst A} hy .fst
        e = ∈-asFiber {a = y} {b = fst A} hy .snd
      out : ⟨ y ∈ DA.defSet ψ ⟩ → ⟨ y ∈ fst A ⟩ × ⟨ envOne y ∈ fst (Sat A (toS ψ)) ⟩
      out h = DA.defSet⊆A ψ y h , subst ⟨_⟩ (at (DA.defSet⊆A ψ y h)) h
      inn : ⟨ y ∈ fst A ⟩ × ⟨ envOne y ∈ fst (Sat A (toS ψ)) ⟩ → ⟨ y ∈ DA.defSet ψ ⟩
      inn (hy , h) = subst ⟨_⟩ (sym (at hy)) h

  fill : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z : S) (ψ : Formula ⟪ fst A ⟫ 1) → 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 ψ (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 ψ)) ⟩

    agrees : (y : S) → (fst y ∈ fst z)
           ≡ ((fst y ∈ fst (lookup w γ)) ⊓ (envOne (fst y) ∈ fst (Sat A (toS ψ))))
    agrees y = cong (λ X → fst y ∈ X) (sym qz)
      ∙ defined-membership ψ (fst y)
      ∙ cong (λ X → (fst y ∈ X) ⊓ (envOne (fst y) ∈ fst (Sat A (toS ψ)))) (sym qw)

    into : (y : S) → ⟨ fst y ∈ fst z ⟩ → Holds y
    into y = subst ⟨_⟩ (agrees y)

    back : (y : S) → Holds y → ⟨ fst y ∈ fst z ⟩
    back y = subst ⟨_⟩ (sym (agrees y))

    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 ⟫ 1 ] (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 ⟫ 1 ] (fst c ≡ fst (keyS A ψ))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
    step (ψ , qc) = ∣ ψ , extensionalV (λ y → ⇔toPath (into y) (back y)) ∣₁
      where
      qv : fst v ≡ fst (Sat A (toS ψ))
      qv = graphAt-unique A ψ (sh3 w) (suc zero) zero δ qw
             (qc ∙ keyBridge A ψ) hgraph

      into : (y : V ℓ) → ⟨ y ∈ DA.defSet ψ ⟩ → ⟨ y ∈ fst z ⟩
      into y hy = DefinesAt-in (suc (suc zero)) (sh3 w) zero δ hdef
        (y , isL-trans (DA.defSet⊆A ψ y hy) (snd A))
        (subst (λ X → ⟨ y ∈ X ⟩) (sym qw) (h .fst)
        , subst (λ X → ⟨ envOne y ∈ X ⟩) (sym qv) (h .snd))
        where h = subst ⟨_⟩ (defined-membership ψ y) hy

      back : (y : V ℓ) → ⟨ y ∈ fst z ⟩ → ⟨ y ∈ DA.defSet ψ ⟩
      back y hy = subst ⟨_⟩ (sym (defined-membership ψ y))
        (subst (λ X → ⟨ y ∈ X ⟩) qw (h .fst)
        , subst (λ X → ⟨ envOne y ∈ X ⟩) qv (h .snd))
        where
        h = DefinesAt-out (suc (suc zero)) (sh3 w) zero δ hdef
          (y , isL-trans hy (snd z)) hy
```

## Reading and assembling the description

The `describe` argument reads a `DefAt` witness through its satisfaction value, while `assemble` starts from an explicit defining formula. Together they prove the introduction and elimination specifications for the complete 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 each member either is an element of `L` or is absent
altogether.

```agda
  private
    describe : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S) → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
    describe w γ qw z = PT.rec squash₁ viaCode
      where
      Target : Type (ℓ-suc ℓ)
      Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (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 ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
             → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
    assemble w γ qw z = PT.rec (snd ((z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)))) step
      where
      step : Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (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 =
    extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    sub₁ : (y : V ℓ) → ⟨ y ∈ fst (lookup u γ) ⟩ → ⟨ y ∈ 𝒟ₒ (fst A) ⟩
    sub₁ y y∈ = 𝒟ₒ-intro (fst A) y (describe w γ qw yS (extAt-out u Φ γ h yS y∈))
      where
      yS : S
      yS = y , isL-trans {x = fst (lookup u γ)} {y = y} y∈ (snd (lookup u γ))

    sub₂ : (y : V ℓ) → ⟨ y ∈ 𝒟ₒ (fst A) ⟩ → ⟨ y ∈ fst (lookup u γ) ⟩
    sub₂ y y∈ = extAt-in u Φ γ h yS (assemble w γ qw yS (𝒟ₒ-inv (fst A) y y∈))
      where
      yS : S
      yS = y , ok y y∈
```

## Definable power sets at constructible stages

When the carrier is a constructible stage, its formula codes and uniform satisfaction objects already belong to `L`, so `DefOK` is discharged. The resulting specialization says directly that `DefAt` defines the stage’s definable power set.

The instantiation is just 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.

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

## Recap

The chapter has produced a bounded formula whose extension over a constructible stage is exactly the collection of subsets definable over that stage with parameters from it.

`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` instantiates both readings 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 recording. 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 difficulty 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
terminated there, while the same two lines with the payload type written out
check in two seconds. Every `PT.rec` here names its payload, and that is
why this chapter checks in half a minute rather than not at all.