---
title: "Building and collapsing a Skolem hull"
module: L.GCH.SkolemHull
lang: en
site: "Bedrock"
description: "Building and collapsing a Skolem hull"
stage: "Proving GCH"
reading_order: 105
canonical: https://bedrock.institute/en/L.GCH.SkolemHull.html
html: L.GCH.SkolemHull.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/SkolemHull.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Absoluteness, FOL.Manipulation.ConstantOccurrences, FOL.Semantics, FOL.Manipulation.ParameterAbstraction, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.Renaming, V.Hierarchy, V.Presentation, V.Collapse, V.Smallness, L.Axioms.Basic, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Rank, L.WellOrder.Base, L.Choice.StageOrders, L.Coding.CodeConstructibility]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.SkolemHull.md, https://bedrock.institute/ja/L.GCH.SkolemHull.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Building and collapsing a Skolem hull

This chapter builds the Skolem hull of a starting set inside a constructible stage, proves that the hull is elementary in the stage, collapses it onto a transitive set by a membership-preserving bijection, and records how satisfaction and bounded formulas travel across that collapse. The key distinction is that the hull itself is only a coded image; transitivity appears only after the Mostowski collapse.

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

The chapter runs on classical logic, and the hypothesis enters here. The hull construction decides satisfiability of queries, the extensionality proof decides membership in both directions, and the elementarity transfer eliminates double negation; each of these steps consumes excluded middle.

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

The module fixes the universe level `ℓ` and states the standing form of the classical hypothesis: excluded middle is received at `ℓ-suc ℓ` as an explicit parameter, never assumed globally, so every theorem of the chapter records exactly which level instance it uses.

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

The object language is the book's first-order language: formulas built from terms by equality and membership, closed under the propositional connectives and under unbounded and bounded quantifiers. The predicate `Δ₀` singles out the formulas whose quantifiers are all bounded.

```agda
open import FOL.ZFStructure using ( ZFStructure; module hPropStructure; _↾_ )
open import FOL.Syntax using
  ( Formula; Term; con; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊥̇
  ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
```

The predicate `Δ₀` is an inductive certificate following the structure of a formula: its constructors cover atoms, connectives, and bounded quantifiers, while unbounded quantifiers have no constructor. Such a certificate supports the later absoluteness argument; `countFo` and `constantsFo` record every constant occurrence.

```agda
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Absoluteness
import FOL.Manipulation.ConstantOccurrences
import FOL.Semantics
open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo )
```

Parameter abstraction replaces constant occurrences by extra environment variables; constant mapping and relabelling change constant alphabets while preserving semantics; and `renameTm` renames variable slots along a context map, providing the weakening by `suc` used below. The ambient hierarchy is opened with its extensionality, the property that sets with the same members are equal.

```agda
open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm; mapFo-comp; embed )
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀; ⊨-map )
open import FOL.Manipulation.Renaming using ( renameTm )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
```

Presentations index the elements of a set by a small type with an embedding, and their fibers name presented elements. The collapse constructs a transitive image of any carrier `X`; extensionality of the restricted membership relation is needed later to make the collapse map injective on `X`. Δ₀ smallness separates a bounded-definable class into a set. The empty set belongs to every definability successor, and `Lset-suc` identifies the stage at a successor index with the definable powerset of the preceding stage.

```agda
open import V.Presentation {ℓ} using ( member; fiber )
open import V.Collapse {ℓ} using ( module Collapse; isExt; isTrans )
open import V.Smallness {ℓ} using ( separateFromSmall; module Δ₀Small )
open import L.Axioms.Basic {ℓ} using ( ∅∈𝒟ₒ; Lset-suc )
open import L.Constructible {ℓ}
```

The constructible stage `Lset α` is transitive and its construction is monotone in the index, so a larger index yields a larger stage. The ordinal facts used repeatedly in the hull argument are that members of ordinals are ordinals, that `ω` is an ordinal, that numerals belong to `ω`, and that the empty set is an ordinal.

```agda
  using ( 𝒮ʟ; isTransV; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ
        ; layer-trans; Lset-layer )
open import L.Ordinal {ℓ} using ( mem-ord; ω-ord; #∈ω; ∅-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈; rank-Lset )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
```

Well orders come with a least-element selector: from the truncated existence of some element satisfying a predicate, it returns an element that satisfies the predicate and is least in the well order. The rank characterization of stage membership and the stage orders restricted to a stage carrier feed this selector its inputs, and the coding of unions and singletons builds the finite starting sets used later.

```agda
open import L.Rank {ℓ} using ( rank-fix )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; leastOf )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt )
open import L.Coding.CodeConstructibility {ℓ} using ( cup-out; cup-inl; cup-inr; sgl-out )
```

The environments of this chapter are vectors of carrier elements, and the operations on them are componentwise: mapping a function over an environment, looking up an index, extending by one element, and concatenating. Pairs with propositional second components record elements together with certificates that never distinguish.

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( Vec; map; lookup; _∷_; []; _++_ )
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_; _,_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
```

The empty type represents contradiction: `Empty.rec` eliminates an inhabitant into any target, while `isProp⊥` allows a truncation to be eliminated when the target is contradiction. Satisfaction of existential formulas and membership in presented sets are expressed by propositional truncation, so they retain existence without choosing a witness.

```agda
import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

The cumulative hierarchy presents a set by an index type and a valuation. The hull uses the finite tree type `Code` as its index type; formulas occur inside witness codes, but are not themselves the codes. The constructions supply the empty set, unions, unordered-pair and singleton constructions, and the infinite ordinal with its successor.

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; _∪_; ⁅_,_⁆; ⁅_⁆s; union-ax; pairing-ax; module InfinitySet
        ; SetPackage; SingletonPackage )  -- lint-agda: keep (SetPackage via record projection)
open InfinitySet using ( ω; sucV )
```

The small membership relation `_∈ₛ_` and its bridge `∈∈ₛ` to the ambient membership `_∈ˢ_` connect the presented reading of a set with its reading inside the hierarchy: what a presentation records internally is exactly what holds in the universe.

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; extensionality )
```

Opening the ambient structure fixes the unqualified symbols for ambient equality and membership; restricted structures introduced below retain their own semantic interpretations.

```agda
open hPropStructure 𝒮ᵥ
```

`SemV` supplies the fixed-length ambient environments used when satisfaction is instantiated below. For formulas whose constants range over `𝒮ʟ`, counting occurrences identifies the constant-free case; `erase` then replaces its impossible constants by the empty constant domain without changing satisfaction.

```agda
module SemV = FOL.Semantics 𝒮ᵥ using ( _^_; module At )
open SemV using ( _^_ )
module CS = hPropStructure 𝒮ʟ using ( S )
module Cnt = FOL.Manipulation.ConstantOccurrences.ZeroOccurrences CS.S using ( erase; erase-inv )
```

With an empty constant domain, `Δ₀-small` shows that the truth value of every bounded formula at every environment is equivalent to a proposition one universe lower; separation requires a separate application of `separateFromSmall`. The term algebra then begins: it is parameterized by a structure, a map of its carrier into the ambient universe, and a well order on that carrier.

```agda
module D0 = Δ₀Small {ℓc = ℓ-suc ℓ} {K = ⊥* {ℓ-suc ℓ}} (λ b → Empty.rec* b)
  using ( Δ₀-small )
module TermAlgebra (𝒮 : ZFStructure (ℓ-suc ℓ))
                   (toSet : ZFStructure.S 𝒮 → V ℓ)
                   (wo : SWO (ZFStructure.S 𝒮))
```

The remaining parameters are a default element `junk` and a family of base generators indexed by `K`; only the later hull instance identifies `K` with a presentation of the starting set. The junk value is a bookkeeping device, and the constructions below never inspect it.

```agda
                   (junk : ZFStructure.S 𝒮)
                   {K : Type ℓ} (emb : K → ZFStructure.S 𝒮) where
```

Only the unqualified Agda name `_∈ˢ_` is hidden from the parameter structure; satisfaction `_⊨₀_` still interprets atomic membership using `𝒮`. Renaming the carrier keeps the chapter's own references to the ambient carrier unambiguous.

```agda
  open ZFStructure 𝒮 hiding ( _∈ˢ_ ) renaming ( S to S𝒮 )
```

Satisfaction for the term algebra is stated at the trivially empty constant domain: the formulas evaluated are exactly those built without constant symbols, the language of pure membership and equality, and satisfaction is proposition-valued. Every query and closure statement in this section uses this reading.

```agda
  private module Sem = FOL.Semantics 𝒮
  open Sem using () renaming ( _^_ to _^𝒮_ )
  module At0 = Sem.At (⊥* {ℓ}) Empty.rec* using ( _⊨_ )
  _⊨₀_ : {n : ℕ} → S𝒮 ^𝒮 n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
  _⊨₀_ = At0._⊨_
```

The codes form a finite tree algebra over the base generators: a base code names a generator, and a witness code records a query of arity `suc k` together with `k` parameter codes. Because `Code` is inductive, every code is a finite tree, and the entries of `cs` are its immediate parameter subcodes, each of which may itself be a base or witness code.

```agda
  data Code : Type ℓ where
    base : K → Code
    wit  : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec Code k → Code
```

`Sat k ψ vs` is the mere existence of an element satisfying `ψ` at the arbitrary parameter vector `vs`; the closure theorem later specializes `vs` to the values of codes. Satisfiability is stated as truncated existence: it asserts that a witness exists, without producing one.

```agda
  Sat : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec S𝒮 k → Type (ℓ-suc ℓ)
  Sat k ψ vs = ∥ Σ[ a ∈ S𝒮 ] ⟨ (a ∷ vs) ⊨₀ ψ ⟩ ∥₁
```

Given this truncated existence, `search` returns a least satisfying element for the particular strict well-order supplied as the parameter `wo`. Least is meant in that well order; it is not minimality with respect to membership, and not a comparison of ranks.

```agda
  search : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
         → Sat k ψ vs → S𝒮
  search k ψ vs w = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vs) ⊨₀ ψ) w .fst
```

Code vectors are evaluated componentwise, mutually with the evaluation of single codes: the values of the parameters of a witness code are the values of its component codes.

```agda
  mutual
    vals : {m : ℕ} → Vec Code m → Vec S𝒮 m
    vals [] = []
    vals (c ∷ cs') = val c ∷ vals cs'
```

A satisfiable witness code evaluates to the least satisfying element; an unsatisfiable one evaluates to `junk`. Since every code contributes a value to the image, `junk` may occur in the hull, while `val-wit` shows that it is irrelevant whenever satisfiability is given.

```agda
    val : Code → S𝒮
    val (base m) = emb m
    val (wit k ψ cs) = Sum.rec (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))
```

The small lemma records how a classical decision is used once its propositional target is known inhabited. If the decision is left, propositionhood identifies its inhabitant with `x`, so the eliminator equals `f x`; if it is right, its refutation contradicts `x`, and the case is impossible.

```agda
  sum-stuck : {X : Type (ℓ-suc ℓ)} (x : X) (px : isProp X)
            → (f : X → S𝒮) (g : (X → Empty.⊥) → S𝒮) (s : X ⊎ (X → Empty.⊥))
            → Sum.rec f g s ≡ f x
  sum-stuck x px f g (Sum.inl x') = sym (cong f (px x x'))
  sum-stuck x px f g (Sum.inr h)  = Empty.rec (h x)
```

Given a satisfiability witness for the query stored in a witness code, this lemma identifies the value of the code with the search's least satisfying element: the junk branch is refuted, and the witnessed branch computes the search.

```agda
  val-wit : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
          → (w : Sat k ψ (vals cs)) → val (wit k ψ cs) ≡ search k ψ (vals cs) w
  val-wit k ψ cs w = sum-stuck w squash₁ (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))
```

Evaluating a code vector is the same as mapping the evaluation over it, proved by a simple recursion. This lets later statements pass freely between the recursive form and the mapped form of an environment.

```agda
  vals≡map : {m : ℕ} (cs : Vec Code m) → vals cs ≡ map val cs
  vals≡map [] = refl
  vals≡map (c ∷ cs') = cong₂ _∷_ refl (vals≡map cs')
```

The hull is presented exactly as the hierarchy presents its sets: a code family together with a valuation. It is the image of the values of all codes, and the presentation may repeat elements, since different codes may evaluate alike. Membership in the hull is therefore only the truncated existence of a code, and nothing in this chapter claims that the hull is transitive or that it is the smallest closed set.

```agda
  Hull : V ℓ
  Hull = sett Code (λ c → toSet (val c))
```

Membership in the presentation is direct: the value of any code is a member of the hull, witnessed by that very code.

```agda
  inHull : (c : Code) → ⟨ toSet (val c) ∈ˢ Hull ⟩
  inHull c = ∣ c , refl ∣₁
```

Thus every satisfiable coded query has a satisfying witness in the hull. The theorem asserts this closure property; it does not characterize all members of the hull as successful least witnesses.

```agda
  closed : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
         → Sat k ψ (vals cs)
         → ∥ Σ[ a ∈ S𝒮 ]
              (⟨ toSet a ∈ˢ Hull ⟩ × ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩) ∥₁
  closed k ψ cs w = ∣ a , a∈H , sat ∣₁
```

The witness is not searched for again: it is the value the term algebra already assigned, namely the least satisfying element returned by the search.

```agda
    where
    a : S𝒮
    a = search k ψ (vals cs) w
```

The selector returns `a` together with both components of `IsLeast`: a proof that `a` satisfies the query and a proof that no strictly smaller satisfying element exists; this line projects the first component.

```agda
    pa : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
    pa = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vals cs) ⊨₀ ψ) w .snd .fst
```

That the witness belongs to the hull comes from the witness code built for this very query: its value is identified with the search result by `val-wit`, and every code value lies in the hull.

```agda
    a∈H : ⟨ toSet a ∈ˢ Hull ⟩
    a∈H = subst (λ z → ⟨ toSet z ∈ˢ Hull ⟩) (val-wit k ψ cs w)
            (inHull (wit k ψ cs))
```

Satisfaction is the recorded component, and the closure clause is complete.

```agda
    sat : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
    sat = pa
```

## Transporting satisfaction along a carrier map

With the hull built and closed, the chapter turns to its second task, transporting satisfaction between structures, and states the transfer for two predicates on the ambient carrier.

```agda
module SatTransfer (MA MB : S → hProp (ℓ-suc ℓ)) where
```

The source carrier pairs each element of the ambient carrier with the proof that it satisfies the first predicate. Its formulas are read only at such pairs.

```agda
  SA : Type (ℓ-suc ℓ)
  SA = Σ[ x ∈ S ] ⟨ MA x ⟩
```

The target carrier is the same construction for the second predicate, and satisfaction there is the target reading of the same formulas.

```agda
  SB : Type (ℓ-suc ℓ)
  SB = Σ[ x ∈ S ] ⟨ MB x ⟩
```

The source structure reads formulas at the paired carrier: its term dictionary evaluates variables to the paired elements, and its satisfaction is proposition-valued.

```agda
  module SemA = FOL.Semantics (𝒮ᵥ ↾ MA)
    using ( module At )
  module SemB = FOL.Semantics (𝒮ᵥ ↾ MB)
    using ( module At )
  open SemA.At SA id renaming ( _⊨_ to _⊨ᴬ_ ; ⟦_⟧ to ⟦_⟧ᴬ )
```

The target structure does the same on the other side, with its own satisfaction and its own term dictionary.

```agda
  open SemB.At SB id renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```

Two principles organize the transfer. Agreement states, for every formula and environment, an equality of propositions: satisfaction on the left equals satisfaction of the mapped formula on the mapped environment. The witness principle, stated next, supports the backward existential direction: target existential truth must yield, merely, some `q : SA` whose image satisfies the matrix.

```agda
  Agree : (SA → SB) → Type (ℓ-suc (ℓ-suc ℓ))
  Agree g = (n : ℕ) (φ : Formula SA n) (δ : SA ^ n)
          → (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
  Witness : (SA → SB) → Type (ℓ-suc ℓ)
  Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : SA ^ n)
```

It need not identify `q` as the preimage of any previously chosen target witness; the principle only asserts the truncated existence of some inner point whose image satisfies the matrix, and that is exactly the form the backward existential direction consumes.

```agda
            → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ φ) ⟩
            → ∥ Σ[ q ∈ SA ] ⟨ (g q ∷ map g δ) ⊨ᴮ mapFo g φ ⟩ ∥₁
```

The transfer module receives the map together with the atomic hypotheses. Atomic membership and equality are required to agree in both directions across `g`, so that membership and equality atoms become paths of propositions in the induction.

```agda
  module Along (g : SA → SB)
    (at∈ : (n : ℕ) (t u : Term SA n) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ∈̇ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ∈̇ u)))
    (at≐ : (n : ℕ) (t u : Term SA n) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ≐ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ≐ u)))
```

The witness principle is the third hypothesis, completing the data of the transfer.

```agda
    (wit : Witness g) where
```

The first weakening fact is stated in the source structure. Renaming by `suc` shifts every old variable past the new head of the environment, so evaluation at `x ∷ δ` recovers evaluation at `δ`; constants are unaffected.

```agda
    private
      renA : {n : ℕ} (t : Term SA n) (x : SA) (δ : SA ^ n)
           → ⟦ renameTm suc t ⟧ᴬ (x ∷ δ) ≡ ⟦ t ⟧ᴬ δ
      renA (con c) x δ = refl
      renA (var i) x δ = refl
```

The same weakening is sound in the target structure, and the next statement begins the comparison of mapping with weakening.

```agda
      renB : {n : ℕ} (t : Term SB n) (x : SB) (δ : SB ^ n)
           → ⟦ renameTm suc t ⟧ᴮ (x ∷ δ) ≡ ⟦ t ⟧ᴮ δ
      renB (con c) x δ = refl
      renB (var i) x δ = refl
      mapTm-ren : {n : ℕ} (t : Term SA n)
```

Mapping and weakening commute on terms, definitionally: the map of a weakened term weakens each renamed component in turn.

```agda
                → mapTm g (renameTm suc t) ≡ renameTm suc (mapTm g t)
      mapTm-ren (con c) = refl
      mapTm-ren (var i) = refl
```

The mapped weakened term, evaluated at an arbitrary target point `x` followed by the mapped environment, has the same value as the mapped term at the mapped environment.

```agda
      renG : {n : ℕ} (t : Term SA n) (x : SB) (δ : SA ^ n)
           → ⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ) ≡ ⟦ mapTm g t ⟧ᴮ (map g δ)
      renG t x δ = cong (λ u → ⟦ u ⟧ᴮ (x ∷ map g δ)) (mapTm-ren t)
                 ∙ renB (mapTm g t) x (map g δ)
```

Membership against a term is unchanged by the weakening, in the form the bounded clauses consume; and the next lemma states the side-condition transfer itself.

```agda
      memRen : {n : ℕ} (t : Term SA n) (x : SB) (δ : SA ^ n)
             → (fst x ∈ˢ fst (⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ)))
             ≡ (fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memRen t x δ = cong (λ s → fst x ∈ˢ fst s) (renG t x δ)
      memPath : {n : ℕ} (t : Term SA n) (q : SA) (δ : SA ^ n)
```

The side condition of a bounded quantifier transfers across the map. The chain starts by weakening in the source structure, then applies the atomic membership hypothesis at the shifted environment.

```agda
              → (fst q ∈ˢ fst (⟦ t ⟧ᴬ δ))
              ≡ (fst (g q) ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memPath {n} t q δ =
        cong (λ s → fst q ∈ˢ fst s) (sym (renA t q δ))
        ∙ at∈ (suc n) (var zero) (renameTm suc t) (q ∷ δ)
```

The chain ends by weakening in the target structure. With it, the side condition of any bounded clause can be read on either side of the map.

```agda
        ∙ memRen t (g q) δ
```

The classical step is packaged once: for a proposition, double-negation elimination follows from excluded middle. The forward universal clauses assume a target counterexample, package it as an existential witness to the negated matrix, pull that counterexample back with `Witness`, and derive a contradiction; `dne` then yields the required target truth.

```agda
      dne : (P : hProp (ℓ-suc ℓ)) → (((⟨ P ⟩) → Empty.⊥) → Empty.⊥) → ⟨ P ⟩
      dne P h = Sum.rec (λ p → p)
        (λ (np : ⟨ P ⟩ → Empty.⊥) → Empty.rec (h np)) (lem P)
```

The induction now runs through the ten clauses, and it starts where the hypotheses are: the two atomic clauses are exactly `at∈` and `at≐`. The propositional connectives transport componentwise, because conjunction, disjunction, and implication on propositions are determined by their components.

```agda
    agree : Agree g
    agree n (t ∈̇ u) δ = at∈ n t u δ
    agree n (t ≐ u) δ = at≐ n t u δ
    agree n (φ ∧̇ ψ) δ = cong₂ _⊓_ (agree n φ δ) (agree n ψ δ)
    agree n (φ ∨̇ ψ) δ = cong₂ _⊔_ (agree n φ δ) (agree n ψ δ)
```

Implication transports componentwise in the same way, falsity is constant, and the existential clause opens with a biconditional. Its forward direction states that inner satisfaction of the existential maps to outer satisfaction of the mapped existential.

```agda
    agree n (φ ⇒̇ ψ) δ = cong₂ _⇒_ (agree n φ δ) (agree n ψ δ)
    agree n ⊥̇ δ = refl
    agree n (∃̇ ψ) δ = ⇔toPath fwd bwd
      where
      fwd : ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩ → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩
```

Forward eliminates the truncation of the inner witness and maps the witness; backward is where the witness principle pays: the outer satisfaction is fed to the witness principle, which returns an inner point whose image satisfies the matrix, and agreement transports that satisfaction back.

```agda
      fwd = PT.rec (snd (map g δ ⊨ᴮ mapFo g (∃̇ ψ)))
        (λ { (q , hq) → ∣ g q , subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hq ∣₁ })
      bwd : ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩ → ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩
      bwd h = PT.map (λ { (q , hq) →
        q , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) hq }) (wit n ψ δ h)
```

The universal clause is the classical one: its forward direction assumes every inner point satisfies the matrix, fixes an outer point `x`, and must show that `x` satisfies the matrix in the image. The proof begins by applying double-negation elimination, which is where excluded middle enters the transfer.

```agda
    agree n (∀̇ ψ) δ = ⇔toPath fwd bwd
      where
      fwd : ((q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x = dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
```

If `x` failed, the mapped environment would satisfy the negated matrix at `x`; the witness principle applied to that negation returns an inner point whose image satisfies the negation, and the agreement at that inner point refutes the assumption that every inner point satisfies the matrix.

```agda
        PT.rec isProp⊥ (λ { (q , hq) →
          lower (hq (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) (h q))) })
          (wit n (¬̇ ψ) δ ∣ x , (λ yes → lift (nx yes)) ∣₁)
      bwd : ((x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
```

Backward is direct, since every inner point maps into the outer carrier. The bounded universal then opens with an auxiliary formula that conjoins the side condition, membership in the renamed bound, with the negated matrix; satisfaction of the auxiliary is the classical reading of "in the bound but the matrix fails".

```agda
      bwd h q = subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (h (g q))
    agree n (∀̇∈ t ψ) δ = ⇔toPath fwd bwd
      where
      mat : Formula SA (suc n)
      mat = (var zero ∈̇ renameTm suc t) ∧̇ ¬̇ ψ
```

Forward states that if every inner point in the bound satisfies the matrix, then every outer point belonging to the mapped bound satisfies the mapped matrix. The proof again begins with double-negation elimination: assume the outer point fails.

```agda
      fwd : ((q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
          → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x hx =
        dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
```

The witness principle is applied to the auxiliary formula, returning an inner point `q` whose image lies in the bound but refutes the matrix. The image's membership in the bound is transported back through the weakening and `memPath`, and agreement then lifts the inner satisfaction of the matrix to its image, contradicting the failure.

```agda
        PT.rec isProp⊥ (λ { (q , hq) →
          lower (hq .snd (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ))
            (h q (subst ⟨_⟩ (sym (memPath t q δ))
                    (subst ⟨_⟩ (memRen t (g q) δ) (hq .fst)))))) })
          (wit n mat δ ∣ x , (subst ⟨_⟩ (sym (memRen t x δ)) hx
```

The auxiliary application closes with the witness record, whose second component is the failure of the matrix at the image, that is, the negated matrix. Backward states that outer satisfaction at images, together with the inner side condition, gives inner satisfaction of the matrix.

```agda
            , (λ yes → lift (nx yes))) ∣₁)
      bwd : ((x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                   → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
      bwd h q hq =
```

Backward applies the outer satisfaction at the image of the inner point, transporting the side condition by `memPath` and the matrix by agreement. The bounded existential then opens with its auxiliary matrix conjoining the side condition and the matrix itself.

```agda
        subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ)))
          (h (g q) (subst ⟨_⟩ (memPath t q δ) hq))
    agree n (∃̇∈ t ψ) δ = ⇔toPath fwd bwd
      where
      mat : Formula SA (suc n)
```

The auxiliary matrix is the side condition conjoined with the matrix, and forward states that an inner witness pair maps to an outer witness pair. The proof is a single mapping over the truncation.

```agda
      mat = (var zero ∈̇ renameTm suc t) ∧̇ ψ
      fwd : ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
          → ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
      fwd = PT.map (λ { (q , hq , hψ) →
```

The two components are transported separately: the side condition by `memPath` and the matrix by agreement. Backward states the converse, an outer witness pair yielding an inner one.

```agda
        g q , (subst ⟨_⟩ (memPath t q δ) hq ,
               subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hψ) })
      bwd : ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
          → ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
```

Backward runs the witness principle on the outer pair read in the auxiliary form, returning an inner point and a pair at its image; the components are then transported back through the weakening and `memPath`, and by agreement.

```agda
      bwd h = PT.map (λ { (q , hq) →
        q , ( subst ⟨_⟩ (sym (memPath t q δ))
                (subst ⟨_⟩ (memRen t (g q) δ) (hq .fst))
            , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (hq .snd)) })
        (wit n mat δ (PT.map (λ { (x , hx , hψ) →
```

The two components close the bounded-existential transfer, and the ten-clause induction is complete.

```agda
          x , (subst ⟨_⟩ (sym (memRen t x δ)) hx , hψ) }) h))
```

## The Tarski-Vaught criterion inside a stage

For an ordinal index `α`, the stage `Lset α` supplies the ambient structure in which this transfer will prove elementarity.

```agda
module AtStage (α : S) (ordα : IsOrd α) where
```

The stage is transitive, and the reason is precise: `Lset-layer α` proves that the layer at `α` is transitive, and `layer-trans` turns that into transitivity of `Lset α`. The ordinality hypothesis is not used here; it is reserved for the well order below.

```agda
  Ltr : isTransV (Lset α)
  Ltr = layer-trans (Lset-layer α)
```

Transitivity lets bounded formulas be interpreted absolutely between `Lset α` and the universe. Thus the restricted stage structure can be used as the outer semantics in the Tarski-Vaught argument.

```agda
  module AbsL = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ Lset α) Ltr
    using ( SM; 𝒮M; _⊨ᵐ_; ⟦_⟧ᵐ; abs₀ )
```

The stage carrier is the type of elements that belong to `Lset α`; every hull member and every stage reading below lives in this type.

```agda
  SL : Type (ℓ-suc ℓ)
  SL = AbsL.SM
```

The stage order of the earlier chapter restricts to a well order on this carrier. Fix a carrier `M` contained in this stage; its inclusion is part of the hypotheses.

```agda
  wL : SWO SL
  wL = orderAt α ordα
  module AtM (M : S) (M⊆L : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ x ∈ˢ Lset α ⟩) where
```

A carrier for the substructure is an element of the ambient carrier together with the proof that it belongs to `M`; formulas are read only at such pairs.

```agda
    SM : Type (ℓ-suc ℓ)
    SM = Σ[ x ∈ S ] ⟨ x ∈ˢ M ⟩
```

The semantics of the substructure is the ambient semantics restricted to `M`: terms evaluate inside the restriction, and satisfaction is proposition-valued.

```agda
    module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
      using ( module At )
    open SemM.At SM id renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

The inclusion into the stage pairs each element of the carrier with its stage membership, supplied by the containment hypothesis.

```agda
    inL : SM → SL
    inL c = fst c , M⊆L (fst c) (snd c)
```

Elementarity states that satisfaction is unchanged by this inclusion, for every formula and every environment of the carrier. It is a path of propositions, which is the form in which the two atomic congruences and the witness principle compose with it.

```agda
    Elementary : Type (ℓ-suc (ℓ-suc ℓ))
    Elementary = (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
               → (δ ⊨ᵐ φ) ≡ (map inL δ AbsL.⊨ᵐ (mapFo inL φ))
```

The Tarski-Vaught criterion is the witness form of elementarity: whenever the stage satisfies an existential at the image of an environment, some element of the carrier, imaged, satisfies the matrix there. Truncated existence suffices, since satisfaction is proposition-valued.

```agda
    TarskiVaught : Type (ℓ-suc ℓ)
    TarskiVaught = (n : ℕ) (φ : Formula SM (suc n)) (δ : SM ^ n)
                 → ⟨ map inL δ AbsL.⊨ᵐ (mapFo inL (∃̇ φ)) ⟩
                 → ∥ Σ[ q ∈ SM ] ⟨ (inL q ∷ map inL δ) AbsL.⊨ᵐ (mapFo inL φ) ⟩ ∥₁
```

Pointwise inclusion commutes with environment lookup; this is the variable case needed for term agreement.

```agda
    private
      lookup-inL : {n : ℕ} (i : Fin n) (δ : SM ^ n)
                 → lookup i (map inL δ) ≡ inL (lookup i δ)
      lookup-inL zero (c ∷ δ) = refl
      lookup-inL (suc i) (c ∷ δ) = lookup-inL i δ
```

Terms agree across the inclusion: a term of the carrier evaluates to the same underlying element whether read in the substructure or read mapped in the stage. Constants are fixed, variables follow the lookups. The transfer machinery is then instantiated at the two membership predicates.

```agda
      tm-agree : (n : ℕ) (t : Term SM n) (δ : SM ^ n)
               → fst (⟦ t ⟧ᵐ δ) ≡ fst (AbsL.⟦ mapTm inL t ⟧ᵐ (map inL δ))
      tm-agree n (con c) δ = refl
      tm-agree n (var i) δ = sym (cong fst (lookup-inL i δ))
    module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ Lset α)
```

Elementarity follows by instantiating the shared induction: the two atoms are the congruences just proved, the witness principle is exactly the Tarski-Vaught instance, and the shared body carries the boolean and quantifier clauses. Nothing about stages is used beyond the two congruences and the criterion.

```agda
    TV→elem : TarskiVaught → Elementary
    TV→elem tv = Tr.Along.agree inL
      (λ n t u δ → cong₂ _∈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
      (λ n t u δ → cong₂ _≈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
      tv
```

## Closing the starting set under least witnesses

A starting set `X` is assumed to lie in the stage, and the index `α` is assumed to contain the empty set. The empty set belongs to `Lset α` because `∅` lies in the ordinal `α` and is coded in the base layer.

```agda
  module Hull (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
               (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
    ∅∈Lsetα : ⟨ ∅ ∈ˢ Lset α ⟩
    ∅∈Lsetα = Lset-in α ∅ ∅ ∅∈α (∅∈𝒟ₒ ∅)
```

The embedding of the starting set's presentation lands in the stage carrier: each index names a member of `X`, and the containment hypothesis certifies that this member lies in the stage `Lset α`.

```agda
    inStg : ⟪ X ⟫ → SL
    inStg m = ⟪ X ⟫↪ m , X⊆L (⟪ X ⟫↪ m) (member X m)
```

The term algebra is instantiated at the restricted structure of the stage: its carrier is mapped into the universe by the first projection, the witness search uses the stage's well order, the junk value is the empty set, and the base codes are indexed by the presentation of `X`. The hull now grows inside the stage.

```agda
    module T = TermAlgebra AbsL.𝒮M fst wL (∅ , ∅∈Lsetα) {K = ⟪ X ⟫} inStg
    open T using ( Code; base; val; Hull; inHull )
```

The hull lies in the stage: every member is the value of some code, and every code value is a member of the stage `Lset α` by the term algebra's own typing. The proof eliminates the truncated presentation and transports along the identification.

```agda
    Hull⊆L : (x : S) → ⟨ x ∈ˢ Hull ⟩ → ⟨ x ∈ˢ Lset α ⟩
    Hull⊆L x x∈H = PT.rec (snd (x ∈ˢ Lset α)) go x∈H
      where
      go : Σ[ c ∈ Code ] (fst (val c) ≡ x) → ⟨ x ∈ˢ Lset α ⟩
      go (c , q) = subst (λ z → ⟨ z ∈ˢ Lset α ⟩) q (snd (val c))
```

Membership reads back only as truncated existence: a member of the hull is the value of some code, with no code selected. This is the honest form of the presentation, since different codes may evaluate alike.

```agda
    hull-member : (x : S) → ⟨ x ∈ˢ Hull ⟩
                → ∥ Σ[ c ∈ Code ] (fst (val c) ≡ x) ∥₁
    hull-member x x∈H = x∈H
```

In the other direction no truncation is needed: the value of every code is a member, by the presentation's own introduction rule.

```agda
    val-in-Hull : (c : Code) → ⟨ fst (val c) ∈ˢ Hull ⟩
    val-in-Hull c = inHull c
```

The starting set enters the hull member by member. A member `x` of `X` is presented by an index, and the fiber of the presentation at `x` returns that index.

```agda
    module XInM (x : S) (x∈X : ⟨ x ∈ˢ X ⟩) where
      mx : ⟪ X ⟫
      mx = fiber X x∈X .fst
```

The fiber carries the identification of the presented element with `x`, which is the transport used to move memberships along.

```agda
      x≡val : ⟪ X ⟫↪ mx ≡ x
      x≡val = fiber X x∈X .snd
```

The base code at that index evaluates to the presented element, hence to `x`; the transport lands membership of `x` in the hull.

```agda
      inM : ⟨ x ∈ˢ Hull ⟩
      inM = subst (λ z → ⟨ z ∈ˢ Hull ⟩) x≡val (inHull (base mx))
```

Assembled once, the containment of the starting set in the hull becomes a single lemma.

```agda
    X⊆M : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Hull ⟩
    X⊆M x x∈X = XInM.inM x x∈X
```

## Satisfaction is invariant under the collapse isomorphism

To compare satisfaction before and after an isomorphism, fix sets `M`, `PM`, and a carrier map `p` from members of `M` to members of `PM`.

```agda
module IsoInv (M : S) (PM : S)
  (p : S → S)
  (p∈ : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ p x ∈ˢ PM ⟩)
```

Besides the closure condition `p∈`, the map `p` satisfies four hypotheses. `iso-fwd` preserves membership, `iso-bwd` reflects it, and the last two parameters state injectivity on `M` and surjectivity onto the target `PM`.

```agda
  (iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
           → ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩)
  (iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
           → ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩)
  (p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
```

The map `p` is injective on `M` and merely surjective onto `PM`. With preservation and reflection, these are exactly the data of a membership isomorphism between the two structures.

```agda
          → p x ≡ p y → x ≡ y)
  (surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
        → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (p y ≡ z)) ∥₁)
  where
```

The source carrier pairs each element of `M` with its membership proof, as in every restricted structure of the chapter.

```agda
  SM : Type (ℓ-suc ℓ)
  SM = Σ[ x ∈ S ] ⟨ x ∈ˢ M ⟩
```

The target carrier pairs each element of `PM` with its membership proof.

```agda
  SPM : Type (ℓ-suc ℓ)
  SPM = Σ[ x ∈ S ] ⟨ x ∈ˢ PM ⟩
```

The isomorphism lifts to the paired carriers: apply `p` to the underlying element and certify membership in the image.

```agda
  g : SM → SPM
  g m = p (fst m) , p∈ (fst m) (snd m)
```

The source semantics interprets terms and formulas in the restriction to `M`.

```agda
  module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
    using ( module At )
  module SemPM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ PM))
    using ( module At )
  open module Mse = SemM.At SM id public renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

The target semantics interprets the mapped terms and formulas in the restriction to `PM`.

```agda
  open module Pse = SemPM.At SPM id public renaming ( _⊨_ to _⊨ᵖᵐ_ ; ⟦_⟧ to ⟦_⟧ᵖᵐ )
```

Surjectivity promotes to the paired carriers: every element of the target `PM` is the image of some point of `M`, and the equality of underlying elements lifts to an equality of pairs because membership in `PM` is a proposition.

```agda
  surj' : (p' : SPM) → ∥ Σ[ q ∈ SM ] (g q ≡ p') ∥₁
  surj' (z , z∈) = PT.map (λ { (y , y∈ , e) →
    (y , y∈) , Σ≡Prop (λ w → (w ∈ˢ PM) .snd) e }) (surj z z∈)
```

The general satisfaction-transfer theorem now applies to the predicates of membership in `M` and `PM`; preservation and reflection supply its membership atom.

```agda
  module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ PM)
```

The map `p` is applied pointwise to environments, so lookups reduce one index at a time.

```agda
  private
    lookup-g : {n : ℕ} (i : Fin n) (δ : SM ^ n)
             → p (fst (lookup i δ)) ≡ fst (lookup i (map g δ))
    lookup-g zero (m ∷ δ) = refl
    lookup-g (suc i) (m ∷ δ) = lookup-g i δ
```

Terms agree under the map `p`: applying `p` to the value of a term of `M` equals evaluating the mapped term at the mapped environment. Constants are fixed; variables follow the lookups. The membership atoms can now be stated.

```agda
    tm-agree : {n : ℕ} (t : Term SM n) (δ : SM ^ n)
             → p (fst (⟦ t ⟧ᵐ δ)) ≡ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ))
    tm-agree (con m) δ = refl
    tm-agree (var i) δ = lookup-g i δ
    at∈ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
```

Membership of atomic terms transfers in both directions: forward, the proof transports inner membership along the term equalities and then applies `iso-fwd`, the preservation of membership.

```agda
        → (δ ⊨ᵐ (t ∈̇ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ∈̇ u))
    at∈ n t u δ = ⇔toPath
      (λ h → subst (λ z → ⟨ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ∈ˢ z ⟩) (tm-agree u δ)
        (subst (λ z → ⟨ z ∈ˢ p (fst (⟦ u ⟧ᵐ δ)) ⟩) (tm-agree t δ)
          (iso-fwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
```

The forward transport lands at membership after applying `p`; backward reflects that membership through the isomorphism, restoring the inner membership along the term equalities.

```agda
            (snd (⟦ t ⟧ᵐ δ)) h)))
      (λ h → iso-bwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
        (snd (⟦ t ⟧ᵐ δ))
        (subst (λ z → ⟨ p (fst (⟦ t ⟧ᵐ δ)) ∈ˢ z ⟩) (sym (tm-agree u δ))
          (subst (λ z → ⟨ z ∈ˢ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) ⟩)
```

The backward direction closes the membership clause: reflection through the isomorphism, guided by the term congruences, returns exactly the inner membership. The equality atom and the witness principle are handled by the remaining hypotheses.

```agda
            (sym (tm-agree t δ)) h)))
```

Equality of atomic terms transfers by applying the collapse to both sides of the equation. The forward direction takes an equality of values in `M`, applies `p` via `cong`, and transports each side to its mapped term by the term congruences.

```agda
    at≐ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ (t ≐ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ≐ u))
    at≐ n t u δ = ⇔toPath
      (λ h → subst (λ z → z ≡ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ))) (tm-agree t δ)
        (subst (λ z → p (fst (⟦ t ⟧ᵐ δ)) ≡ z) (tm-agree u δ) (cong p h)))
```

The backward direction is where injectivity earns its place: the collapsed sides are equal, and `p-inj` recovers the equality of the original values from it. Together the two directions turn the equality atom into a path of propositions.

```agda
      (λ h → p-inj (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ)) (snd (⟦ t ⟧ᵐ δ))
        (snd (⟦ u ⟧ᵐ δ))
        (subst (λ z → z ≡ p (fst (⟦ u ⟧ᵐ δ))) (sym (tm-agree t δ))
          (subst (λ z → fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ≡ z)
            (sym (tm-agree u δ)) h)))
```

The witness principle is produced from surjectivity. An outer witness `p'` in the image is, merely, the collapse of some `q` in `M`; transporting the satisfaction along that identification returns the inner witness together with its satisfaction in the image.

```agda
    wit : Tr.Witness g
    wit n ψ δ h = PT.rec squash₁
      (λ { (p' , hp) → PT.map
        (λ { (q , gq≡p) →
          q , subst (λ z → ⟨ (z ∷ map g δ) ⊨ᵖᵐ mapFo g ψ ⟩) (sym gq≡p) hp })
```

The surjectivity lemma supplies the preimage, and the two transports compose into the witness principle of the transfer.

```agda
        (surj' p') }) h
```

With the atomic cases and witness principle in place, the shared induction proves that satisfaction is preserved when environments are mapped by the collapse and constants are relabelled by `g`.

```agda
  agree : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ φ) ≡ (map g δ ⊨ᵖᵐ mapFo g φ)
  agree = Tr.Along.agree g at∈ at≐ wit
```

The agreement is recorded in two one-directional forms for later composition. Forward, inner satisfaction yields satisfaction of the mapped formula at the mapped environment.

```agda
  iso-inv : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
          → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩
  iso-inv n φ δ = subst ⟨_⟩ (agree n φ δ)
```

Backward returns outer satisfaction to inner satisfaction. The chapter then instantiates this invariance at the collapse of a set `X` with extensionality, opening the collapse with its membership isomorphism and its injectivity.

```agda
  iso-inv-bwd : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
              → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
  iso-inv-bwd n φ δ = subst ⟨_⟩ (sym (agree n φ δ))
module CollapseIso (X : S) (Xext : isExt X) where
  module C = Collapse X using ( module InjExt; π; πX; πX-intro; πX-member )
```

Extensionality of `X` is exactly what the collapse needs: the restricted structure is injective, and the isomorphism between membership on `X` and membership on the collapse becomes available.

```agda
  module CI = C.InjExt Xext using ( iso; π-inj )
```

The target carrier is the collapse image `πX`; its points are precisely the collapse values of members of `X`.

```agda
  PM : S
  PM = C.πX
```

The map `p` sends each set to its Mostowski collapse value.

```agda
  p : S → S
  p = C.π
```

Members of `X` land in the image, by the collapse's own introduction rule for the image.

```agda
  p∈ : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ p x ∈ˢ PM ⟩
  p∈ = C.πX-intro
```

Membership is preserved forward along the collapse: if `y` is a member of `x` in `X`, then the collapse of `y` is a member of the collapse of `x`. This is the first component of the membership isomorphism.

```agda
  iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
          → ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩
  iso-fwd x y x∈ y∈ = CI.iso x y x∈ y∈ .fst
```

Membership reflects backward as well: a collapsed membership can only have arisen from a genuine membership in `X`. The two directions together say the collapse is faithful on membership.

```agda
  iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
          → ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩
  iso-bwd x y x∈ y∈ = CI.iso x y x∈ y∈ .snd
```

The collapse is injective on `X`: two members with equal collapses are equal. Faithfulness on membership plus injectivity are the two halves of the isomorphism on elements.

```agda
  p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
        → p x ≡ p y → x ≡ y
  p-inj = CI.π-inj
```

Every point of the image comes from a member of `X`: surjectivity is truncated, so it asserts the existence of a preimage without choosing one, which is exactly the form the witness principle consumes.

```agda
  surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
       → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (p y ≡ z)) ∥₁
  surj = C.πX-member
```

For the extensional set `X`, collapse preserves and reflects membership, is injective on `X`, and covers every point of `πX`.

```agda
  module I = IsoInv X PM p p∈ iso-fwd iso-bwd p-inj surj
    using ( SM; SPM; g; surj'; iso-inv; iso-inv-bwd; _⊨ᵐ_; _⊨ᵖᵐ_; ⟦_⟧ᵐ; ⟦_⟧ᵖᵐ )
```

## The Skolem hull is elementary

Hence satisfaction transfers in both directions between the structure on `X` and the structure on `πX`.

```agda
module HullElemDown (α : S) (ordα : IsOrd α)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩) (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
```

Applied to the Skolem hull inside `Lset α`, this reduces elementarity to the Tarski-Vaught witness condition.

```agda
  module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
  module H = ASt.Hull X X⊆L ∅∈α
    using ( module T; Hull⊆L; hull-member )
  M : S
  M = H.T.Hull
```

The substructure machinery is instantiated at the hull, and its formulas receive an ambient reading. Every element of the hull's carrier has a code: the code exists by truncated presentation, and the identification of value with inclusion is promoted by the propositionhood of stage membership.

```agda
  module A = ASt.AtM M H.Hull⊆L using ( Elementary; SM; module SemM; TV→elem; inL )
  module Mse = A.SemM.At A.SM id using ( _⊨_ )
  codeOf : (q : A.SM) → ∥ Σ[ c ∈ H.T.Code ] (H.T.val c ≡ A.inL q) ∥₁
  codeOf q = PT.map (λ { (c , e) → c , Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) e })
    (H.hull-member (fst q) (snd q))
```

Codes lift from single elements to finite environments: the empty environment is coded by the empty vector, and the recursive case pairs one new code with the codes already built.

```agda
  codeEnv : {n : ℕ} (δ : Vec A.SM n)
          → ∥ Σ[ ds ∈ Vec H.T.Code n ]
               (map H.T.val ds ≡ map A.inL δ) ∥₁
  codeEnv [] = ∣ [] , refl ∣₁
  codeEnv (q ∷ δ) = PT.map2
```

The cons case composes the two truncated existences into one: the extended vector of codes evaluates exactly to the included environment.

```agda
    (λ { (c , ec) (ds , eds) → c ∷ ds , cong₂ _∷_ ec eds })
    (codeOf q) (codeEnv δ)
```

Componentwise mapping also respects concatenation of finite environments. Thus the free-variable values and the values replacing constant occurrences can be combined into one coded environment for the Tarski-Vaught argument.

```agda
  inL-++ : {n m : ℕ} (δ : Vec A.SM n) (σ : Vec A.SM m)
          → map A.inL (δ ++ σ) ≡ map A.inL δ ++ map A.inL σ
  inL-++ [] σ = refl
  inL-++ (q ∷ δ) σ = cong (A.inL q ∷_) (inL-++ δ σ)
  tv : (n : ℕ) (ψ : Formula A.SM (suc n)) (δ : Vec A.SM n)
```

The statement is the Tarski-Vaught condition itself: if the stage satisfies an existential at the included environment, then, merely, some element of the hull satisfies the matrix there. The proof eliminates the coding of the environment and passes to the search closure.

```agda
     → ⟨ map A.inL δ ASt.AbsL.⊨ᵐ (mapFo A.inL (∃̇ ψ)) ⟩
     → ∥ Σ[ q ∈ A.SM ]
          ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩ ∥₁
  tv n ψ δ h = PT.rec squash₁ takeEnvironment (codeEnv params)
    where
```

Parameter abstraction replaces every constant occurrence by an additional free variable. The resulting formula has empty constant domain and arity increased by `countFo ψ`, while retaining the full logical structure of `ψ`.

```agda
    bodyFo : Formula (⊥* {ℓ}) (suc (n + countFo ψ))
    bodyFo = absFo ψ
```

The environment for the abstracted body is the old environment followed by the constant occurrences: the abstraction turns constants into extra free variables, so one vector carries everything the search needs.

```agda
    params : Vec A.SM (n + countFo ψ)
    params = δ ++ constantsFo ψ
```

Once this combined environment has codes, least-witness closure supplies a hull witness. The semantic identification between the abstracted formula and the original parameterized formula then yields the required Tarski-Vaught witness.

```agda
    takeEnvironment : Σ[ ds ∈ Vec H.T.Code (n + countFo ψ) ]
                        (map H.T.val ds ≡ map A.inL params)
                    → ∥ Σ[ q ∈ A.SM ]
                         ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
                             (mapFo A.inL ψ) ⟩ ∥₁
```

The search closure runs at the coded environment. Its own evaluation record is then combined with the coding equation and the distribution of the inclusion over concatenation, producing the evaluation of the codes as the included parameters.

```agda
    takeEnvironment (ds , eds) = PT.map finish (H.T.closed _ bodyFo ds witness)
      where
      vals-env : H.T.vals ds
               ≡ map A.inL δ ++ map A.inL (constantsFo ψ)
      vals-env = H.T.vals≡map ds ∙ eds ∙ inL-++ δ (constantsFo ψ)
```

The key identification states that the abstracted body, read in the bare search semantics at the coded environment, is the same proposition as the body read in the stage semantics at the included environment.

```agda
      body-path : (b : ASt.SL)
                → ((b ∷ H.T.vals ds) H.T.⊨₀ bodyFo)
                ≡ ((b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ mapFo A.inL ψ)
      body-path b =
          cong (λ ε → ε H.T.⊨₀ bodyFo) (cong (b ∷_) vals-env)
```

The path combines two semantic compatibility laws: `⊨-abs` relates parameter abstraction to the extended environment, and `⊨-map` relates relabelling to the mapped environment.

```agda
        ∙ sym (⊨-abs ASt.AbsL.𝒮M A.inL ψ
                 (b ∷ map A.inL δ))
        ∙ sym (⊨-map ASt.AbsL.𝒮M A.inL id ψ
                 (b ∷ map A.inL δ))
```

The stage's satisfaction of the existential is transported along the body path into the bare reading, producing exactly the satisfiability witness the search closure requires.

```agda
      witness : H.T.Sat (n + countFo ψ) bodyFo (H.T.vals ds)
      witness = PT.map (λ { (b , hb) →
        b , subst ⟨_⟩ (sym (body-path b)) hb }) h
```

The search returns a least witness inside the hull, satisfying the abstracted body at the coded environment. The conversion must turn this into the Tarski-Vaught pair for the original formula.

```agda
      finish : Σ[ a ∈ ASt.SL ]
                 ( ⟨ fst a ∈ˢ M ⟩
                 × ⟨ (a ∷ H.T.vals ds) H.T.⊨₀ bodyFo ⟩ )
             → Σ[ q ∈ A.SM ]
                 ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
```

The witness is read back into the carrier of the substructure: the underlying set is the hull, and the membership is the one just produced.

```agda
      finish (a , a∈H , ha) = q , sat
        where
        q : A.SM
        q = fst a , a∈H
```

The inclusion of the witness into the stage is the witness itself: the two carriers differ only by the proposition-valued membership proof, which is identified by reflexivity.

```agda
        q≡a : A.inL q ≡ a
        q≡a = Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) refl
```

The satisfaction of the body at the witness transports along the body path into the stage reading, and along the identification of the witness into the substructure's carrier; that is exactly the Tarski-Vaught conclusion for the original formula and environment.

```agda
        sat : ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
        sat = subst (λ b → ⟨ (b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
                                (mapFo A.inL ψ) ⟩)
                (sym q≡a) (subst ⟨_⟩ (body-path a) ha)
```

The Tarski-Vaught condition therefore yields elementarity of the hull in `Lset α`.

```agda
  elem : A.Elementary
  elem = A.TV→elem tv
```

## Reading parameter-free formulas in the ambient universe

For formulas with empty constant domain, ambient satisfaction can then be compared without any nontrivial relabelling of constants.

```agda
module AtP = SemV.At (⊥* {ℓ-suc ℓ}) (λ b → Empty.rec* b) using ( _⊨_ )
```

Ambient satisfaction for parameter-free formulas is named for reuse, and the key observation is stated: relabelling a parameter-free formula does not change it, since there are no constants to remap.

```agda
_⊨ₚ_ : {n : ℕ} → S ^ n → Formula (⊥* {ℓ-suc ℓ}) n → hProp (ℓ-suc ℓ)
_⊨ₚ_ = AtP._⊨_
embed-map : {ℓ₁ ℓ₂ : Level} {K : Type ℓ₁} {K' : Type ℓ₂} (f : K → K')
            {n : ℕ} (φ : Formula (⊥* {ℓ-suc ℓ}) n)
          → mapFo f (embed φ) ≡ embed φ
```

The proof composes the mapping law with the fact that the empty domain's embedding is the identity on occurrences: nothing is left for the relabelling to move.

```agda
embed-map f φ =
    mapFo-comp Empty.rec* f φ
  ∙ cong (λ h → mapFo h φ) (funExt (λ b → Empty.rec* b))
opaque
  isOrdAt : Formula (⊥* {ℓ-suc ℓ}) 1
```

Ordinality is expressed by a one-slot bounded formula saying that the parameter is transitive and that every member of it is transitive.

```agda
  isOrdAt =
    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
    ∧̇ (∀̇∈ (var zero) (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
```

The `Δ₀` certificate follows the outer conjunction, then the two bounded quantifiers of the first clause and the three bounded quantifiers of the second, ending at membership atoms.

```agda
  Δ₀-isOrdAt : Δ₀ isOrdAt
  Δ₀-isOrdAt =
    δ-∧ (δ-∀∈ (δ-∀∈ δ-∈))
        (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
```

The two reading lemmas identify satisfaction of `isOrdAt` exactly with the ordinal predicate, in both directions.

```agda
module Amb where
  opaque
    unfolding isOrdAt
```

Reading ordinality out of the formula unpacks the two bounded clauses into the two fields of the ordinal predicate: transitivity of the parameter, and transitivity of every member.

```agda
    isOrdAt-out : (x : S) → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩ → IsOrd x
    isOrdAt-out x h =
        ( λ {x₁} {y} y∈x₁ x₁∈x → h .fst x₁ x₁∈x y y∈x₁ )
      , ( λ a a∈x {x₁} {y} y∈x₁ x₁∈a → h .snd a a∈x x₁ x₁∈a y y∈x₁ )
```

Conversely, the two fields of `IsOrd` satisfy the two bounded clauses. The three-slot companion expresses the same predicate at the middle free slot; the other two free slots do not occur in the formula.

```agda
    isOrdAt-in : (x : S) → IsOrd x → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩
    isOrdAt-in x o =
        ( λ a a∈x b hb → o .fst {a} {b} hb a∈x )
      , ( λ a a∈x b b∈a c hc → o .snd a a∈x {b} {c} hc b∈a )
isOrd-at-p : Formula (⊥* {ℓ-suc ℓ}) 3
```

The three-slot formula's first conjunct says that every member of a member of the parameter is a member of the parameter: transitivity, read at the second slot.

```agda
isOrd-at-p =
    (∀̇∈ (var (suc zero))
      (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc (suc zero))))))
  ∧̇ (∀̇∈ (var (suc zero))
      (∀̇∈ (var zero)
```

The second conjunct says that each member `a` of the parameter is transitive: whenever `c ∈ b ∈ a`, one has `c ∈ a`.

```agda
        (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
```

Its boundedness certificate follows the same recursion. The erasure lemma then begins: for a formula with no constant occurrences, erasing the constants preserves the Δ₀ certificate, clause by clause.

```agda
Δ₀-isOrd-at-p : Δ₀ isOrd-at-p
Δ₀-isOrd-at-p = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
erase-Δ₀ : {m : ℕ} (φ : Formula CS.S m) (p : countFo φ ≡ 0)
         → Δ₀ φ → Δ₀ (Cnt.erase φ p)
erase-Δ₀ (t ∈̇ u) p δ-∈ = δ-∈
```

Atoms pass through unchanged, and the propositional connectives recurse, since erasure is applied structurally.

```agda
erase-Δ₀ (t ≐ u) p δ-≐ = δ-≐
erase-Δ₀ (φ ∧̇ ψ) p (δ-∧ c d) = δ-∧ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ∨̇ ψ) p (δ-∨ c d) = δ-∨ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ⇒̇ ψ) p (δ-⇒ c d) = δ-⇒ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ ⊥̇ p δ-⊥ = δ-⊥
```

The bounded-quantifier cases recurse on their matrices.

```agda
erase-Δ₀ (∀̇∈ t φ) p (δ-∀∈ c) = δ-∀∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇∈ t φ) p (δ-∃∈ c) = δ-∃∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇ φ) p ()
erase-Δ₀ (∀̇ φ) p ()
```

## The hull data required by condensation

The unbounded quantifier cases are impossible because no `Δ₀` certificate has such a constructor.

```agda
module HullStage (lam : S) (ordλ : IsOrd lam)
```

The frame receives a stage whose index admits successors of its members, a starting set contained in that stage, and the empty set's membership in the index.

```agda
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩) (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
```

Inside `Lset lam`, the starting set generates a Skolem hull `M`. Every element of `M` remains in the stage.

```agda
  module ASt = AtStage lam ordλ
    using ( module AbsL; module AtM; module Hull; Ltr; SL; wL )
```

The original set and the empty-set fallback are both represented in the hull construction.

```agda
  module H = ASt.Hull X X⊆L ∅∈λ
    using ( module T; module XInM; Hull⊆L; X⊆M; hull-member
          ; val-in-Hull; ∅∈Lsetα; inStg )
```

This set `M` is the carrier whose elementarity and Mostowski collapse enter the condensation argument.

```agda
  M : S
  M = H.T.Hull
```

For the hull `M`, let `π` be its Mostowski collapse and `πX` its image. Every collapsed hull point belongs to `πX`, every member of `πX` comes from a hull point, and `πX` is transitive. Moreover, the collapse fixes any transitive point of the hull.

```agda
  module C = Collapse M
    using ( module InjExt; π; πX; πX-intro; πX-member; πX-trans; fixes )
```

The condensation argument assumes two properties of the image. First, if an ordinal `δ` belongs to the image, then so does the level `Lset δ`. Second, the collapse of every hull member belongs to some level whose ordinal index lies in the image. These closure and covering properties will identify the image with a single level of `L`.

```agda
  module Condense
    (levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ C.πX ⟩ → ⟨ Lset δ ∈ˢ C.πX ⟩)
    (cover : (y : S) → ⟨ y ∈ˢ M ⟩
           → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ C.π y ∈ˢ Lset γ ⟩) ∥₁)
    where
```

Separation forms the set of exactly those members of `πX` that are ordinals. Thus `β` records the ordinal part of the collapse image. The separating predicate is the bounded ordinality formula, small at every environment by its Δ₀ certificate.

```agda
    β-sep : Σ[ s ∈ S ]
              (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt)))
    β-sep = separateFromSmall C.πX (λ y → (y ∷ []) ⊨ₚ isOrdAt)
              (λ y → D0.Δ₀-small Δ₀-isOrdAt (y ∷ []))
```

We call this ordinal part `β`; the following argument proves that it is itself an ordinal and that its level is exactly the collapse image.

```agda
    β : S
    β = β-sep .fst
```

Membership in `β` is equivalent to membership in `πX` together with satisfaction of the constant-free ordinal formula when its free variable is assigned the member.

```agda
    β-spec : (y : S) → (y ∈ˢ β) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt))
    β-spec = β-sep .snd
```

The first projection of the equivalence shows every member of beta is a member of the collapse image.

```agda
    β∈πX : (δ : S) → ⟨ δ ∈ˢ β ⟩ → ⟨ δ ∈ˢ C.πX ⟩
    β∈πX δ δ∈β = subst ⟨_⟩ (β-spec δ) δ∈β .fst
```

The second component converts satisfaction of this constant-free one-variable formula into ambient ordinality.

```agda
    β-ord : (δ : S) → ⟨ δ ∈ˢ β ⟩ → IsOrd δ
    β-ord δ δ∈β = Amb.isOrdAt-out δ (subst ⟨_⟩ (β-spec δ) δ∈β .snd)
```

Conversely, an ordinal of the collapse image lies in beta: both defining components are supplied, membership and ordinality, and the defining equivalence transports them back inside.

```agda
    ord∈β : (δ : S) → ⟨ δ ∈ˢ C.πX ⟩ → IsOrd δ → ⟨ δ ∈ˢ β ⟩
    ord∈β δ δ∈πX oδ = subst ⟨_⟩ (sym (β-spec δ)) (δ∈πX , Amb.isOrdAt-in δ oδ)
```

To prove that `β` is an ordinal, we verify its two defining requirements. The first is transitivity: whenever `z ∈ x ∈ β`, we must have `z ∈ β`.

```agda
    β-isOrd : IsOrd β
    β-isOrd = β-trans , β-mem
      where
      β-trans : isTransV β
      β-trans {x = x} {y = z} z∈x x∈β =
```

Transitivity uses the transitivity of the collapse image at the intermediate membership and reads the ordinality of the middle point from the ambient formula. The second field follows because every member of beta is an ordinal, hence transitive.

```agda
        subst ⟨_⟩ (sym (β-spec z))
          ( C.πX-trans {x = x} {y = z} z∈x (β∈πX x x∈β)
          , Amb.isOrdAt-in z (mem-ord {A = x} (β-ord x x∈β) z z∈x) )
      β-mem : (x : S) → ⟨ x ∈ˢ β ⟩ → isTransV x
      β-mem x x∈β = β-ord x x∈β .fst
```

The covering hypothesis lifts from hull members to collapse members. Since a collapse member is, merely, the collapse of a hull member, the cover of that hull member transports along the identification.

```agda
    covered : (x : S) → ⟨ x ∈ˢ C.πX ⟩
            → ∥ Σ[ γ ∈ S ]
                 (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
    covered x x∈πX = PT.rec squash₁ go (C.πX-member x x∈πX)
      where
```

The inversion is the collapse's own member description: a member of the image is, merely, the collapse of a hull member.

```agda
      go : Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (C.π y ≡ x))
         → ∥ Σ[ γ ∈ S ]
              (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
      go (y , y∈M , e) = PT.map
        (λ { (γ , oγ , γ∈πX , h) →
```

The cover transports along the equality of the collapse values. The lifted statement is then applied immediately: every ordinal of beta sits inside a larger ordinal of beta, the classical limit-stage step of the condensation argument.

```agda
          γ , oγ , γ∈πX , subst (λ w → ⟨ w ∈ˢ Lset γ ⟩) e h })
        (cover y y∈M)
    β-succ : (δ : S) → ⟨ δ ∈ˢ β ⟩
           → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩) ∥₁
    β-succ δ δ∈β = PT.map go (covered δ (β∈πX δ δ∈β))
```

The ordinality of delta is read off beta, and the conversion restates the covering conclusion in membership form: the level containing delta can be chosen to have its index inside beta.

```agda
      where
      oδ : IsOrd δ
      oδ = β-ord δ δ∈β
      go : Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ δ ∈ˢ Lset γ ⟩)
         → Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
```

Because both `δ` and `γ` are ordinals, `δ ∈ Lset γ` implies `δ ∈ γ`; and because `γ` is an ordinal in `πX`, it belongs to `β`. The reverse inclusion is then stated: every member of the collapse lies in the level at beta.

```agda
      go (γ , oγ , γ∈πX , δ∈Lγ) =
        γ , oγ , ord∈Lset→∈ γ oγ δ oδ δ∈Lγ , ord∈β γ γ∈πX oγ
    πX⊆Lβ : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ x ∈ˢ Lset β ⟩
    πX⊆Lβ x x∈πX = PT.rec (snd (x ∈ˢ Lset β)) go (covered x x∈πX)
      where
```

The reverse inclusion holds because the level at beta contains every smaller level: monotonicity of the stage construction transports the covering level inside beta.

```agda
      go : Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩)
         → ⟨ x ∈ˢ Lset β ⟩
      go (γ , oγ , γ∈πX , x∈Lγ) =
        Lset-mono {α = β} {β = γ} (ord∈β γ γ∈πX oγ) x∈Lγ
    Lβ⊆πX : (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ C.πX ⟩
```

The forward inclusion decomposes a member of the level at beta by the stage construction, and the limit step supplies a larger ordinal inside beta.

```agda
    Lβ⊆πX x x∈Lβ = PT.rec (snd (x ∈ˢ C.πX)) go (Lset-out β x x∈Lβ)
      where
      go : Σ[ δ ∈ S ] (⟨ δ ∈ˢ β ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
         → ⟨ x ∈ˢ C.πX ⟩
      go (δ , δ∈β , x∈𝒟ₒδ) = PT.rec (snd (x ∈ˢ C.πX)) liftStage (β-succ δ δ∈β)
```

The lifting stage is stated: from an ordinal inside beta containing delta, produce the membership of `x` in the collapse.

```agda
        where
        liftStage : Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
             → ⟨ x ∈ˢ C.πX ⟩
        liftStage (γ , oγ , δ∈γ , γ∈β) =
          C.πX-trans {x = Lset γ} {y = x}
```

The lifting composes two closures: the level at gamma contains x because x is defined at delta below gamma, and the collapse image contains the level at gamma by the first hypothesis. The two inclusions then meet in the extensionality of the universe.

```agda
            (Lset-in γ δ x δ∈γ x∈𝒟ₒδ)
            (levelIn γ oγ (β∈πX γ γ∈β))
    ext : C.πX ≡ Lset β
    ext = extensionality C.πX (Lset β) (sub , sup)
      where
```

The first half of the extensionality argument moves each member through the bridge into the stage reading, applies the reverse inclusion, and returns through the bridge.

```agda
      sub : (x : S) → ⟨ x ∈ₛ C.πX ⟩ → ⟨ x ∈ₛ Lset β ⟩
      sub x x∈ₛπX = ∈∈ₛ {a = x} {b = Lset β} .fst
        (πX⊆Lβ x (∈∈ₛ {a = x} {b = C.πX} .snd x∈ₛπX))
      sup : (x : S) → ⟨ x ∈ₛ Lset β ⟩ → ⟨ x ∈ₛ C.πX ⟩
      sup x x∈ₛLβ = ∈∈ₛ {a = x} {b = C.πX} .fst
```

The second half does the same for the forward inclusion, and the two halves identify the collapse image with the level at beta.

```agda
        (Lβ⊆πX x (∈∈ₛ {a = x} {b = Lset β} .snd x∈ₛLβ))
```

The condensation statement is thus assembled: the collapse image is the level at its ordinal `β`. For the applications, take as a starting set the union of a stage `Lset α` with one extra point `x`, where `α ∈ lam`, `x ⊆ Lset α`, and `x ∈ Lset lam`.

```agda
    condenses : Σ[ γ ∈ S ] (IsOrd γ × (C.πX ≡ Lset γ))
    condenses = β , β-isOrd , ext
module UnionKit (α lam x : S) (ordα : IsOrd α) (ordλ : IsOrd lam)
  (α∈λ : ⟨ α ∈ˢ lam ⟩) (x⊆Lα : (z : S) → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ Lset α ⟩)
  (x∈Lλ : ⟨ x ∈ˢ Lset lam ⟩) (α∉ω : ⟨ α ∈ˢ ω ⟩ → Empty.⊥) where
```

The starting set is the union of `Lset α` and the singleton `{x}`; singleton classification gives `x ∈ {x}`.

```agda
  X : S
  X = Lset α ∪ ⁅ x ⁆s
  x∈sgl : ⟨ x ∈ₛ ⁅ x ⁆s ⟩
  x∈sgl = SetPackage.classification (SingletonPackage x) x .snd refl
```

The extra point belongs to the starting set through the right side of the union.

```agda
  x∈X : ⟨ x ∈ˢ X ⟩
  x∈X = cup-inr (Lset α) ⁅ x ⁆s x (∈∈ₛ {a = x} {b = ⁅ x ⁆s} .snd x∈sgl)
```

Every member of the stage belongs to the starting set through the left side.

```agda
  Lα∈X : (z : S) → ⟨ z ∈ˢ Lset α ⟩ → ⟨ z ∈ˢ X ⟩
  Lα∈X = cup-inl (Lset α) ⁅ x ⁆s
```

The singleton characterization says that every member of `{x}` is equal to `x`.

```agda
  sgl≡ : (z : S) → ⟨ z ∈ˢ ⁅ x ⁆s ⟩ → z ≡ x
  sgl≡ = sgl-out x
```

Consequently, membership in the starting set splits into two cases: a point belongs either to `Lset α` or to the singleton `{x}`.

```agda
  X-mem : (z : S) → ⟨ z ∈ˢ X ⟩
        → ⟨ (z ∈ˢ Lset α) ⊔ (z ∈ˢ ⁅ x ⁆s) ⟩
  X-mem = cup-out (Lset α) ⁅ x ⁆s
```

The generator is contained in the ambient stage: a member on the stage side is transported by the monotonicity of the stage construction along the index inclusion.

```agda
  X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z z∈X = PT.rec (snd (z ∈ˢ Lset lam)) go (X-mem z z∈X)
    where
    go : (⟨ z ∈ˢ Lset α ⟩ ⊎ ⟨ z ∈ˢ ⁅ x ⁆s ⟩) → ⟨ z ∈ˢ Lset lam ⟩
    go (inl z∈Lα) = Lset-mono {α = lam} {β = α} α∈λ z∈Lα
```

A member on the singleton side reduces to the extra point, whose stage membership was a hypothesis.

```agda
    go (inr z∈sgl) = subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym (sgl≡ z z∈sgl)) x∈Lλ
```

The generator is transitive. A member of a member on the stage side is in the stage by the layer's transitivity, and the left inclusion then places it in the generator.

```agda
  Xtr : isTransV X
  Xtr {x = a} {y = b} b∈a a∈X = PT.rec (snd (b ∈ˢ X)) go (X-mem a a∈X)
    where
    go : (⟨ a ∈ˢ Lset α ⟩ ⊎ ⟨ a ∈ˢ ⁅ x ⁆s ⟩) → ⟨ b ∈ˢ X ⟩
    go (inl a∈Lα) = Lα∈X b (layer-trans (Lset-layer α) b∈a a∈Lα)
```

On the singleton side, the intermediate set is `x`; the hypothesis `x ⊆ Lset α` then places each of its members in the left side of the union.

```agda
    go (inr a∈sgl) = Lα∈X b (x⊆Lα b
      (subst (λ u → ⟨ b ∈ˢ u ⟩) (sgl≡ a a∈sgl) b∈a))
  one∈α : ⟨ sucV ∅ ∈ˢ α ⟩
  one∈α = Sum.rec
      (λ α∈ω → Empty.rec (α∉ω α∈ω))
```

Infinity means not belonging to `ω`, and the trichotomy of ordinals decides the cases: membership in `ω` contradicts the hypothesis, equality with `ω` is witnessed by the numeral one, and `ω` below `α` places the numeral one inside `α` by transitivity.

```agda
      (Sum.rec (λ α≡ω → subst (λ w → ⟨ sucV ∅ ∈ˢ w ⟩) (sym α≡ω) (#∈ω 1))
               (λ ω∈α → ordα .fst (#∈ω 1) ω∈α))
      (ord-tri α ordα ω ω-ord)
```

The empty set appears at the first successor stage, by the base-layer coding transported along the description of the successor stage.

```agda
  ∅∈Lset1 : ⟨ ∅ ∈ˢ Lset (sucV ∅) ⟩
  ∅∈Lset1 = subst (λ w → ⟨ ∅ ∈ˢ w ⟩) (sym (Lset-suc ∅)) (∅∈𝒟ₒ ∅)
```

Monotonicity lifts the empty set first into `Lset α` and then into `Lset lam`.

```agda
  ∅∈Lλ : ⟨ ∅ ∈ˢ Lset lam ⟩
  ∅∈Lλ = Lset-mono {α = lam} {β = α} α∈λ
    (Lset-mono {α = α} {β = sucV ∅} one∈α ∅∈Lset1)
```

The rank characterization then promotes this to membership of the empty set in the index `lam` itself. It remains to prove that the hull is extensional, which is the final condition needed to make its collapse injective.

```agda
  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = subst (λ w → ⟨ w ∈ˢ lam ⟩) (rank-fix ∅ ∅-ord)
    (rank-Lset lam ordλ ∅ ∅∈Lλ)
module HullExt (α : S) (ordα : IsOrd α)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
```

The empty-set membership assumption ensures that the Skolem hull at `Lset α` has the default value required by its term algebra.

```agda
  (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
```

Let `M` be the Skolem hull of `X` inside `Lset α`. Its inclusion into the stage is elementary. We compare formulas in the hull with their interpretations in the stage in order to prove that membership restricted to `M` is extensional.

```agda
  module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
  module H = ASt.Hull X X⊆L ∅∈α using ( module T; Hull⊆L )
  module A = ASt.AtM H.T.Hull H.Hull⊆L using ( SM; inL; module SemM )
  module E = HullElemDown α ordα X X⊆L ∅∈α using ( elem )
  module Mse = A.SemM.At A.SM id using ( _⊨_ )
```

The hull is named, and the symmetric difference of two sets is stated at the level of membership truths: a point lies in one side and provably not in the other.

```agda
  M : S
  M = H.T.Hull
  Different : S → S → S → Type (ℓ-suc ℓ)
  Different x y z = (z ∈ᵗ x × (z ∈ᵗ y → Empty.⊥))
                  ⊎ (z ∈ᵗ y × (z ∈ᵗ x → Empty.⊥))
```

Unequal sets have a point in their symmetric difference, classically: the truncated existence is decided by excluded middle.

```agda
  different : (x y : S) → (x ≡ y → Empty.⊥) → ∥ Σ[ z ∈ S ] Different x y z ∥₁
  different x y nxy = go (lem P)
    where
    P : hProp (ℓ-suc ℓ)
    P = ∥ Σ[ z ∈ S ] Different x y z ∥₁ , squash₁
```

If no point separated the sets, every membership truth would agree in both directions, and the universe's extensionality would force equality, contradicting the assumption.

```agda
    go : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → ⟨ P ⟩
    go (inl p) = p
    go (inr np) = Empty.rec (nxy (extensionalV (λ z → ⇔toPath (fwd z) (bwd z))))
      where
      fwd : (z : S) → z ∈ᵗ x → z ∈ᵗ y
```

Both directions of the agreement are decided by excluded middle, and each failing direction contributes its point to the symmetric difference.

```agda
      fwd z zx = Sum.rec (λ zy → zy)
        (λ nzy → Empty.rec (np ∣ z , inl (zx , nzy) ∣₁)) (lem (z ∈ˢ y))
      bwd : (z : S) → z ∈ᵗ y → z ∈ᵗ x
      bwd z zy = Sum.rec (λ zx → zx)
        (λ nzx → Empty.rec (np ∣ z , inr (zy , nzx) ∣₁)) (lem (z ∈ˢ x))
```

The difference formula is the disjunction `(z ∈ x ∧ z ∉ y) ∨ (z ∈ y ∧ z ∉ x)`, with the two hull members occupying its constant slots.

```agda
  φ : A.SM → A.SM → Formula A.SM 1
  φ x y = ((var zero ∈̇ con x) ∧̇ (¬̇ (var zero ∈̇ con y)))
        ∨̇ ((var zero ∈̇ con y) ∧̇ (¬̇ (var zero ∈̇ con x)))
  outer : (u v : S) (u∈M : u ∈ᵗ M) (v∈M : v ∈ᵗ M)
        → (z : S) → Different u v z
```

Existential satisfaction is truncated, so the distinguishing point is returned under truncation. In either branch of the symmetric difference, the same point witnesses the corresponding disjunct of the formula in the stage.

```agda
        → ∥ Σ[ a ∈ ASt.SL ]
            ⟨ (a ∷ []) ASt.AbsL.⊨ᵐ (mapFo A.inL (φ (u , u∈M) (v , v∈M))) ⟩ ∥₁
  outer u v u∈M v∈M z d = ∣ a , ∣ objectDifferent d ∣₁ ∣₁
    where
    objectDifferent = Sum.map
```

In either branch, ambient membership supplies the positive conjunct, while the nonmembership proof is lifted to the negation required by formula semantics. Transitivity of the stage places the distinguishing point in its carrier.

```agda
      (λ (zu , nzv) → zu , λ zv → lift (nzv zv))
      (λ (zv , nzu) → zv , λ zu → lift (nzu zu))
    z∈L : ⟨ z ∈ˢ Lset α ⟩
    z∈L = Sum.rec
      (λ (zx , _) → layer-trans (Lset-layer α) zx (H.Hull⊆L u u∈M))
```

Pairing the distinguishing point with its stage membership makes it a witness in the stage carrier. To prove hull extensionality, assume first that every hull element belonging to `x` also belongs to `y`.

```agda
      (λ (zv , _) → layer-trans (Lset-layer α) zv (H.Hull⊆L v v∈M)) d
    a : ASt.SL
    a = z , z∈L
  refute : (x y : S) (x∈M : x ∈ᵗ M) (y∈M : y ∈ᵗ M)
         → (ag1 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩)
```

Assume conversely that every hull element belonging to `y` also belongs to `x`. If `x` and `y` were nevertheless unequal, a point in their symmetric difference would lead to a contradiction.

```agda
         → (ag2 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩)
         → (x ≡ y → Empty.⊥) → Empty.⊥
  refute x y x∈M y∈M ag1 ag2 nxy = PT.rec Empty.isProp⊥ diff (different x y nxy)
    where
    xS : A.SM
```

The two hull members are read as elements of the substructure carrier, ready to be plugged into the difference formula.

```agda
    xS = x , x∈M
    yS : A.SM
    yS = y , y∈M
```

The refutation eliminates the difference point. Elementarity converts the stage's satisfaction of the existential formula, with the difference point as witness, into satisfaction of the same existential inside the hull.

```agda
    diff : Σ[ z ∈ S ] Different x y z → Empty.⊥
    diff (z , d) = PT.rec Empty.isProp⊥ inside h
      where
      h : ⟨ [] Mse.⊨ (∃̇ (φ xS yS)) ⟩
      h = subst ⟨_⟩ (sym (E.elem 0 (∃̇ (φ xS yS)) []))
```

Elementarity supplies a hull witness satisfying the difference formula. Eliminating its truncated disjunction reveals which of the two asymmetric membership statements holds.

```agda
        (outer x y x∈M y∈M z d)
      inside : Σ[ b ∈ A.SM ] ⟨ (b ∷ []) Mse.⊨ φ xS yS ⟩ → Empty.⊥
      inside (b , q) = PT.rec Empty.isProp⊥ cases q
        where
        cases : (⟨ fst b ∈ˢ x ⟩ × (⟨ fst b ∈ˢ y ⟩ → Lift Empty.⊥))
```

Either disjunct identifies the witness as a member of one hull member but not the other, and the corresponding agreement hypothesis contradicts the negation. This contradiction is exactly what extensionality of the hull requires.

```agda
              ⊎ (⟨ fst b ∈ˢ y ⟩ × (⟨ fst b ∈ˢ x ⟩ → Lift Empty.⊥))
              → Empty.⊥
        cases (inl (bx , nby)) = lower (nby (ag1 (fst b) (snd b) bx))
        cases (inr (by , nbx)) = lower (nbx (ag2 (fst b) (snd b) by))
```

Extensionality of the hull is proved by classical contradiction. Since the universe of sets is an h-set, `x ≡ y` is a proposition, so excluded middle gives either an equality or a refutation of equality. In the second case, `refute` turns `x ≢ y` into a hull member belonging to exactly one of `x` and `y`, contradicting the two membership-agreement hypotheses; hence `x ≡ y`.

```agda
  hullExt : isExt M
  hullExt x y x∈M y∈M ag1 ag2 =
    Sum.rec (λ p → p) (λ np → Empty.rec (bad np))
      (lem ((x ≡ y) , isSetS x y))
    where
```

The contradictory branch is eliminated by `bad`, completing extensionality of the hull.

```agda
    bad : (x ≡ y → Empty.⊥) → Empty.⊥
    bad = refute x y x∈M y∈M ag1 ag2
```

## Carrying bounded formulas across the collapse

To compare the collapse with the ambient universe, now fix a transitive set `U`. A constant-free Δ₀ formula evaluated at members of `U` has the same truth value in the restricted structure on `U` as in the ambient structure.

```agda
module Unpack (U : S) (Utr : isTrans U) where
```

An element of the restricted carrier `SM` is a set together with evidence that it belongs to `U`. Projecting each such pair to its first component gives the corresponding ambient environment, and bounded absoluteness `abs₀` compares satisfaction before and after this projection.

```agda
  module Ab = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ U) Utr using (SM; abs₀; _⊨ᵐ_)
```

For a constant-free Δ₀ formula `φ`, `read` first regards `embed φ` as a formula over the restricted carrier. Bounded absoluteness compares its restricted and ambient readings; `embed-⊨` removes the induced relabelling, and uniqueness of a function from the empty constant domain identifies the remaining constant interpretations.

```agda
  read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Ab.SM ^ n)
       → (δ Ab.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
  read {n} {φ} dφ δ =
      Ab.abs₀ (mapΔ₀ Empty.rec* dφ) δ
    ∙ embed-⊨ 𝒮ᵥ {K = Ab.SM} fst φ (map fst δ)
```

The final path uses function extensionality: because the constant domain is empty, its two interpretations agree pointwise and hence are equal. We then fix the data for a hull inside `Lset lam`: an ordinal `lam` closed under successors and a starting set `X ⊆ Lset lam`.

```agda
    ∙ cong (λ ι → SemV.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ)
           (funExt (λ b → Empty.rec* b))
module Frame (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
```

We also assume `∅ ∈ lam`, the base-stage hypothesis used by the hull construction.

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
```

Let `M` be the hull of `X` inside `Lset lam`. We use its inclusion into the stage, the resulting notion of elementarity, and the extensionality proved above.

```agda
  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using (module ASt; module C; module Condense; module H; M)
  module ASt = HS.ASt using (module AbsL; module AtM; Ltr; SL)
  module A = ASt.AtM HS.M HS.H.Hull⊆L using (Elementary; SM; module SemM; inL)
  module HE = HullExt lam ordλ X X⊆Lλ ∅∈λ using (hullExt)
```

Thus `M` is extensional. This is the hypothesis needed to identify `M` with its transitive Mostowski collapse.

```agda
  Mext : isExt HS.M
  Mext = HE.hullExt
```

The carry argument takes explicitly the elementarity of the inclusion `M → Lset lam`. Together with extensionality of `M`, this supplies the two comparisons used below: from the hull to the stage and from the hull to its collapse.

```agda
  module Carry (elem : A.Elementary) where
```

The comparison now involves three structures: the hull `M`, the stage `Lset lam`, and the transitive collapse image `πX`. The collapse isomorphism relates the first and third, while bounded absoluteness relates each transitive set to the ambient universe.

```agda
    module CIso = CollapseIso HS.M Mext using (module I; iso-fwd; iso-bwd)
    module TL = Unpack (Lset lam) ASt.Ltr using (read)
    module Tπ = Unpack HS.C.πX HS.C.πX-trans using (module Ab; read)
```

Membership is preserved by the collapse directly: the forward direction of the membership isomorphism is exactly the push needed for atomic membership.

```agda
    member-push : (x y : S) → ⟨ x ∈ˢ HS.M ⟩ → ⟨ y ∈ˢ HS.M ⟩
                → ⟨ y ∈ˢ x ⟩ → ⟨ HS.C.π y ∈ˢ HS.C.π x ⟩
    member-push = CIso.iso-fwd
```

Because `Lset lam` is transitive, every constant-free Δ₀ formula has equal restricted and ambient readings there; `atL` is `read` specialized to this stage.

```agda
    atL : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : ASt.SL ^ n)
        → (δ ASt.AbsL.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atL dφ δ = TL.read dφ δ
```

The collapse image `πX` is also transitive, so the same agreement holds there for constant-free Δ₀ formulas.

```agda
    atπ : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Tπ.Ab.SM ^ n)
        → (δ Tπ.Ab.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atπ dφ δ = Tπ.read dφ δ
```

For the hull's own carrier, the reading factors through elementarity: the embedded formula is first read internally, the relabelling is fixed because the formula carries no constants, and the result is transported to the stage reading.

```agda
    atM : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
        → (δ CIso.I.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atM {n} {φ} dφ δ =
        elem n (embed φ) δ
      ∙ cong (λ ψ → map A.inL δ ASt.AbsL.⊨ᵐ ψ) (embed-map A.inL φ)
```

After stage absoluteness, only the environments must be compared. Including a hull member into `Lset lam` does not change its underlying set, so projecting the included environment gives the same vector of ambient sets as projecting the original environment.

```agda
      ∙ atL dφ (map A.inL δ)
      ∙ cong (λ γ → γ ⊨ₚ φ) (map-inL-fst δ)
      where
      map-inL-fst : {m : ℕ} (γ : A.SM ^ m)
                  → map fst (map A.inL γ) ≡ map fst γ
```

This equality is immediate for the empty environment and is preserved when one entry is prepended. Hence, for a constant-free Δ₀ formula, ambient truth at an environment of hull members implies ambient truth at the environment of their collapse values.

```agda
      map-inL-fst [] = refl
      map-inL-fst (q ∷ γ) = cong (fst q ∷_) (map-inL-fst γ)
    push : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
         → ⟨ map fst δ ⊨ₚ φ ⟩
         → ⟨ map fst (map CIso.I.g δ) ⊨ₚ φ ⟩
```

Starting from ambient truth at the hull environment, `atM` is used backward to obtain internal truth in the hull. `iso-inv` carries that truth to the collapse image, `embed-map` removes the vacuous relabelling of constants, and `atπ` is used forward to return to ambient truth at the collapse values.

```agda
    push {n} {φ} dφ δ h =
      subst ⟨_⟩ (atπ dφ (map CIso.I.g δ))
        (subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
               (embed-map CIso.I.g φ)
               (CIso.I.iso-inv n (embed φ) δ (subst ⟨_⟩ (sym (atM dφ δ)) h)))
```

For `pull`, ambient truth at the collapse values is moved backward along `atπ` into the collapse image. After `embed-map` restores the relabelled form, `iso-inv-bwd` returns to internal truth in the hull, and `atM` is used forward to recover ambient truth at the original hull environment.

```agda
    pull : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
         → ⟨ map fst (map CIso.I.g δ) ⊨ₚ φ ⟩
         → ⟨ map fst δ ⊨ₚ φ ⟩
    pull {n} {φ} dφ δ h =
      subst ⟨_⟩ (atM dφ δ)
```

Together, `push` and `pull` show that for every constant-free Δ₀ formula and every finite environment of hull members, ambient satisfaction is unchanged when each entry is replaced by its collapse value. The separate lemma `member-push` gives the corresponding direct preservation statement for membership.

```agda
        (CIso.I.iso-inv-bwd n (embed φ) δ
          (subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
                 (sym (embed-map CIso.I.g φ))
                 (subst ⟨_⟩ (sym (atπ dφ (map CIso.I.g δ))) h)))
```