---
title: "Locating the hull and its collapse inside L"
module: L.GCH.ConstructibleHull
lang: en
site: "Bedrock"
description: "Locating the hull and its collapse inside L"
stage: "Proving GCH"
reading_order: 116
canonical: https://bedrock.institute/en/L.GCH.ConstructibleHull.html
html: L.GCH.ConstructibleHull.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/ConstructibleHull.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.Renaming, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Presentation, V.Coding, V.Collapse, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Infinity, L.Axioms.Numerals, L.Recursion, L.Recursion.Graph, L.Definability, L.Coding.Model, L.Coding.Expressions, L.Coding.Environment, L.Coding.EnvironmentSet, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.CodeConstructibility, L.Coding.UniformSatisfaction, L.Choice.CanonicalNames, L.Choice.NameComparison, L.Choice.InternalWellOrder, L.Choice.StageOrders, L.WellOrder.Base, L.GCH.CardinalSquareLaw, L.GCH.OrderType, L.GCH.OmegaRecursion, L.GCH.SkolemHull, L.InjectionComposition, L.GCH.AdequateStages, L.Coding.SatisfactionGraphSet, L.GCH.CondensationTransfer, V.Model]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.ConstructibleHull.md, https://bedrock.institute/ja/L.GCH.ConstructibleHull.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Locating the hull and its collapse inside L

The condensation argument needs more than an external hull: the hull itself and every value of its collapse must belong to L. This chapter proves these membership facts by coding the collapse and expressing the hull as an ω-iteration.

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

The chapter runs under classical logic: an excluded-middle instance at the successor of the model's own level. This is the same hypothesis the choice construction carries, and it is the only classical assumption made here.

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

The module is parameterized by that hypothesis, so every statement below is relative to it rather than to an ambient principle of excluded middle.

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

The chapter speaks the first-order language of set theory: formulas are built over the carrier of the constructible structure, their constants name elements of `L`, and constants can be relabeled along any map, with satisfaction invariant under such relabeling. This is the vocabulary in which the collapse and the hull will be described.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ⊥̇ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
```

Formula readings move between environments by renaming, and renaming is harmless for satisfaction. The ambient hierarchy contributes the background facts: induction along membership, extensionality of sets, and the presentation of an element as an index together with its membership proof.

```agda
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Presentation {ℓ} using ( member; fiber )
```

The argument begins where every set of `L` lives: in the tower of stages indexed by ordinals. The collapse of a set is computed from its members alone, and constructibility travels along membership; what must be shown is that this local computation never leaves `L`. Since a hull is not transitive, the argument cannot invoke global facts about the collapse; it re-derives, stage by stage, that the values stay inside.

```agda
open import V.Coding {ℓ} using ( pr; module VCode )
open import V.Collapse {ℓ} using ( module Collapse )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-out; Lset→isL; 𝒟ₒ; 𝒟ₒ∋⊆
        ; Lset-layer; layer-trans )
```

The constructible set `ωʟ` represents the ambient `ω`, and its specification identifies its members with the internal numerals. Separation will carve the bounded slices and one-step closures used later. In both operations the result is an element of `L` again, which is what keeps the whole construction inside the universe it describes.

```agda
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )
```

Replacement assembles values into tables: a recursion whose graph is definable becomes an element of `L`, and it suffices that a unique value merely exists at each argument. Definability interprets the constants of formulas, and the model-side coding of pairs and numerals provides the entries and their names.

```agda
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to RecursionGraph )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate; consAtL; consAtL-adequate )
```

Environments code parameter vectors as single sets, from which the vectors are recovered; the satisfaction bridge reads internal satisfaction externally; the code set gathers all codes into one element of `L`; and constructible unions combine the pieces that the construction collects along the way.

```agda
open import L.Coding.Environment {ℓ} using ( env; cons )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envS; Ix; envOver; module Recover )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( graph; envFor; envFor-graph )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; keyS; key∈AllCodes )
open import L.Coding.CodeConstructibility {ℓ} using ( cupʟ; cupʟ-inl; cupʟ-inr )
```

The uniform satisfaction table assigns to every code its satisfaction set, read externally; the canonical-names construction places numerals and the codes of parameter-free formulas, which may still have free-variable slots, in `Lset ω`; the internal well-order of a stage compares its members, first by birth stage and then by name.

```agda
open import L.Coding.UniformSatisfaction {ℓ} lem using ( val-sat )
open import L.Choice.CanonicalNames {ℓ} lem using ( limitCode; numeral∈limit; pr∈limit )
open import L.Choice.NameComparison {ℓ} lem using ( freeCode-in; freeCode-out )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf )
```

Least-element search over a strict well-order returns, from an inhabited family, the least element; relations themselves become sets of pairs with two readings, and the order-type chapter states the three predicates describing a collapse table.

```agda
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; leastOf; isPropLeastOf )
  renaming ( Tri to Tri∙; lt to tri-lt; eq to tri-eq; gt to tri-gt )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( module Relation; isL-ord )
open import L.GCH.OrderType {ℓ} lem
```

Correctness, completeness at an argument, and the value clause are each a formula with its two satisfaction readings; internal ω-recursion iterates a definable two-place step along the model's own `ω`. The hull's members are named by codes of arbitrary nesting depth, so no single separation can produce the hull; it is reached by iterating a definable one-step closure along `ω`, and this is why the closure must be built ω times.

```agda
  using ( Holds; Complete; Src; ValueIs; Correct
        ; completeAt; complete-in; complete-out
        ; valueAt; value-in; value-out
        ; correctAt; correct-in; correct-out )
open import L.GCH.OmegaRecursion {ℓ} lem using ( module Iterate )
```

The proof has two connected parts. First, a local collapse table shows that each collapse value of a constructible carrier is constructible. Second, the Skolem hull is realized as the union of its finite closure stages, making the carrier itself constructible and allowing the first argument to apply to it.

```agda
open import L.GCH.SkolemHull {ℓ} lem using ( module HullStage; module Frame )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.CondensationTransfer {ℓ} lem using ( module Condense )
```

A nested hull code has a finite depth, computed by taking maxima over the depths of its parameter codes. This depth bounds the closure stage at which its value appears.

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Nat.Properties using ( max )
open import Cubical.Data.Nat.Order using ( _≤_; left-≤-max; right-≤-max )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
```

Finite parameter vectors let one witness code depend on finitely many earlier values. Empty sets, singletons and unordered pairs provide the set codes needed to represent those parameters and their ordered pairs inside the hierarchy.

```agda
import Cubical.Data.Empty as Empty
open import Cubical.Foundations.Prelude using ( subst2; J )
open import Cubical.Data.Vec using ( Vec; _∷_; []; lookup )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⁅_,_⁆; ⁅_⁆s; module InfinitySet )
```

The von Neumann successor and numerals organize the finite closure stages inside `ω`. Unordered pairs also supply the ingredients from which the ordered pairs used in graphs and environments are encoded.

```agda
open import V.Model {ℓ} using ( pair-spec )
open InfinitySet {ℓ} using ( ω; sucV; #_ )
open import Cubical.Foundations.HLevels
  using ( isPropΣ; isPropΠ; isPropΠ2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

Existence statements are kept propositionally truncated until their witnesses are needed only to prove another proposition. Equalities in the cumulative hierarchy are propositions, so the collapse argument can eliminate such truncated data when proving its set equalities.

```agda
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 ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
```

Two levels of membership must be distinguished. Ambient membership belongs to the cumulative hierarchy, whereas an element of the constructible carrier packages an ambient set together with a proof of constructibility; carrier membership is read through those underlying sets.

```agda
open hPropStructure 𝒮ᵥ
module CS = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
```

For formulas whose constants are elements of `L`, `⊨` denotes satisfaction in the class model of `L`. Relabeling constants by the identity map leaves both the environment and satisfaction unchanged.

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
```

Seven names, `i0` through `i6`, abbreviate the first seven de Bruijn indices, one per slot of a long environment.

```agda
private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0
```

Each successor shifts the preceding index into a larger finite type; the names continue slot by slot.

```agda
  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
```

These are free-variable positions, whose interpretation changes as later binders extend the environment.

```agda
  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5
```

An element of the carrier is determined by its underlying set, because constructibility is a proposition: two carrier elements with equal underlying sets are equal, and the helper `S≡` makes that identification wherever a carrier element is rebuilt from the same underlying set.

```agda
  S≡ : {x y : CS.S} → fst x ≡ fst y → x ≡ y
  S≡ = Σ≡Prop (λ v → snd (isL v))
```

The renaming `ρs` swaps the two slots: a formula about a pair in the swapped order is read in the original order. It is used when the step formula is proved in one slot order and consumed in the other.

```agda
  ρs : Fin 2 → Fin 2
  ρs zero = suc zero
  ρs (suc zero) = zero
```

The renaming `ρf` keeps `w` in slot zero and sends `Z` from slot one to slot two, skipping the middle slot occupied by the candidate next stage `Z'`.

```agda
  ρf : Fin 2 → Fin 3
  ρf zero = zero
  ρf (suc zero) = suc (suc zero)
```

An agreement for `ρs` says that the swapped environment carries the same elements as the original at the moved slots. Both cases are proved by reflexivity, since each slot is sent to the position of the very same element.

```agda
  ags : (Z'' w : CS.S) → Ren.Agrees ρs (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ [])
  ags Z'' w zero = refl
  ags Z'' w (suc zero) = refl
```

Fix an arbitrary constructible carrier `M`.

```agda
  agf : (w Z' Z : CS.S) → Ren.Agrees ρf (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ [])
  agf w Z' Z zero = refl
  agf w Z' Z (suc zero) = refl
```

## The collapse of a constructible carrier stays in L

The collapse argument uses only the constructibility of `M` and the predecessors that remain inside it; no transitivity assumption is imposed.

```agda
module PiIn (Mʟ : CS.S) where
```

Let `M` be the underlying set of the chosen constructible carrier. Its accompanying certificate ensures that every member later lifted from `M` is constructible.

```agda
  M : S
  M = fst Mʟ
```

The collapse `π x` is formed from the collapse values of those members of `x` that also lie in `M`; `πX` collects the values `π x` for `x ∈ M`. This restricted predecessor relation makes the definition meaningful without assuming that `M` is transitive.

```agda
  module C = Collapse M using ( Fiber; π; π-compute; πX; πX-member; π∈-fwd )
```

Since constructibility is inherited by members, every `y ∈ M` is constructible. Hence such a `y` can be paired with that proof and treated as an element of the constructible carrier.

```agda
  memL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL y ⟩
  memL y y∈M = isL-trans {x = M} {y = y} y∈M (snd Mʟ)
```

The lifting `up` packages a member as a carrier element. The first lemma reads the collapse value outward: every member of `π x` is the collapse of a member of `x` that lies in `M`, which follows from the computation clause of the collapse, the identity `π x` equals the image of the collapse over the members of `x` inside `M`.

```agda
  up : (y : S) → ⟨ y ∈ˢ M ⟩ → CS.S
  up y y∈M = y , memL y y∈M
  π-mem-out : (x w : S) → ⟨ w ∈ˢ C.π x ⟩
            → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) ∥₁
  π-mem-out x w w∈ = PT.map mk (subst (λ u → ⟨ w ∈ˢ u ⟩) (C.π-compute x) w∈)
```

The conversion turns the collapse's own fibre witness into the member statement: the fibre pairs a presented index with the proof that the collapse of the presented element equals `w`, and the presented element is a member of `x` whose collapse is taken.

```agda
    where
    mk : Σ[ p ∈ C.Fiber x ] (C.π (⟪ x ⟫↪ (p .fst)) ≡ w)
       → Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w))
    mk (p , q) = ⟪ x ⟫↪ (p .fst)
               , ( member x (p .fst)
```

The membership relation of `M` is expressed using three free-variable slots, read by `Relation` at the environment `y ∷ x ∷ e ∷ []`; the third slot carries the coded pair, while the formula asserts `y ∈ M`, `x ∈ M`, and `y ∈ x`.

```agda
                 , ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = M} .snd (p .snd)
                 , q )
  private
    module Membership = Relation Mʟ Mʟ
      ((var i1 ∈̇ con Mʟ) ∧̇ ((var i0 ∈̇ con Mʟ) ∧̇ (var i1 ∈̇ var i0)))
```

The host-side reading of the relation is exactly the three memberships, conjoined; this is the adequacy that lets the object-language formula and the external statement stand for each other.

```agda
      (λ y x → (fst y ∈ˢ M) ⊓ ((fst x ∈ˢ M) ⊓ (fst y ∈ˢ fst x)))
      (λ y x z h → h) (λ y x z h → h)
```

The relation becomes an element of the model: a set of pairs of carrier elements, introduced and eliminated by the two readings. Because the relation is bounded by the carrier, the pair set is small enough to be carved out by separation.

```agda
  R : CS.S
  R = Membership.rel
```

The introduction reading exhibits both endpoint memberships and the membership between them, which is the content of the relation at the pair.

```agda
  R-in : (y x : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst x ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst x ⟩
       → Holds R y x
  R-in y x my mx yx = Membership.into y x my mx (my , mx , yx)
```

The elimination reading returns the same three memberships; the two directions together say the relation is adequate, neither stronger nor weaker than the host-side statement.

```agda
  R-out : (y x : CS.S) → Holds R y x
        → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst x ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst x ⟩
  R-out = Membership.pair-out
```

The collapse formula is local, not global. At slots for a value and an argument it says: there merely exists a table `F` correct for the relation `R`, complete at the argument, whose value at the argument is the given value. No single global function graph is claimed; at each argument only the existence of such a table is asserted, which is what lets the formula hold over a non-transitive carrier.

```agda
  opaque
    piFo : Formula CS.S 2
    piFo = ∃̇ ( correctAt i0 R
             ∧̇ ( completeAt i0 R i2 ∧̇ valueAt i0 R i2 i1 ) )
```

The outward reading of the formula unpacks the satisfaction into the three components: the correct table, its completeness at the argument, and the value clause, each transported out of its binder by the order-type chapter's own projections.

```agda
    piFo-out : (v p : CS.S) → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
             → ∥ Σ[ F ∈ CS.S ] (Correct F R × (Complete F R p × ValueIs F R p v)) ∥₁
    piFo-out v p = PT.map (λ { (F , (hc , (hm , hv))) → F
      , ( correct-out i0 R (F ∷ v ∷ p ∷ []) hc
        , ( complete-out i0 R i2 (F ∷ v ∷ p ∷ []) hm
```

The innermost projection finishes the unpacking: the value clause arrives as an ordinary statement about the table's entry at the argument.

```agda
          , value-out i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) })
```

The inward reading chooses the table `F` for the existential quantifier and supplies proofs of its correctness, completeness at the argument, and value clause. Together with the outward reading, this identifies the formula exactly with its intended content.

```agda
    piFo-in : (v p F : CS.S) → Correct F R → Complete F R p → ValueIs F R p v
            → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
    piFo-in v p F hc hm hv = ∣ F
      , ( correct-in i0 R (F ∷ v ∷ p ∷ []) hc
        , ( complete-in i0 R i2 (F ∷ v ∷ p ∷ []) hm
```

Uniqueness is proved by one membership induction. The motive says: at every constructible member `x` of the carrier, any table correct for the relation and complete at `x` assigns the collapse of `x` as its value. Both the constructibility and the membership travel with the motive, because the table's entries are pairs of carrier elements.

```agda
          , value-in i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) ∣₁
  private
    Pv : CS.S → S → Type (ℓ-suc ℓ)
    Pv F x = (xL : ⟨ isL x ⟩) → ⟨ x ∈ˢ M ⟩ → (v : CS.S)
           → Complete F R (x , xL) → ValueIs F R (x , xL) v → fst v ≡ C.π x
```

The induction runs along membership in the ambient hierarchy, exactly as the collapse itself is defined along it: to prove the motive at `x`, prove it at every member of `x`.

```agda
  value-val′ : (F : CS.S) → Correct F R → (x : S) → Pv F x
  value-val′ F hc = ∈-induction {P = Pv F} go
    where
    go : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → Pv F y) → Pv F x
    go x IH xL x∈M v cmp val =
```

The step compares members: the recorded value and the collapse have the same members, and extensionality of the ambient hierarchy turns that into equality. The argument is presented as a carrier element, so its entries may be typed over the carrier.

```agda
      extensionalV {a = fst v} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w))
      where
      xS : CS.S
      xS = x , xL
```

Forward: a member `w` of the recorded value is carried, and the value clause produces a relation entry together with a table entry at it. The carrying packages `w` with the constructibility inherited from the recorded value.

```agda
      fwd : (w : S) → ⟨ w ∈ˢ fst v ⟩ → ⟨ w ∈ˢ C.π x ⟩
      fwd w w∈ = PT.rec (snd (w ∈ˢ C.π x)) read (val wS .fst w∈)
        where
        wS : CS.S
        wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)
```

The source witness separates into a relation fact `ry` and a table entry `fy`. Reading `ry` yields `y ∈ M` and `y ∈ x`; the induction hypothesis applied to `fy` identifies `w` with `π y`, and `π∈-fwd` then places `w` in `π x`.

```agda
        read : Σ[ y ∈ CS.S ] (Holds R y xS × Holds F y wS) → ⟨ w ∈ˢ C.π x ⟩
        read (y , (ry , fy)) =
          subst (λ t → ⟨ t ∈ˢ C.π x ⟩) e (C.π∈-fwd x (fst y) y∈x y∈M)
          where
          y∈M : ⟨ fst y ∈ˢ M ⟩
```

The relation entry also says the component lies in the argument, which unlocks the induction hypothesis: the table's value at that component equals the collapse of the component. This equation, composed with the collapse reading, is the identification of `w`.

```agda
          y∈M = R-out y xS ry .fst
          y∈x : ⟨ fst y ∈ˢ x ⟩
          y∈x = R-out y xS ry .snd .snd
          e : C.π (fst y) ≡ w
          e = sym (IH (fst y) y∈x (snd y) y∈M wS (hc y wS fy .fst) (hc y wS fy .snd))
```

Backward: a member `w` of the collapse decomposes, by the outward reading already proved, into a component of the argument inside the carrier whose collapse is `w`. Completeness at the original argument `x`, applied to the predecessor `y`, supplies an entry `(y,u)`.

```agda
      bwd : (w : S) → ⟨ w ∈ˢ C.π x ⟩ → ⟨ w ∈ˢ fst v ⟩
      bwd w w∈ = PT.rec (snd (w ∈ˢ fst v)) read (π-mem-out x w w∈)
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst v ⟩
        read (y , (y∈x , y∈M , e)) = PT.rec (snd (w ∈ˢ fst v)) inner (cmp yS ry)
```

The component is carried as a carrier element, and the relation entry at the pair is reintroduced from the two memberships and the membership between them.

```agda
          where
          yS : CS.S
          yS = up y y∈M
          ry : Holds R yS xS
          ry = R-in yS xS y∈M x∈M y∈x
```

The induction hypothesis identifies `u` with `π y`, and `π y = w` transports membership in the recorded value to `w`. This is what the backward direction claims.

```agda
          inner : Σ[ u ∈ CS.S ] Holds F yS u → ⟨ w ∈ˢ fst v ⟩
          inner (u , fu) =
            subst (λ t → ⟨ t ∈ˢ fst v ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁)
            where
            eu : fst u ≡ C.π y
```

The equation `eu` is the induction hypothesis at the component: the table's value at `y` equals the collapse of `y`. Composed with the equation carried by the decomposition, it identifies the entry's value with `w`, which is exactly what the backward direction had to place.

```agda
            eu = IH y y∈x (snd yS) y∈M u (hc yS u fu .fst) (hc yS u fu .snd)
```

Applying the induction to the underlying set of a carrier element gives the same uniqueness statement in the restricted structure. The resulting determination lemma says that whenever the collapse formula is satisfied at a member of `M`, its value must equal that member's collapse.

```agda
  value-val : (F : CS.S) → Correct F R → (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → (v : CS.S)
            → Complete F R x → ValueIs F R x v → fst v ≡ C.π (fst x)
  value-val F hc x = value-val′ F hc (fst x) (snd x)
  piFo-val : (q : CS.S) → ⟨ fst q ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩
           → fst v ≡ C.π (fst q)
```

The proof eliminates the truncated existence into the equality of two h-sets, which is a proposition, and applies the uniqueness just proved to the correct table handed over by the outward reading. The next construction cuts from the carrier the elements lying inside a given element of `L`.

```agda
  piFo-val q mq v h = PT.rec (setIsSet (fst v) (C.π (fst q)))
    (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv })
    (piFo-out v q h)
  module Cut (K : CS.S) where
```

The cutting formula is the single atomic formula: the free slot is a member of the constant `K`. Everything the slice contains is what satisfies it.

```agda
    cutFo : Formula CS.S 1
    cutFo = var i0 ∈̇ con K
```

Separation applied at `Mʟ` yields the slice as an element of `L`, so the slice is more than a mere class of members. This is what lets the slice serve as the domain of an internal recursion.

```agda
    opaque
      cut : CS.S
      cut = hasSeparationL Mʟ cutFo .fst .fst
```

The membership specification identifies membership in the slice with membership in the carrier together with satisfaction of the cutting formula, which unpacks to lying in the underlying set of `K`.

```agda
      cut-mem : (y : CS.S) → (y CS.∈ˢ cut) ≡ ((y CS.∈ˢ Mʟ) ⊓ ((y ∷ []) ⊨ cutFo))
      cut-mem = hasSeparationL Mʟ cutFo .fst .snd
```

The inward direction combines membership in `M` with membership in the underlying set of `K` to place the carried element in the slice.

```agda
      cut-in : (y : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst K ⟩ → ⟨ y CS.∈ˢ cut ⟩
      cut-in y my yK = subst ⟨_⟩ (sym (cut-mem y)) (my , yK)
```

The outward direction reads the same specification back into its two components. A member `q` of the carrier is good at a stage `δ` when membership in that stage yields both a constructible presentation of its collapse and the collapse formula at `q`.

```agda
      cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst K ⟩
      cut-out y h = subst ⟨_⟩ (cut-mem y) h
  Good : S → S → Type (ℓ-suc ℓ)
  Good δ q = ⟨ q ∈ˢ M ⟩ → ⟨ q ∈ˢ Lset δ ⟩
           → Σ[ qL ∈ ⟨ isL (C.π q) ⟩ ] ((mq : ⟨ q ∈ˢ M ⟩)
```

The second component of goodness packages the collapse as an element of `𝒮ʟ` using its constructibility proof, and states that the collapse formula holds of this value and the chosen presentation of the member of `M`.

```agda
                → ⟨ ((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo ⟩)
```

Goodness is a proposition: membership in the carrier, in the stage, constructibility, and satisfaction are each one. This matters because the stage decomposition returns a merely-existing witness, and a merely-existing goodness can be consumed without choosing among witnesses.

```agda
  isPropGood : (δ q : S) → isProp (Good δ q)
  isPropGood δ q = isPropΠ2 λ _ _ → isPropΣ (snd (isL (C.π q)))
    λ qL → isPropΠ λ mq → snd (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo)
```

Fix an ordinal stage `δ'` and assume goodness for every `q` that lies both in `M` and in `Lset δ'`. These earlier collapse values will be assembled into the value at the next argument.

```agda
  module Step (δ' : S) (oδ' : IsOrd δ')
              (IH : (q : S) → Good δ' q) where
```

The slice is cut at the stage `Lset δ'`: the members of the carrier that the stage already contains. Because the stage is a set of `L`, the slice is an element of `L` by separation, and it is exactly the domain the induction hypothesis speaks about.

```agda
    module Sl = Cut (LsetS δ' oδ') using ( cut; cut-in; cut-out )
```

Stages are transitive, so a member of a member of the stage is still inside the stage; this is the fact that later restricts the table's conditions to smaller arguments. By the induction hypothesis, the collapse of a slice member is available as an element of `𝒮ʟ`; its constructibility proof is the first component of goodness.

```agda
    Lδ'-trans : {x y : S} → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ Lset δ' ⟩ → ⟨ y ∈ˢ Lset δ' ⟩
    Lδ'-trans {x} {y} = layer-trans (Lset-layer δ') {x = x} {y = y}
    πʟ : (y : CS.S) → ⟨ y CS.∈ˢ Sl.cut ⟩ → CS.S
    πʟ y hy = C.π (fst y) , IH (fst y) (Sl.cut-out y hy .fst) (Sl.cut-out y hy .snd) .fst
```

The collapse formula holds at the pair of that collapse and the member, by the same induction hypothesis: the second component of goodness is exactly a satisfaction of the formula at the pair, transported along the identification of the element with its underlying set.

```agda
    πʟ-graph : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩)
             → ⟨ (πʟ y hy ∷ y ∷ []) ⊨ piFo ⟩
    πʟ-graph y hy =
      subst (λ y' → ⟨ (πʟ y hy ∷ y' ∷ []) ⊨ piFo ⟩) (S≡ refl)
        (IH (fst y) my (Sl.cut-out y hy .snd) .snd my)
```

The identification uses the membership of the member in the carrier, read out of the slice specification; the underlying set has not changed, so the transport is determined by the propositionality of constructibility.

```agda
      where
      my : ⟨ fst y ∈ˢ M ⟩
      my = Sl.cut-out y hy .fst
```

Over the slice, these collapse values form an internal recursion with domain the slice and graph `piFo`. Constructibility supplies each value as an element of `𝒮ʟ`, so the graph entries are pairs of `𝒮ʟ`-elements.

```agda
    private
      Rπ : Recursion
      Rπ = record
        { dom = Sl.cut ; graph = piFo
        ; funct = λ y hy → (πʟ y hy , πʟ-graph y hy)
```

Functionality holds because the collapse formula determines its value at every member of the carrier: any other value satisfying the formula at the same pair is equal to it, which the determination lemma reads out. The equality of the corresponding `𝒮ʟ`-elements then follows because their constructibility proofs are proposition-valued.

```agda
            , λ { (v , h) → Σ≡Prop (λ w → snd ((w ∷ y ∷ []) ⊨ piFo))
                (sym (S≡ (piFo-val y (Sl.cut-out y hy .fst) v h))) } }
```

The graph recursion of `L` collects the table: a set of pairs of carrier elements whose entries are exactly the collapse records over the slice.

```agda
      module T = RecursionGraph Rπ using ( F; F-in; pair-out )
```

The collected set is the table at the stage: an element of `L` that pairs each slice member with its constructible collapse.

```agda
    Tab : CS.S
    Tab = T.F
```

The inward reading of the table exhibits its entries: at every slice member, the pair of the member with its collapse is recorded.

```agda
    Tab-in : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩) → Holds Tab y (πʟ y hy)
    Tab-in = T.F-in
```

The outward reading decomposes an entry into a slice member and a value equal to the collapse of its underlying set. Together with the inward reading this says the table records exactly the collapses, nothing distorted.

```agda
    Tab-pair : (x v : CS.S) → Holds Tab x v
             → ⟨ x CS.∈ˢ Sl.cut ⟩ × (fst v ≡ C.π (fst x))
    Tab-pair = T.pair-out
```

An argument `x` is closed when every member of `x` that also belongs to `M` lies in the stage slice. This condition is imposed on each argument separately, because no transitivity assumption is made on `M`.

```agda
    Closed : CS.S → Type (ℓ-suc ℓ)
    Closed x = (y : S) (y∈x : ⟨ y ∈ˢ fst x ⟩) (y∈M : ⟨ y ∈ˢ M ⟩)
             → ⟨ up y y∈M CS.∈ˢ Sl.cut ⟩
```

A slice member is closed by transitivity of the stage: any member of it that lies in `M` remains in the stage and therefore belongs to the slice.

```agda
    slice-closed : (x : CS.S) → ⟨ x CS.∈ˢ Sl.cut ⟩ → Closed x
    slice-closed x hx y y∈x y∈M =
      Sl.cut-in (up y y∈M) y∈M (Lδ'-trans {x = fst x} {y = y} y∈x (Sl.cut-out x hx .snd))
```

For a closed argument, completeness of the table is the truncated existence of the table's own entry at each related member: closedness places that member inside the slice, where the table records its collapse. The relation entry is decomposed to name the member.

```agda
    complete-of : (x : CS.S) → Closed x → Complete Tab R x
    complete-of x cl y ry = ∣ πʟ y' hy' , subst (λ w → ⟨ pr w (C.π (fst y)) ∈ˢ fst Tab ⟩) refl (Tab-in y' hy') ∣₁
      where
      ro = R-out y x ry
      y' : CS.S
```

The member is carried as a carrier element, and closedness places the carried element inside the slice, which is exactly the hypothesis under which the table recorded the collapse.

```agda
      y' = up (fst y) (ro .fst)
      hy' : ⟨ y' CS.∈ˢ Sl.cut ⟩
      hy' = cl (fst y) (ro .snd .snd) (ro .fst)
```

For a closed argument, the value clause holds of the collapse itself. The proof has two directions: every member of the collapse value comes from a related member, and every member related to the argument is carried into the collapse value by the table.

```agda
    valueIs-of : (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → Closed x → (v : CS.S) → fst v ≡ C.π (fst x)
               → ValueIs Tab R x v
    valueIs-of x mx cl v ev w = fwd , bwd
      where
      fwd : ⟨ fst w ∈ˢ fst v ⟩ → Src Tab R x w
```

Forward: a member `w` of the candidate value `v` is decomposed by the collapse reading into a component of the argument inside the carrier, whose collapse equals `w`. The decomposition is a truncated existence, and the elimination targets a proposition.

```agda
      fwd w∈ = PT.map read (π-mem-out (fst x) (fst w) (subst (λ t → ⟨ fst w ∈ˢ t ⟩) ev w∈))
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ fst x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ fst w))
             → Σ[ y ∈ CS.S ] (Holds R y x × Holds Tab y w)
        read (y , (y∈x , y∈M , e)) = up y y∈M
```

The component is lifted to the carrier. Its membership in the argument yields the relation entry, while the table entry is transported along the equality between its collapse and `w`. Together these two entries form the required witness of `Src Tab R x w`.

```agda
          , ( R-in (up y y∈M) x y∈M mx y∈x
            , subst (λ t → ⟨ pr y t ∈ˢ fst Tab ⟩) e (Tab-in (up y y∈M) (cl y y∈x y∈M)) )
```

Backward: a source entry for `w` names a related member whose table value is `w`. The pair reading splits the entry into memberships and an equality; the collapse reading places `w` in the collapse of the first component, and the two equations transport it back into the recorded value.

```agda
      bwd : Src Tab R x w → ⟨ fst w ∈ˢ fst v ⟩
      bwd = PT.rec (snd (fst w ∈ˢ fst v)) (λ { (y , (ry , ty)) →
        subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev)
          (C.π∈-fwd (fst x) (fst y) (R-out y x ry .snd .snd) (R-out y x ry .fst)) })
```

The correctness of the table at each entry is assembled from the two clauses at the slice member that the entry names. The pair reading contributes the slice membership and the carrier membership.

```agda
    Tab-correct : Correct Tab R
    Tab-correct x v hxv = complete-of x cl , valueIs-of x mx cl v (Tab-pair x v hxv .snd)
      where
      hx : ⟨ x CS.∈ˢ Sl.cut ⟩
      hx = Tab-pair x v hxv .fst
```

The carrier membership and closedness complete the hypotheses, and the step module is parameterized by an argument `q` of the carrier all of whose members lie below the earlier stage. This is the situation needed for an element of the definable powerset of `Lset δ'`; here closedness follows from `q⊆`.

```agda
      mx : ⟨ fst x ∈ˢ M ⟩
      mx = Sl.cut-out x hx .fst
      cl : Closed x
      cl = slice-closed x hx
    module At (q : S) (mq : ⟨ q ∈ˢ M ⟩) (q⊆ : (y : S) → ⟨ y ∈ˢ q ⟩ → ⟨ y ∈ˢ Lset δ' ⟩) where
```

The argument is carried as a carrier element, so that it can serve as an environment slot and as the second component of pairs.

```agda
      qS : CS.S
      qS = up q mq
```

Closedness of the carried argument holds by the hypothesis: each member inside the carrier lies below the earlier stage, and the slice admits it. The members of the argument inside the carrier are then cut out as their own slice, the domain on which the collapse value will be computed.

```agda
      cl : Closed qS
      cl y y∈q y∈M = Sl.cut-in (up y y∈M) y∈M (q⊆ y y∈q)
      module Mq = Cut qS using ( cut; cut-in; cut-out )
```

The collapse value of `q` is built as an internal recursion: domain the slice of members of `q` in the carrier, graph the collapse formula. This functional graph therefore meets the hypotheses of replacement in `L`.

```agda
      private
        valR : Recursion
        valR = record
          { dom   = Mq.cut
          ; graph = piFo
```

Functionality is assembled through `mereFunct`, from a merely-existing unique value at each argument. The witness `wit` produces such a value together with its satisfaction and uniqueness, all inside the truncation, because uniqueness of the collapse formula at a member of the carrier is a proposition.

```agda
          ; funct = λ y hy → mereFunct piFo y (wit y hy) }
          where
          wit : (y : CS.S) (hy : ⟨ y CS.∈ˢ Mq.cut ⟩)
              → ∥ Σ[ v ∈ CS.S ] (⟨ (v ∷ y ∷ []) ⊨ piFo ⟩
                                × ((v' : CS.S) → ⟨ (v' ∷ y ∷ []) ⊨ piFo ⟩ → v' ≡ v)) ∥₁
```

The witness is the global collapse value `C.π (fst y)`, presented as constructible by the induction hypothesis. The stage-slice table supplies its `piFo` proof, and `piFo-val` supplies uniqueness.

```agda
          wit y hy = ∣ πʟ y hy'
            , ( πʟ-graph y hy'
              , λ v' hv' → S≡ (piFo-val y my v' hv') ) ∣₁
            where
            my : ⟨ fst y ∈ˢ M ⟩
```

The membership of `y` in the carrier comes from the slice of `q`. The hypothesis puts every member of `q` in `Lset δ'`, so every such carrier element is admitted by the stage slice.

```agda
            my = Mq.cut-out y hy .fst
            hy' : ⟨ y CS.∈ˢ Sl.cut ⟩
            hy' = Sl.cut-in y my (q⊆ (fst y) (Mq.cut-out y hy .snd))
```

Replacement now collects the values of this recursion into an element of `L`: its members are exactly the constructible collapse values of members of `q` that lie in `M`.

```agda
        module Vq = Of valR using ( table; table-in; table-out )
```

The underlying set of the table agrees with the collapse of `q`, proved by extensionality through a member-by-member equivalence. Forward: a member of the table is a value at some member `y` of `q` inside the carrier, and the elimination targets the proposition that `w` lies in the collapse of `q`.

```agda
      val≡π : fst Vq.table ≡ C.π q
      val≡π = extensionalV {a = fst Vq.table} {b = C.π q} (λ w → ⇔toPath (fwd w) (bwd w))
        where
        fwd : (w : S) → ⟨ w ∈ˢ fst Vq.table ⟩ → ⟨ w ∈ˢ C.π q ⟩
        fwd w hw = PT.rec (snd (w ∈ˢ C.π q))
```

The outward reading names the member `y` and its value; the determination lemma identifies the value with the collapse of `y`, and the collapse reading places the collapse of `y` inside the collapse of `q`, which the transport composes.

```agda
          (λ { (y , (hy , h)) →
             subst (λ t → ⟨ t ∈ˢ C.π q ⟩)
               (sym (piFo-val y (Mq.cut-out y hy .fst) wS h))
               (C.π∈-fwd q (fst y) (Mq.cut-out y hy .snd) (Mq.cut-out y hy .fst)) })
          (Vq.table-out wS hw)
```

Since `w` belongs to the constructible value set `Vq.table`, transitivity of `L` supplies its constructibility and hence its presentation as an element of `𝒮ʟ`.

```agda
          where
          wS : CS.S
          wS = w , isL-trans {x = fst Vq.table} {y = w} hw (snd Vq.table)
```

Backward: a member of the collapse of `q` decomposes into a component of `q` inside the carrier whose collapse equals it, which is precisely the form in which the table records entries.

```agda
        bwd : (w : S) → ⟨ w ∈ˢ C.π q ⟩ → ⟨ w ∈ˢ fst Vq.table ⟩
        bwd w hw = PT.rec (snd (w ∈ˢ fst Vq.table)) read (π-mem-out q w hw)
          where
          read : Σ[ y ∈ S ] (⟨ y ∈ˢ q ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst Vq.table ⟩
          read (y , (y∈q , y∈M , e)) =
```

The equation transports `w` to the collapse of the component, and the table's inward reading produces the entry at the carried component, which records exactly that collapse.

```agda
            subst (λ t → ⟨ t ∈ˢ fst Vq.table ⟩) e
              (Vq.table-in yS (πʟ yS hy') hy (πʟ-graph yS hy'))
            where
            yS : CS.S
            yS = up y y∈M
```

The carried component lies in the slice of `q` by its carrier membership, and in the stage slice by the hypothesis that members of `q` lie below the earlier stage.

```agda
            hy : ⟨ yS CS.∈ˢ Mq.cut ⟩
            hy = Mq.cut-in yS y∈M y∈q
            hy' : ⟨ yS CS.∈ˢ Sl.cut ⟩
            hy' = Sl.cut-in yS y∈M (q⊆ y y∈q)
```

The collapse of `q` is constructible: it equals the underlying set of the table, and the table is an element of `L`, so constructibility is transported along the equality. This is the first clause of goodness at `q`.

```agda
      πq-isL : ⟨ isL (C.π q) ⟩
      πq-isL = subst (λ t → ⟨ isL t ⟩) val≡π (snd Vq.table)
```

The second clause of goodness is the collapse formula satisfied at the pair of the collapse with the member: correctness of the table, completeness at the closed argument, and the value clause identifying the value with the collapse. With both clauses, the stage induction can be stated: goodness at every ordinal.

The induction runs along membership in the hierarchy, consuming at each step the decomposition of membership in the stage.

```agda
      good : (mq' : ⟨ q ∈ˢ M ⟩) → ⟨ ((C.π q , πq-isL) ∷ up q mq' ∷ []) ⊨ piFo ⟩
      good mq' = subst (λ q' → ⟨ ((C.π q , πq-isL) ∷ q' ∷ []) ⊨ piFo ⟩) (S≡ refl)
        (piFo-in (C.π q , πq-isL) qS Tab Tab-correct (complete-of qS cl)
          (valueIs-of qS mq cl (C.π q , πq-isL) refl))
  good-at : (δ : S) → IsOrd δ → (q : S) → Good δ q
```

To prove goodness at `δ`, the membership of `q` in the stage `Lset δ` is decomposed: `q` lies in the definable powerset of an earlier stage `δ'`. The decomposition is eliminated into goodness, because goodness is a proposition.

```agda
  good-at = ∈-induction {P = λ δ → IsOrd δ → (q : S) → Good δ q} go
    where
    go : (δ : S) → ((δ' : S) → ⟨ δ' ∈ˢ δ ⟩ → IsOrd δ' → (q : S) → Good δ' q)
       → IsOrd δ → (q : S) → Good δ q
    go δ IH oδ q mq q∈Lδ = PT.rec (isPropGood δ q) read (Lset-out δ q q∈Lδ) mq q∈Lδ
```

The decomposition names the earlier stage `δ'` below `δ` and the membership of `q` in its definable powerset. Using goodness below `δ'`, the step construction yields goodness at `q`. The definable powerset clause then says every member of `q` lies in the stage `Lset δ'`, which is the closedness hypothesis the step consumes.

```agda
      where
      read : Σ[ δ' ∈ S ] (⟨ δ' ∈ˢ δ ⟩ × ⟨ q ∈ˢ 𝒟ₒ (Lset δ') ⟩) → Good δ q
      read (δ' , (δ'∈δ , q∈𝒟)) _ _ = A.πq-isL , A.good
        where
        oδ' : IsOrd δ'
```

Ordinality of `δ'` follows from `δ' ∈ δ`. Applying the induction hypothesis below `δ'`, together with the definable-powerset fact that every member of `q` lies in `Lset δ'`, yields goodness at `q`. Thus the membership induction proves `good-at`. Since `M` itself belongs to `L`, its constructibility certificate supplies a stage containing `M`; transitivity of that stage then places every member of `M` inside it.

```agda
        oδ' = mem-ord {A = δ} oδ δ' δ'∈δ
        module A = Step.At δ' oδ' (IH δ' δ'∈δ oδ') q mq (λ y y∈q → 𝒟ₒ∋⊆ (Lset δ') q q∈𝒟 y y∈q)
          using ( πq-isL; good )
  π-isL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL (C.π y) ⟩
  π-isL y y∈M = PT.rec (snd (isL (C.π y)))
```

A stage containing the constructible carrier `M` is obtained from the proof `Mʟ`, and goodness at that stage yields constructibility of the collapse of every member of `M`. The following claim begins the corresponding argument for members of the whole collapse image `C.πX`, again eliminating a truncated presentation into constructibility.

```agda
    (λ { (α , (oα , M∈Lα)) →
       good-at α oα y y∈M (layer-trans (Lset-layer α) {x = M} {y = y} y∈M M∈Lα) .fst })
    (snd Mʟ)
  πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩
  πX-isL x x∈πX = PT.rec (snd (isL x))
```

The statement of `πX-isL` is about members: each member of the collapse image is the collapse of some member of the carrier, hence constructible.

```agda
    (λ { (y , (y∈M , e)) → subst (λ w → ⟨ isL w ⟩) e (π-isL y y∈M) })
    (C.πX-member x x∈πX)
```

## The Skolem hull as an ω-iteration

This says exactly that the collapse image is contained in `L`; it is a statement about members, and no claim is made that the image itself is an element of `L`. With the first half finished, the second half opens under new parameters: a stage `lam` closed under successors of its members, and a start `X` whose members all lie in the stage.

```agda
module Telescope (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
```

The empty set lies in the stage as well, and the hull machinery is opened on these data: the hull carrier `M`, the fact that the hull is contained in the stage, and that every member of the start is a member of the hull.

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ
    using ( ∅∈Lsetα; hull-member; X⊆M; Hull⊆L )
  open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ public
```

A hull code is either a base name for a member of `X`, or `wit k ψ cs`, which stores a constant-free formula and codes for its parameters. Its value is obtained by evaluating the subcodes and then, according as a witness exists, choosing the least witness or the junk value.

```agda
    using ( Code; base; wit; val; vals; search; Sat; Hull; val-wit )
  open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ using ( inHull; _⊨₀_ )
```

The small carrier `SL` collects the members of the stage over which everything is typed. A parameter vector is drawn from a set `Z` when each of its components belongs to the underlying set of `Z`; the searches of the step range only over such vectors.

```agda
  SL : Type (ℓ-suc ℓ)
  SL = HullStage.ASt.SL lam ordλ succλ X X⊆L ∅∈λ
  From : {k : ℕ} → CS.S → Vec SL k → Type (ℓ-suc ℓ)
  From {k} Z vs = (i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ fst Z ⟩
  Searched : CS.S → S → Type (ℓ-suc ℓ)
```

A search uses a constant-free formula of arity `k+1`. The vector from `Z` assigns its `k` parameter variables, while the remaining variable is assigned the candidate witness; `Sat` asserts that such a witness exists.

```agda
  Searched Z z = Σ[ k ∈ ℕ ] Σ[ ψ ∈ Formula (⊥* {ℓ}) (suc k) ] Σ[ vs ∈ Vec SL k ]
                 Σ[ w ∈ Sat k ψ vs ] (From Z vs × (z ≡ fst (search k ψ vs w)))
  Reads : CS.S → S → Type (ℓ-suc ℓ)
  Reads Z z = ⟨ z ∈ˢ fst Z ⟩ ⊎ ((z ≡ ∅) ⊎ Searched Z z)
```

The package contains the operation `Φ`, a two-variable formula `ΦFo`, and a proof that for every `Z` the environment assigning `Φ Z` and `Z` to its two variables satisfies that formula.

```agda
  record StepPack : Type (ℓ-suc (ℓ-suc ℓ)) where
    field
      Φ       : CS.S → CS.S
      ΦFo     : Formula CS.S 2
      defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩
```

The remaining fields pin the step down: any set satisfying the formula is the step's, members grow, the junk value is always present, and for every search at parameters from the current set the least witness is adjoined.

```agda
      only    : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
      grows   : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ fst (Φ Z) ⟩
      junk    : (Z : CS.S) → ⟨ ∅ ∈ˢ fst (Φ Z) ⟩
      least   : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
              → From Z vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ fst (Φ Z) ⟩
```

The outward field reads a member of the step host-side, provided the current set lies below the stage: every member of the step is an old member, the junk value, or the value of a search. This reading is what the exhaustion proof will spend.

```agda
      out     : (Z : CS.S) → ((z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
              → (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → ∥ Reads Z z ∥₁
```

The iteration module takes the constructibility of the start together with the packaged step. Both are needed: the internal recursion begins at an element of `L`, and the step supplies the formula and its clauses.

```agda
  module HullIter (X-isL : ⟨ isL X ⟩) (P : StepPack) where
    open StepPack P
```

The start is presented as a carrier element, pairing the set with its constructibility; this is the form the internal recursion consumes.

```agda
    Xʟ : CS.S
    Xʟ = X , X-isL
```

The internal ω-recursion produces the iterates, and its closure machinery carries the growth field along: each iterate contains the previous one. The iterates are sets of the model, which is what will make their union an element of `L`.

```agda
    module It = Iterate Xʟ ΦFo Φ defines only
      using ( it; module Closure; iterUnion; iterUnion-in; iterUnion-out; iter; iter-in; iter-out; ω-num; Num )
    module Cl = It.Closure (λ Z z → grows Z (fst z)) using ( it-up )
```

The stages of the iteration are named `hullStep n`, the `n`-th application of the step to the start.

```agda
    hullStep : ℕ → CS.S
    hullStep = It.it
```

The iteration is governed by its defining equation: applying the step `n+1` times produces exactly the one-step closure `Φ` applied to the `n`-th iterate. The equation holds by `refl`, because internal ω-recursion computes its successor stage by calling the step operation directly, and nothing needs to be transported. This is the arithmetic of the construction in its barest form: each layer of the telescope is the closure of the previous layer under the single definable step.

```agda
    hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ Φ (hullStep n)
    hullStep-suc n = refl
```

The iterates grow with their index: if `n` does not exceed `n'`, then everything collected by the `n`-th iterate is still collected by the `n'`-th. The growth field of the step is applied once for each step of the difference, keeping the old members every time; the numeric equation carries the count, and the constructibility of the member travels with it, since it belongs to a constructible iterate. This monotonicity is what makes collection in an earlier iterate permanent.

```agda
    hullStep-≤ : (n n' : ℕ) → n ≤ n' → (z : S)
               → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ fst (hullStep n') ⟩
    hullStep-≤ n n' (k , e) z h =
      subst (λ m → ⟨ z ∈ˢ fst (hullStep m) ⟩) e (Cl.it-up n k (z , zL) h)
      where
```

Monotonicity of the iterates follows from the growth field: a member of an earlier iterate remains a member of every later one, and constructibility is carried along. Depth is assigned to hull codes by recursion: a base code has depth zero.

The witness code is one deeper than its code vector, because its value is computed one step after the values of the parameters.

```agda
      zL : ⟨ isL z ⟩
      zL = isL-trans {x = fst (hullStep n)} {y = z} h (snd (hullStep n))
    mutual
      depth : Code → ℕ
      depth (base m) = 0
```

The witness constructor adds one to the depth of its vector of subcodes.

```agda
      depth (wit k ψ cs) = suc (depths cs)
```

The depth of a code vector is the maximum of the depths of its entries: a vector is available once all of its entries are.

```agda
      depths : {m : ℕ} → Vec Code m → ℕ
      depths [] = 0
      depths (c ∷ cs) = max (depth c) (depths cs)
```

A helper records how a case split on a decidable disjunction behaves when one disjunct is impossible: if satisfaction is empty, the computed value is the junk branch, whatever the other branch would have said.

```agda
    private
      stuck-r : {A : Type (ℓ-suc ℓ)} (na : A → Empty.⊥)
                (f : A → SL) (g : (A → Empty.⊥) → SL) (s : A ⊎ (A → Empty.⊥))
              → Sum.rec f g s ≡ g na
      stuck-r na f g (inl a) = Empty.rec (na a)
```

The refutation branch is proved by the function extensionality of the impossible function: no member exists to distinguish.

```agda
      stuck-r na f g (inr h) = cong g (funExt (λ a → Empty.rec (na a)))
```

Hull into union, first half: every hull code has its value staged at the iterate indexed by its depth. A base code names a member of the start, present at the zeroth iterate.

```agda
    mutual
      hullStep-in : (c : Code) → ⟨ fst (val c) ∈ˢ fst (hullStep (depth c)) ⟩
      hullStep-in (base m) = member X m
      hullStep-in (wit k ψ cs) = go (lem (Sat k ψ (vals cs) , squash₁))
        where
```

A witness code is split according to whether its search is satisfiable. Its depth is one more than the depth of its parameter-code vector, and the successor equation identifies that depth with the iterate obtained by applying `Φ` once more.

```agda
        n : ℕ
        n = depths cs
        go : (s : Sat k ψ (vals cs) ⊎ (Sat k ψ (vals cs) → Empty.⊥))
           → ⟨ fst (Sum.rec (search k ψ (vals cs)) (λ _ → (∅ , HSH.∅∈Lsetα)) s)
                ∈ˢ fst (hullStep (suc n)) ⟩
```

If the search is satisfied, the least-witness clause of the step adjoins the searched value at the next iterate, whose parameters are available by the vector depths. If the search is unsatisfiable, there is no witness to adjoin, and the step keeps the junk value instead.

```agda
        go (inl w) = least (hullStep n) k ψ (vals cs) (vals-in cs) w
        go (inr h) = junk (hullStep n)
```

The parameters of a code vector are available at the maximum of the entry depths: each entry's value appeared at its own depth, and monotonicity carries it to the later iterate where the vector is consumed.

```agda
      vals-in : {m : ℕ} (cs : Vec Code m) → From (hullStep (depths cs)) (vals cs)
      vals-in (c ∷ cs) zero =
        hullStep-≤ (depth c) (max (depth c) (depths cs)) left-≤-max (fst (val c)) (hullStep-in c)
      vals-in (c ∷ cs) (suc i) =
        hullStep-≤ (depths cs) (max (depth c) (depths cs)) right-≤-max
```

The choice proceeds recursively over the parameter vector. For the empty vector, the empty code vector has the required value vector; at a nonempty vector, hull membership supplies a code for the head and recursion supplies codes for the tail.

```agda
          (fst (lookup i (vals cs))) (vals-in cs i)
    private
      choose : {k : ℕ} (vs : Vec SL k)
             → ((i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ Hull ⟩)
             → ∥ Σ[ cs ∈ Vec Code k ] (vals cs ≡ vs) ∥₁
```

The recursive step codes the head by hull membership and the tail recursively; the value equation is assembled componentwise, with the carrier equality reduced to the underlying sets.

```agda
      choose [] h = ∣ [] , refl ∣₁
      choose (v ∷ vs) h = PT.rec squash₁ (λ { (c , ec) → PT.map
        (λ { (cs , ecs) → (c ∷ cs)
           , cong₂ _∷_ (Σ≡Prop (λ z → snd (z ∈ˢ Lset lam)) ec) ecs })
        (choose vs (λ i → h (suc i))) })
```

For a code vector `cs`, `val-wit` identifies the value of `wit k ψ cs` with the least witness returned by the search. Since every code value belongs to the hull, the searched value belongs to the hull.

```agda
        (HSH.hull-member (fst v) (h zero))
      search-val : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k) (vs : Vec SL k)
                 → vals cs ≡ vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ Hull ⟩
      search-val k ψ cs vs e w =
        J (λ vs' e' → (w' : Sat k ψ vs') → ⟨ fst (search k ψ vs' w') ∈ˢ Hull ⟩)
```

The path induction transports the statement along the identification of the parameter vectors, and the witness code is judged inside the hull.

```agda
          (λ w' → subst (λ z → ⟨ fst z ∈ˢ Hull ⟩) (val-wit k ψ cs w') (inHull (wit k ψ cs)))
          e w
```

The code `wit 0 ⊥̇ []` has no satisfying witness, so its value follows the failure branch and is `∅`. As every code value lies in the hull, the junk value lies there as well.

```agda
      junk∈Hull : ⟨ ∅ ∈ˢ Hull ⟩
      junk∈Hull = subst (λ z → ⟨ fst z ∈ˢ Hull ⟩)
        (stuck-r no (search 0 ⊥̇ []) (λ _ → (∅ , HSH.∅∈Lsetα)) (lem (Sat 0 ⊥̇ [] , squash₁)))
        (inHull (wit 0 ⊥̇ []))
        where
```

No environment satisfies falsity: unpacking such a satisfaction proof would produce an element of the empty type.

```agda
        no : Sat 0 ⊥̇ [] → Empty.⊥
        no = PT.rec Empty.isProp⊥ (λ { (a , h) → Empty.rec* h })
```

Union into hull, second half: every member of every iterate lies in the hull, by induction on the iterate index. The base case is the start, whose members are hull members by the hull chapter.

```agda
    hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Hull ⟩
    hullStep⊆Hull zero z h = HSH.X⊆M z h
    hullStep⊆Hull (suc n) z h = PT.rec (snd (z ∈ˢ Hull)) read
      (out (hullStep n) (λ z' hz' → HSH.Hull⊆L z' (hullStep⊆Hull n z' hz')) z h)
      where
```

The step case reads a member of the successor iterate through the outward clause: it is an old member, already in the hull by the induction hypothesis; it is the junk value, already in the hull; or it is a searched value, handled next.

```agda
      read : Reads (hullStep n) z → ⟨ z ∈ˢ Hull ⟩
      read (inl h') = hullStep⊆Hull n z h'
      read (inr (inl e)) = subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e) junk∈Hull
      read (inr (inr (k , ψ , vs , w , from , e))) =
        subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e)
```

A searched value is matched with the code vector of its parameters, each parameter being a hull member by the induction hypothesis; the search then lies in the hull by `search-val`, and the equation transports that membership to `z`. The union of the iterates is named as the element of `L` presenting the hull.

```agda
          (PT.rec (snd (fst (search k ψ vs w) ∈ˢ Hull))
            (λ { (cs , ecs) → search-val k ψ cs vs ecs w })
            (choose vs (λ i → hullStep⊆Hull n (fst (lookup i vs)) (from i))))
    hullL : CS.S
    hullL = It.iterUnion
```

The hull as an element of `L` is the union of the iterates, and its membership description says its members are exactly the hull members. Forward: a member of the union lies at some iterate, hence in the hull.

```agda
    hullL-spec : fst hullL ≡ Hull
    hullL-spec = extensionalV {a = fst hullL} {b = Hull} (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : S) → ⟨ z ∈ˢ fst hullL ⟩ → ⟨ z ∈ˢ Hull ⟩
      fwd z h = PT.rec (snd (z ∈ˢ Hull))
```

The iterate index is consumed by the outward reading of the union, and the constructibility of the member is carried from the union, itself constructible by construction.

```agda
        (λ { (n , hn) → hullStep⊆Hull n z hn })
        (It.iterUnion-out (z , isL-trans {x = fst hullL} {y = z} h (snd hullL)) h)
```

Backward: a hull member is named by a code, whose value appears at the iterate indexed by the code's depth; the inward reading of the union admits it.

```agda
      bwd : (z : S) → ⟨ z ∈ˢ Hull ⟩ → ⟨ z ∈ˢ fst hullL ⟩
      bwd z h = PT.rec (snd (z ∈ˢ fst hullL))
        (λ { (c , ec) → It.iterUnion-in (depth c) zS
               (subst (λ t → ⟨ t ∈ˢ fst (hullStep (depth c)) ⟩) ec (hullStep-in c)) })
        (HSH.hull-member z h)
```

The named member is carried into the carrier: its constructibility follows from the hull being contained in the stage, whose element presentation supplies the certificate.

```agda
        where
        zS : CS.S
        zS = z , Lset→isL lam ordλ z (HSH.Hull⊆L z h)
```

The equality of underlying sets transports the union's constructibility onto the hull: the hull is an element of `L`. The first half of the chapter is now discharged in full, and the second module builds the definable step whose iteration was just consumed.

The step is built inside the stage, and its constants name objects of the stage: ordinality of `lam` comes from being an ordinal.

```agda
    M-isL : ⟨ isL HS.M ⟩
    M-isL = subst (λ t → ⟨ isL t ⟩) hullL-spec (snd hullL)
  module Build where
```

An ordinal of the hierarchy is constructible, which anchors the stage inside `L`.

```agda
    λ-isL : ⟨ isL lam ⟩
    λ-isL = isL-ord lam ordλ
```

`A` presents `Lset lam` together with its constructibility proof. It is the stage parameter used by the satisfaction graph and the coding of formulas over the stage.

```agda
    A : CS.S
    A = LsetS lam ordλ
```

The satisfaction graph over the stage supplies the satisfaction sets of all codes at once, with both readings; and definability over the stage interprets the constants of formulas as elements of the stage.

```agda
    module SM = SatGraph A using ( pairs; pairs-in; pairs-out; valOf; valOf≡ )
    module DA = DefOf (Lset lam) using ( ι; _⊨ᵐ_; 𝒮M )
```

The code set at the empty alphabet collects the codes of the parameter-free formulas. Such formulas may have free variables; what they lack is constants, and the free variables will be assigned by the parameter environments of the searches.

```agda
    C₀ : CS.S
    C₀ = AllCodes ∅ʟ
```

The stage's internal well-order is presented as an element of the model, the relation by which least witnesses will be compared.

```agda
    Rel : CS.S
    Rel = relL lam λ-isL ordλ
```

The strict well-order on the small carrier is read from that relation; its comparison is stated on carrier elements. The second component of a constructible ordered pair is again constructible, which the parameters of names will need.

```agda
    wL : SWO SL
    wL = orderAt lam ordλ
    relOf-at : SL → SL → Type (ℓ-suc ℓ)
    relOf-at = relOf wL
    pr-snd-isL : (a b : V ℓ) → ⟨ isL (pr a b) ⟩ → ⟨ isL b ⟩
```

The proof peels the ordered pair twice through singletons: membership in a pair puts the second component inside a singleton-pair nesting, and each peeling keeps constructibility by transitivity.

```agda
    pr-snd-isL a b h =
      isL-trans {x = ⁅ a , b ⁆} {y = b} (subst ⟨_⟩ (sym (pair-spec a b b)) ∣ inr refl ∣₁)
        (isL-trans {x = pr a b} {y = ⁅ a , b ⁆}
          (subst ⟨_⟩ (sym (pair-spec ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆)) ∣ inr refl ∣₁) h)
```

Numerals are presented as carrier elements: the finite ordinal together with its constructibility, which the key clause of the witness formula will quantify over.

```agda
    nn : ℕ → CS.S
    nn k = # k , numL k
```

Because the constant alphabet is empty, there is a unique interpretation `ε′` into the stage carrier. It allows a constant-free formula to be relabeled into the stage language without making any choices.

```agda
    ε′ : ⊥* {ℓ} → ⟪ Lset lam ⟫
    ε′ = Empty.rec*
    sat-bridge : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k)
               → (δ ⊨₀ χ) ≡ (δ DA.⊨ᵐ mapFo ε′ χ)
    sat-bridge k χ δ =
```

The bridge is a composition: the environments of the empty alphabet agree trivially because there is nothing to interpret, and the relabeling theorem identifies the external satisfaction of the relabeled formula with the stage's internal satisfaction.

```agda
        cong (λ κ → FOL.Semantics.At._⊨_ DA.𝒮M (⊥* {ℓ}) κ δ χ)
          (funExt (λ b → Empty.rec* b))
      ∙ sym (⊨-map DA.𝒮M ε′ DA.ι χ δ)
    opaque
      keyOf : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
```

The key of a parameter-free formula at the stage is the key of its relabeled form in the stage's code set. It is named once, so that later statements can mention it without reopening its construction.

```agda
      keyOf k χ = keyS A (mapFo ε′ χ)
```

The key belongs to the code set at the stage: a code of the relabeled formula is a code over the stage's alphabet, and the code set contains all of them.

```agda
      keyOf∈ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ keyOf k χ CS.∈ˢ AllCodes A ⟩
      keyOf∈ k χ = key∈AllCodes A (mapFo ε′ χ)
```

Although `keyOf` is opaque, the lemma `keyOf≡` exposes the exact equation with `keyS A (mapFo ε′ χ)`. Later proofs use this equation without unfolding the sealed definition.

```agda
      keyOf≡ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → keyOf k χ ≡ keyS A (mapFo ε′ χ)
      keyOf≡ k χ = refl
```

The underlying set of the sealed key is computed: it is the ordered pair of the numeral of the arity with the code of the relabeled formula. The proof composes the two relabelings of the formula, the empty alphabet followed by the stage's embedding, and the relabeling theorem identifies the result with the code the limit level records.

```agda
      keyOf-fst : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
                → fst (keyOf k χ) ≡ pr (# k) (fst (limitCode χ))
      keyOf-fst k χ = cong (pr (# k)) (cong VCode.⌜_⌝
        ( mapFo-comp ε′ ⟪ Lset lam ⟫↪ χ
        ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b)) ))
```

For each parameter-free formula, `Tof` is the satisfaction set selected by the satisfaction graph at the formula's sealed key. This fixed set represents satisfaction of that formula throughout the stage.

```agda
    Tof : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
    Tof k χ = SM.valOf (keyOf k χ) (keyOf∈ k χ)
```

The ordered pair of the key and its satisfaction set belongs to the satisfaction graph. Moreover, any carrier element with the same underlying set as the key selects the same satisfaction set: their constructibility witnesses are propositions, so equality of the underlying sets lifts to equality in the carrier and hence to equality of the selected values.

```agda
    Tof-pair : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
             → ⟨ pr (fst (keyOf k χ)) (fst (Tof k χ)) ∈ˢ fst SM.pairs ⟩
    Tof-pair k χ = SM.pairs-in (keyOf k χ) (keyOf∈ k χ)
    valOf-same : (x : CS.S) (m : ⟨ x CS.∈ˢ AllCodes A ⟩) (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
               → fst x ≡ fst (keyOf k χ) → SM.valOf x m ≡ Tof k χ
```

The proof runs by path induction on the equation of underlying sets, with the propositionality of code-set membership absorbing the difference of membership proofs. Only the underlying sets matter, so the transport is silent about everything else.

```agda
    valOf-same x m k χ e =
      J (λ x' e' → (m' : ⟨ x' CS.∈ˢ AllCodes A ⟩) → SM.valOf x m ≡ SM.valOf x' m')
        (λ m' → cong (SM.valOf x) (snd (x CS.∈ˢ AllCodes A) m m'))
        (S≡ {x = x} {y = keyOf k χ} e) (keyOf∈ k χ)
    sat-at : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k) (z : CS.S)
```

Membership in a satisfaction set is now computed as the stage's own satisfaction. The bridge composes three identifications: the sealed name agrees with the key it was built from; the value at the key is read externally by the uniform satisfaction theorem; and the external satisfaction of the relabeled formula is the stage's internal satisfaction by the relabeling bridge.

```agda
           → fst z ≡ graph A δ → (z CS.∈ˢ Tof k χ) ≡ (δ ⊨₀ χ)
    sat-at k χ δ z qz =
        cong (z CS.∈ˢ_) (SM.valOf≡ (keyOf k χ) (keyOf∈ k χ))
      ∙ val-sat A (mapFo ε′ χ) (keyOf k χ) (keyOf∈ k χ) (cong fst (keyOf≡ k χ)) δ z qz
      ∙ sym (sat-bridge k χ δ)
```

The key recognizer is a formula. It says that the value in slot `s` belongs to the stage's code set and is the ordered pair of the successor of the numeral in slot `a` with some code. Thus, when slot `a` contains `# k`, it recognizes a key of arity `k+1` for a parameter-free formula. Parameter-free here means that the constant domain is empty; the formula may still have free variables.

```agda
    opaque
      keyIn : ∀ {n} → Fin n → Fin n → Formula CS.S n
      keyIn s a = (var s ∈̇ con C₀)
                ∧̇ ∃̇ ( sucAtL (suc a) zero
                     ∧̇ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) )
```

The readings are stated at a variable environment, for a fixed arity `k` whose numeral is named at slot `a`. Fixing the arity in advance is what makes the two readings equations about codes rather than searches through them.

```agda
    module KeyIn {n : ℕ} (s a : Fin n) (γ : CS.S ^ n) (k : ℕ)
                 (qa : fst (lookup a γ) ≡ # k) where
```

The formula is opened for computation at its own slots, since the readings must compute through the conjunctions and existentials of the definition.

```agda
      opaque
        unfolding keyIn
```

The introduction builds the satisfaction from three data: the code-set membership of `s`, an element `c` of the hierarchy, and the equation identifying `s` with the pair of the successor numeral and `c`. The numeral, the successor clause and the pair clause are filled in order.

```agda
        keyIn-in : ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩ → (c : V ℓ)
                 → fst (lookup s γ) ≡ pr (# (suc k)) c → ⟨ γ ⊨ keyIn s a ⟩
        keyIn-in h c q = h , ∣ numAt , ( hsuc , ∣ cS , hpr ∣₁ ) ∣₁
          where
          numAt : CS.S
```

The numeral is presented as a carrier element, and the code `c` is lifted to one as well. From the equation identifying `s` with the ordered pair and from the constructibility of `s`, `pr-snd-isL` extracts the constructibility of the pair's second component `c`.

```agda
          numAt = nn (suc k)
          cS : CS.S
          cS = c , pr-snd-isL (# (suc k)) c
                     (subst (λ u → ⟨ isL u ⟩) q (isL-trans h (snd C₀)))
          hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
```

The successor clause is transported from the equation of the numeral at slot `a`, and the pair clause from the equation of `s`, each through the adequacy of its coding operator. Both transports are exactly what converts host equations into satisfaction.

```agda
          hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
            (cong sucV (sym qa))
          hpr : ⟨ (cS ∷ numAt ∷ γ) ⊨ prAtL (suc (suc s)) (suc zero) zero ⟩
          hpr = subst ⟨_⟩
            (sym (prAtL-adequate (suc (suc s)) (suc zero) zero (cS ∷ numAt ∷ γ))) q
```

The elimination recovers the two data: the code-set membership of `s`, and the truncated statement that `s` is the pair of the successor numeral with some code. The existential chain of the formula is unpacked step by step.

```agda
        keyIn-out : ⟨ γ ⊨ keyIn s a ⟩
                  → ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩
                  × ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
        keyIn-out (h , hk) = h , PT.rec squash₁ atNum hk
          where
```

The intermediate binder names the numeral at the successor slot, and the adequacy of the successor coding converts its satisfaction into the equation of the underlying sets.

```agda
          atNum : Σ[ z ∈ CS.S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                                × ⟨ (z ∷ γ) ⊨ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) ⟩ )
                → ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
          atNum (z , (hs , hc)) = PT.map
            (λ { (c , hp) → fst c
```

The inner existential then yields the code `c` with a satisfaction of the pair clause; the adequacy transports it to the equation of pairs, composed with the identifications of the numeral and its successor. The equation recovered is exactly the truncated statement sought.

```agda
               , ( subst ⟨_⟩ (prAtL-adequate (suc (suc s)) (suc zero) zero (c ∷ z ∷ γ)) hp
                 ∙ cong (λ u → pr u (fst c)) (qz ∙ cong sucV qa) ) })
            hc
            where
            qz : fst z ≡ sucV (fst (lookup a γ))
```

The seven-slot environment is now assembled: the satisfaction table, the extended environment, the parameter environment, the key, the numeral, the witness and the current set, in the order the body will read them.

```agda
            qz = subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs
    Env : CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S ^ 7
    Env T e' e s k w Z = T ∷ e' ∷ e ∷ s ∷ k ∷ w ∷ Z ∷ []
```

The minimality subformula quantifies over the stage's alphabet. It says: if some extension of the parameter environment by a stage element satisfies the coded formula, then no such element stands before the witness in the stage's well-order. It is bounded by the constant `A`, so the quantifier runs over the stage and not over the universe.

```agda
    opaque
      minFo : Formula CS.S 7
      minFo = ∀̇∈ (con A)
        ( (∃̇ ( consAtL i0 i1 i4 ∧̇ (var i0 ∈̇ var i2) )) ⇒̇ ¬̇ (appC Rel i0 i6) )
```

The body conjuncts now say, in order: the numeral lies in the internal `ωʟ`; `s` is a key of arity one more; the parameter environment codes a vector over the current set; the extended environment extends it by the witness.

```agda
      bodyFo : Formula CS.S 7
      bodyFo = (var i4 ∈̇ con ωʟ)
            ∧̇ ( keyIn i3 i4
            ∧̇ ( envOverAt i2 i4 i6
            ∧̇ ( consAtL i1 i5 i2
```

The remaining conjuncts say: the pair of the key and the table lies in the satisfaction graph; the extended environment lies in the table; the witness lies in the stage; and minimality holds. There are eight conjuncts in all. The stage bounds the witness and the candidates used by minimality, while the coding conjuncts supply the auxiliary objects that connect the record to the satisfaction table.

```agda
            ∧̇ ( appC SM.pairs i3 i0
            ∧̇ ( (var i1 ∈̇ var i0)
            ∧̇ ( (var i5 ∈̇ con A)
            ∧̇ minFo ))))))
```

Fix the seven objects `T,e',e,s,k,w,Z`. At their joint environment, the body is a concrete proposition whose eight conjuncts can be projected and assembled in both directions.

```agda
    module BodyRd (T e' e s k w Z : CS.S) where
```

The seven-slot environment is recorded, and the host-side minimality is stated relative to a family presenting the parameter environment: no extension by a smaller stage element lands in the satisfaction table while ranking before the witness.

```agda
      γ₇ : CS.S ^ 7
      γ₇ = Env T e' e s k w Z
      Min : {m : ℕ} (g : Fin m → V ℓ) → Type (ℓ-suc ℓ)
      Min g = (w' : CS.S) → ⟨ fst w' ∈ˢ fst A ⟩ → (e'' : CS.S)
            → fst e'' ≡ env (cons (fst w') g) → ⟨ fst e'' ∈ˢ fst T ⟩
```

The clause ends in the empty type: minimality is refutation, and the data of a counterexample, a smaller extension with the pair membership, is exactly what must be impossible.

```agda
            → ⟨ pr (fst w') (fst w) ∈ˢ fst Rel ⟩ → Empty.⊥
```

Because the body is a nested conjunction, each of its eight conditions can be read by projection, while a proof of all eight conditions can be assembled back into satisfaction of the body.

```agda
      opaque
        unfolding bodyFo
```

The first reading projects the numeral clause. Membership in the internal `ωʟ` lets us recover a natural number `n`; together with the key clause, this identifies `s` as a key of arity `n+1`, with one slot reserved for the witness.

```agda
        b-num : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst k ∈ˢ fst ωʟ ⟩
        b-num h = h .fst
```

The second projection is the key clause: at slots `s` and `k`, the formula asserts that `s` is a recognized key whose arity is one more than the numeral `k`.

```agda
        b-key : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩
        b-key h = h .snd .fst
```

The third reading projects the environment clause: the parameter environment codes a vector over the current set at the recorded slots.

```agda
        b-env : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
        b-env h = h .snd .snd .fst
```

The fourth reading states the extension equation, transported along the adequacy of the cons coding: the extended environment is the parameter environment extended by the witness.

```agda
        b-cons : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g
               → ⟨ γ₇ ⊨ bodyFo ⟩ → fst e' ≡ env (cons (fst w) g)
        b-cons g hE h =
          subst ⟨_⟩ (consAtL-adequate i1 i5 i2 γ₇ g hE) (h .snd .snd .snd .fst)
```

The fifth reading states the graph membership of the pair of the key and the table, transported along the adequacy of the application coding.

```agda
        b-tab : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩
        b-tab h = subst ⟨_⟩ (appC-adequate SM.pairs i3 i0 γ₇) (h .snd .snd .snd .snd .fst)
```

The sixth reading is the membership of the extended environment in the satisfaction table, the fact that says the witness satisfies the coded formula at the parameters.

```agda
        b-mem : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst e' ∈ˢ fst T ⟩
        b-mem h = h .snd .snd .snd .snd .snd .fst
```

The seventh projection states that the witness belongs to the stage `A`, so the witness and all candidates compared with it range over the same stage.

```agda
        b-stage : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst w ∈ˢ fst A ⟩
        b-stage h = h .snd .snd .snd .snd .snd .snd .fst
```

The eighth reading is the minimality clause, read refutationally: a smaller candidate with a satisfying extension would contradict the bounded quantifier, after the relation entry is transported through the application's adequacy.

```agda
        b-min : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g → ⟨ γ₇ ⊨ bodyFo ⟩ → Min g
        b-min g hE h w' hw' e'' qe hm hr =
          lower (h .snd .snd .snd .snd .snd .snd .snd w' hw' ∣ e'' , (hc , hm) ∣₁
            (subst ⟨_⟩ (sym (appC-adequate Rel i0 i6 (w' ∷ γ₇))) hr))
          where
```

The cons clause of the candidate extension is transported from its host equation, exactly mirroring the coding of the extension in the inner existential.

```agda
          hc : ⟨ (e'' ∷ w' ∷ γ₇) ⊨ consAtL i0 i1 i4 ⟩
          hc = subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE)) qe
```

The filling reading assembles a satisfaction of the body from its eight components: the numeral clause, the key clause, the environment clause, the extension equation, the graph membership, the table membership, the stage membership, and minimality.

```agda
        b-fill : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g
               → ⟨ fst k ∈ˢ fst ωʟ ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
               → fst e' ≡ env (cons (fst w) g) → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩
               → ⟨ fst e' ∈ˢ fst T ⟩ → ⟨ fst w ∈ˢ fst A ⟩ → Min g
               → ⟨ γ₇ ⊨ bodyFo ⟩
```

Five conjuncts are inserted directly. The extension equation and the graph entry are converted back into satisfactions by the reversed adequacy equations for `consAtL` and `appC`; minimality is supplied in the final clause.

```agda
        b-fill g hE c1 c2 c3 c4 c5 c6 c7 mn =
          c1 , c2 , c3
          , subst ⟨_⟩ (sym (consAtL-adequate i1 i5 i2 γ₇ g hE)) c4
          , subst ⟨_⟩ (sym (appC-adequate SM.pairs i3 i0 γ₇)) c5
          , c6 , c7
```

Minimality is filled by eliminating its truncated counterexample into the empty type: the counterexample is transported through both adequacy equations and handed to the refutation, so the filler needs only the contradiction, not a construction.

```agda
          , λ w' hw' hex hr → lift (PT.rec Empty.isProp⊥
              (λ { (e'' , (hc , hm)) → mn w' hw' e''
                     (subst ⟨_⟩ (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE) hc) hm
                     (subst ⟨_⟩ (appC-adequate Rel i0 i6 (w' ∷ γ₇)) hr) })
              hex)
```

The witness formula wraps the body in five nested existentials, one per object: the satisfaction table, the extended environment, the parameter environment, the key, and the numeral. Satisfaction of the formula at `w` and `Z` says exactly that a complete record for a least witness at `w` over `Z` exists.

```agda
    opaque
      witFo : Formula CS.S 2
      witFo = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ bodyFo))))
```

The inward reading injects the five objects and the body satisfaction through the five binders, each injection carrying one object into its slot.

```agda
      witFo-in : (w Z T e' e s k : CS.S) → ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩
               → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
      witFo-in w Z T e' e s k h = ∣ k , ∣ s , ∣ e , ∣ e' , ∣ T , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
```

The outward reading eliminates the five truncated existentials in binder order. At the innermost layer, `PT.map` merely rearranges the recovered objects into the displayed dependent tuple, leaving the body satisfaction unchanged.

```agda
      witFo-out : (w Z : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
                → ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] Σ[ k ∈ CS.S ]
                     ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩ ∥₁
      witFo-out w Z = PT.rec squash₁ (λ { (k , hk) → PT.rec squash₁ (λ { (s , hs) →
        PT.rec squash₁ (λ { (e , he) → PT.rec squash₁ (λ { (e' , he') → PT.map
```

Unwrapping `witFo` yields a table, an extended environment, a parameter environment, a key, and a numeral whose joint environment satisfies the body.

```agda
          (λ { (T , hT) → T , e' , e , s , k , hT }) he' }) he }) hs }) hk })
```

## The least-witness relation at a fixed key and environment

When `e` and `s` are fixed, `LeastWitness Z e s z` retains the truncated existence of the remaining table, extended environment, and numeral.

```agda
    LeastWitness : CS.S → CS.S → CS.S → CS.S → Type (ℓ-suc ℓ)
    LeastWitness Z e s z =
      ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
          ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩ ∥₁
```

To bind the table, extended environment, and numeral while retaining six ambient variables, the body is renamed from seven slots to nine. The map places its seven meaningful entries at `T,e',e,s,k,z,Z`.

```agda
    private
      ρ₉ : Fin 7 → Fin 9
      ρ₉ zero = i0
      ρ₉ (suc zero) = i1
      ρ₉ (suc (suc zero)) = i4
```

The remaining four cases place the key `s`, the numeral `k`, the candidate `z`, and the current set `Z`. The final slots `p` and `q` are unused, so satisfaction is independent of their values.

```agda
      ρ₉ (suc (suc (suc zero))) = i5
      ρ₉ (suc (suc (suc (suc zero)))) = i2
      ρ₉ (suc (suc (suc (suc (suc zero))))) = i6
      ρ₉ (suc (suc (suc (suc (suc (suc zero)))))) = i3
```

`Γ₉` displays this placement, and each agreement with the original seven-slot environment is judgmental reflexivity.

```agda
      Γ₉ : (T e' k Z e s z p q : CS.S) → CS.S ^ 9
      Γ₉ T e' k Z e s z p q = T ∷ e' ∷ k ∷ Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []
```

The agreements say that, at each renamed slot, the two environments carry the same carrier element. The first three are proved by reflexivity, one per renamed position.

```agda
      ag₉ : (T e' k Z e s z p q : CS.S)
          → Ren.Agrees ρ₉ (Γ₉ T e' k Z e s z p q) (Env T e' e s k z Z)
      ag₉ T e' k Z e s z p q zero = refl
      ag₉ T e' k Z e s z p q (suc zero) = refl
      ag₉ T e' k Z e s z p q (suc (suc zero)) = refl
```

The remaining four agreements are again reflexivity, one per slot; every agreement is a computation, which is what makes the renaming usable inside a satisfaction.

```agda
      ag₉ T e' k Z e s z p q (suc (suc (suc zero))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc zero)))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc zero))))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc (suc zero)))))) = refl
```

The renamed body is the body formula pushed through the slot map, living over nine slots while saying the same thing as before.

```agda
      body₉ : Formula CS.S 9
      body₉ = renameFo ρ₉ bodyFo
```

The reading equation says that satisfying the renamed body over the nine-slot environment is the same proposition as satisfying the body over the seven-slot environment.

```agda
      body₉-read : (T e' k Z e s z p q : CS.S)
                 → ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩
                 ≡ ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩
      body₉-read T e' k Z e s z p q =
        cong ⟨_⟩ (Ren.⊨-rename ρ₉ bodyFo (Γ₉ T e' k Z e s z p q)
```

The proof is the renaming theorem applied with the slot agreement, transported under the bracket of satisfaction.

```agda
                    (Env T e' e s k z Z) (ag₉ T e' k Z e s z p q))
```

The least-witness formula wraps the renamed body in three more existentials: the numeral, the extended environment, and the table. Satisfaction at the six-slot environment says that a least-witness record exists for the candidate at the current set, key and parameter environment.

```agda
    opaque
      leastWitnessFo : Formula CS.S 6
      leastWitnessFo = ∃̇ (∃̇ (∃̇ body₉))
```

The inward reading eliminates the truncated least-witness data and injects the three objects, transporting the body satisfaction along the reading equation of the renamed body.

```agda
      leastWitness-in : (Z e s z p q : CS.S) → LeastWitness Z e s z
                      → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
      leastWitness-in Z e s z p q = PT.rec (snd ((Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo))
        (λ { (T , e' , k , h) →
          ∣ k , ∣ e' , ∣ T , transport (sym (body₉-read T e' k Z e s z p q)) h ∣₁ ∣₁ ∣₁ })
```

The outward reading eliminates the three nested existentials in order, each into the truncated continuation, so the formula satisfaction becomes a least-witness record again.

```agda
      leastWitness-out : (Z e s z p q : CS.S)
                       → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
                       → LeastWitness Z e s z
      leastWitness-out Z e s z p q = PT.rec squash₁ at₁
        where
```

The innermost elimination rebuilds the least-witness data from the named table, extended environment and numeral, transporting the body satisfaction along the reading equation. The two outer eliminations supply the bound objects required by this construction.

```agda
        at₃ : (k e' : CS.S) → Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩
            → LeastWitness Z e s z
        at₃ k e' (T , h) = ∣ T , e' , k , transport (body₉-read T e' k Z e s z p q) h ∣₁
        at₂ : (k : CS.S) → Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁
            → LeastWitness Z e s z
```

At this point two nested truncations remain: the outer one hides the extension environment `e'`, and the inner one hides the table `T`. The two eliminations expose them in turn, after which `at₃` transports the renamed body proof back to a `LeastWitness`.

```agda
        at₂ k (e' , h) = PT.rec squash₁ (at₃ k e') h
        at₁ : Σ[ k ∈ CS.S ] ∥ Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ]
                ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁ ∥₁
            → LeastWitness Z e s z
        at₁ (k , h) = PT.rec squash₁ (at₂ k) h
```

The numeral slot carries a member of the internal `ω`, and `decode-num` decodes it: a truncated natural number `n` together with the equation identifying the entry with the ambient numeral `# n`. Decoding is the bridge between the internal numbering and the natural-number bookkeeping of the witness data.

```agda
    private
      decode-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
      decode-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
        (subst ⟨_⟩ (ω-specL q) h)
```

`LeastWitnessData` is the honest data behind a least witness: a natural number `n`, an assignment `g` of `n` indices into the presentation of `Z`, the equation saying that `e` is the environment naming those values, and the stage membership placing `s` in `Lset ω`.

```agda
    LeastWitnessData : CS.S → CS.S → CS.S → Type (ℓ-suc ℓ)
    LeastWitnessData Z e s =
      Σ[ n ∈ ℕ ] Σ[ g ∈ (Fin n → ⟪ fst Z ⟫) ]
        ((fst e ≡ env (λ i → ⟪ fst Z ⟫↪ (g i))) × (⟨ fst s ∈ Lset ω ⟩))
```

The theorem `leastWitness-data` says that a formula-level least witness determines, up to propositional truncation, a natural arity, an indexed parameter environment over `Z`, and a proof that the key lies in `Lset ω`.

```agda
    opaque
      leastWitness-data : (Z e s z : CS.S) → LeastWitness Z e s z
                        → ∥ LeastWitnessData Z e s ∥₁
      leastWitness-data Z e s z = PT.rec squash₁ body
        where
```

The body of the conversion consumes the body satisfaction: it unpacks into the table `T`, the extension `e'`, the key `k`, and the body proof, and the numeral entry of the key is decoded first.

```agda
        body : Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
                 ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩
             → ∥ LeastWitnessData Z e s ∥₁
        body (T , e' , k , hb) = PT.map at (decode-num k (BodyRd.b-num T e' e s k z Z hb))
          where
```

With the numeral `n` and the equation naming the key, the data assembles: the length `n`, the recovered assignment `g`, the recovery equation for the environment, and the stage membership of `s`. The seven-entry context is named once so the recovery can address its slots.

```agda
          at : Σ[ n ∈ ℕ ] (fst k ≡ # n) → LeastWitnessData Z e s
          at (n , qk) = n , R.g , R.recovers , s∈Lω
            where
            γ : CS.S ^ 7
            γ = Env T e' e s k z Z
```

The environment clause recovers an assignment `g` of indices in `Z` and proves that `e` is the graph of their values. Independently, the key clause says that `s` is a code and is an ordered pair of the successor arity numeral with a formula code.

```agda
            module R = Recover Z n γ i2 i4 i6 qk refl (BodyRd.b-env T e' e s k z Z hb)
              using ( g; recovers )
            kr : ⟨ fst s ∈ fst C₀ ⟩ × ∥ Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) ∥₁
            kr = KeyIn.keyIn-out i3 i4 γ n qk (BodyRd.b-key T e' e s k z Z hb)
            s∈Lω : ⟨ fst s ∈ Lset ω ⟩
```

The stage membership of the key's value is the last piece of the data. It is proved from the pair equation: the second component `c` of the key is a code, and codes are constructible by the limit stage.

```agda
            s∈Lω = PT.rec (snd (fst s ∈ Lset ω)) read (kr .snd)
              where
              read : Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) → ⟨ fst s ∈ Lset ω ⟩
              read (c , qs) = PT.rec (snd (fst s ∈ Lset ω))
                (λ { (χ , qc) → subst (λ w → ⟨ w ∈ Lset ω ⟩) (sym qs)
```

Both components of the key therefore live in `Lset ω`: the successor numeral belongs to the limit by the numerals' membership, and pairs of members of a limit stage stay in the limit. Transporting along the pair equation places `s` in `Lset ω`, completing `LeastWitnessData`.

```agda
                       (pr∈limit (# (suc n)) c (numeral∈limit (suc n))
                         (subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym qc) (snd (limitCode χ)))) })
                (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ fst C₀ ⟩) qs (kr .fst)))
```

The outward reading of the witness formula now assembles: satisfaction of `witFo` at `(z, Z)` unpacks into a table, an extension, a key, and the body proof, and the body proof converts into a truncated `LeastWitness`. This is the form in which the satisfaction of the Skolem clause is consumed.

```agda
      witFo-leastWitness : (z Z : CS.S) → ⟨ (z ∷ Z ∷ []) ⊨ witFo ⟩
                         → ∥ Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] LeastWitness Z e s z ∥₁
      witFo-leastWitness z Z h = PT.map
        (λ { (T , e' , e , s , k , hb) → e , s , ∣ T , e' , k , hb ∣₁ })
        (witFo-out z Z h)
```

For comparing two witnesses, we retain seven of the eight body clauses: the numeral, environment, extension, table, membership, stage, and minimality clauses. The key clause is not needed here, because the two witnesses already share `s`, and uniqueness of the value associated with that key identifies their tables.

```agda
    private
      module WitnessBody (z T e' e s k Z : CS.S)
        (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩) where
        module Rd = BodyRd T e' e s k z Z
          using ( b-num; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
```

Two retained clauses immediately give that the extended environment lies in the table and that the witness lies in `Lset lam`. Once the key numeral is identified with `# n`, the environment clause also recovers an `n`-tuple of indices from `Z`.

```agda
        h6 = Rd.b-mem hb
        h7 = Rd.b-stage hb
        module AtNum (n : ℕ) (qk : fst k ≡ # n) where
          module R = Recover Z n (Env T e' e s k z Z) i2 i4 i6 qk refl (Rd.b-env hb)
            using ( g; recovers )
```

The recovered indices name their ambient values through the presentation of `Z`, and the recovery equation says that the extension environment names exactly these ambient values, in the order the indices list them.

```agda
          g′ : Fin n → V ℓ
          g′ i = ⟪ fst Z ⟫↪ (R.g i)
          hE : fst e ≡ env g′
          hE = R.recovers
```

To prove uniqueness, take two body witnesses with the same `Z`, parameter environment `e`, and formula key `s`. Decoding the first arity numeral fixes a common length `n` for the recovered parameter sequence.

```agda
      module WitnessUnique (Z e s z T e' k : CS.S)
        (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩)
        (z' T₂ e'₂ k₂ : CS.S)
        (hb₂ : ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩)
        (n : ℕ) (qk : fst k ≡ # n) where
```

The stage clauses turn `z` and `z'` into elements of `Lset lam`. They can therefore be compared by the well-order of that stage, while the decoded first witness supplies the common parameter sequence used for both bodies.

```agda
        module A₁ = WitnessBody z T e' e s k Z hb
        module A₂ = WitnessBody z' T₂ e'₂ e s k₂ Z hb₂
        module N = A₁.AtNum n qk
        zS : SL
        zS = fst z , A₁.h7
```

The second element is packaged likewise. The extension equations say that each body's environment is the parameter environment extended by its own witnessed element: `e'` names `z` consed onto the recovered values, and `e'₂` names `z'` the same way.

```agda
        z'S : SL
        z'S = fst z' , A₂.h7
        e'≡ : fst e' ≡ env (cons (fst z) N.g′)
        e'≡ = A₁.Rd.b-cons N.g′ N.hE hb
        e'₂≡ : fst e'₂ ≡ env (cons (fst z') N.g′)
```

The two table slots are then shown to agree. Both bodies assert that the pair of the key `s` and their table belongs to the table family's pairs, and the injectivity of the code naming forces two tables paired with the same key to be equal.

```agda
        e'₂≡ = A₂.Rd.b-cons N.g′ N.hE hb₂
        T≡ : fst T ≡ fst T₂
        T≡ =
          let p = SM.pairs-out s T (A₁.Rd.b-tab hb)
              q = SM.pairs-out s T₂ (A₂.Rd.b-tab hb₂)
```

The table equality is assembled from the outward readings of the two table clauses: each table is the value named by the key, and the injectivity of code naming identifies the two keys' code indices. The statement `not-below` is then prepared: a strictly smaller constructible element with its own body witness cannot have its extension inside the other's table.

```agda
          in snd p ∙ cong (λ m → fst (SM.valOf s m))
            (snd (fst s ∈ fst (AllCodes A)) (fst p) (fst q)) ∙ sym (snd q)
        not-below : (a b : CS.S) (ha : ⟨ fst a ∈ fst A ⟩) (hb' : ⟨ fst b ∈ fst A ⟩)
                    (Ta e'a ka : CS.S) (hba : ⟨ Env Ta e'a e s ka a Z ⊨ bodyFo ⟩)
                    (e'b : CS.S) → fst e'b ≡ env (cons (fst b) N.g′) → ⟨ fst e'b ∈ fst Ta ⟩
```

If a constructible candidate lies below one witness and its extended environment belongs to the same table, the minimality clause gives a contradiction. The stage well-order supplies the internal comparison relation needed by that clause.

```agda
                  → relOf wL (fst b , hb') (fst a , ha) → Empty.⊥
        not-below a b ha hb' Ta e'a ka hba e'b qe hm b<a =
          BodyRd.b-min Ta e'a e s ka a Z N.g′ N.hE hba b hb' e'b qe hm
            (relL-fill lam λ-isL ordλ (fst b , hb') (fst a , ha) b<a)
        result : fst z ≡ fst z'
```

The result follows by the trichotomy of the internal well-order on the two packaged witnesses. If `z` were below `z'`, the smaller element `z` would contradict the minimality recorded by `z'`'s body, the shared table supplied through the table equality.

```agda
        result = go (SWO.tri∙ wL zS z'S)
          where
          go : Tri∙ (relOf wL zS z'S) (zS ≡ z'S) (relOf wL z'S zS) → fst z ≡ fst z'
          go (tri-lt h) = Empty.rec (not-below z' z A₂.h7 A₁.h7 T₂ e'₂ k₂ hb₂ e' e'≡
                        (subst (λ t → ⟨ fst e' ∈ t ⟩) T≡ A₁.h6) h)
```

If the two packaged witnesses are equal, their underlying sets are equal. The remaining strict case is symmetric: if `z'` lies below `z`, the minimality of `z` gives a contradiction.

```agda
          go (tri-eq q) = cong fst q
          go (tri-gt h) = Empty.rec (not-below z z' A₁.h7 A₂.h7 T e' k hb e'₂ e'₂≡
                        (subst (λ t → ⟨ fst e'₂ ∈ t ⟩) (sym T≡) A₂.h6) h)
```

Uniqueness of least witnesses is assembled: two witnesses for the same `Z`, `e` and `s` have equal underlying elements. The two truncations are consumed together, the goal being an equality in an h-set.

```agda
    opaque
      leastWitness-unique : (Z e s z z' : CS.S) → LeastWitness Z e s z
                          → LeastWitness Z e s z' → fst z ≡ fst z'
      leastWitness-unique Z e s z z' = PT.rec2 (setIsSet (fst z) (fst z')) inner
        where
```

The inner lemma receives both unpacked body witnesses: tables, extensions, keys, and body satisfactions for the two candidate elements `z` and `z'`.

```agda
        inner : (Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
                   ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩)
              → (Σ[ T₂ ∈ CS.S ] Σ[ e'₂ ∈ CS.S ] Σ[ k₂ ∈ CS.S ]
                   ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩)
              → fst z ≡ fst z'
```

The first key is decoded to a numeral, allowing the preceding uniqueness argument to run at that arity. The same decoding principle is recorded as `ω-num`: every member of the internal `ω` is, up to truncation, an ambient numeral `# n`.

```agda
        inner (T , e' , k , hb) (T₂ , e'₂ , k₂ , hb₂) =
          PT.rec (setIsSet (fst z) (fst z'))
            (λ { (n , qk) → WitnessUnique.result Z e s z T e' k hb z' T₂ e'₂ k₂ hb₂ n qk })
            (decode-num k (BodyRd.b-num T e' e s k z Z hb))
    ω-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
```

The decoding maps a member of the internal `ω` to a natural number with the numeral equation, and `vecOf` turns a function on `Fin k` into a length-`k` vector of constructible elements, the form the satisfaction clauses consume.

```agda
    ω-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
      (subst ⟨_⟩ (ω-specL q) h)
    vecOf : {k : ℕ} → (Fin k → SL) → Vec SL k
    vecOf {zero} f = []
    vecOf {suc k} f = f zero ∷ vecOf (λ i → f (suc i))
```

Lookups in `vecOf f` recover `f` entry by entry. Now fix a set `Z`, an arity `k`, a formula `χ` with one witness variable and `k` parameter variables, a parameter vector `vs` drawn from `Z`, and evidence that `χ` has a witness at `vs`.

```agda
    lookup-vecOf : {k : ℕ} (f : Fin k → SL) (i : Fin k) → lookup i (vecOf f) ≡ f i
    lookup-vecOf {suc k} f zero = refl
    lookup-vecOf {suc k} f (suc i) = lookup-vecOf (λ j → f (suc j)) i
    module Least (Z : CS.S) (k : ℕ) (χ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
                 (from : From Z vs) (w₀ : Sat k χ vs) where
```

The predicate to be minimized says of an element `a` that the extended environment `(a ∷ vs)` satisfies `χ`. It is packaged as a proposition, so it can serve as the leastness predicate of a well-order.

```agda
      P : SL → hProp (ℓ-suc ℓ)
      P a = (a ∷ vs) ⊨₀ χ
```

The least witness `a` is selected by the least-element search along the internal well-order of `L`, applied to this predicate and the nonemptiness record.

```agda
      a : SL
      a = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .fst
```

Its leastness data is kept in full: `a` satisfies the predicate, and no smaller element of the well-order satisfies it.

```agda
      a-least : IsLeast wL P a
      a-least = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .snd
```

Because the chosen witness `a` belongs to `Lset lam`, it is constructible and can be viewed as an element `aS` of the constructible carrier. For each parameter position, `g` chooses an index in the presentation of `Z` naming that parameter.

```agda
      aS : CS.S
      aS = fst a , Lset→isL lam ordλ (fst a) (snd a)
      g : Ix Z k
      g i = fiber (fst Z) (from i) .fst
```

The naming equation says that each parameter's index presents exactly that parameter: the embedded index equals the parameter as an element of `L`.

```agda
      g-val : (i : Fin k) → ⟪ fst Z ⟫↪ (g i) ≡ fst (lookup i vs)
      g-val i = fiber (fst Z) (from i) .snd
```

The ambient values of the parameters are collected in `g′`, one per slot, so that the parameter environment can be described both internally and ambiently.

```agda
      g′ : Fin k → V ℓ
      g′ i = ⟪ fst Z ⟫↪ (g i)
```

The parameter environment `e` is the internal graph of these values over `Z`, and `ext b` is the extension environment for a candidate `b`: the parameters with `b` consed in front.

```agda
      e : CS.S
      e = envS Z g
      ext : SL → CS.S
      ext b = envFor A (b ∷ vs)
```

The extension's graph equation says that its underlying set is the graph of the candidate consed onto the ambient parameter values, the two readings of the extension being identified entry by entry.

```agda
      ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′)
      ext-graph b = envFor-graph A (b ∷ vs)
        ∙ cong env (funExt (λ { zero → refl ; (suc i) → sym (g-val i) }))
```

The extension belongs to the satisfaction table of `χ` at arity `suc k` exactly when the extended environment satisfies `χ`. The table here is the one for this formula alone, and the equation is what lets membership in the table be traded for satisfaction.

```agda
      ext-sat : (b : SL) → (ext b CS.∈ˢ Tof (suc k) χ) ≡ ((b ∷ vs) ⊨₀ χ)
      ext-sat b = sat-at (suc k) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs))
```

The key `sS` names the formula and its arity: it is the pair by which the table family indexes the table of `χ`.

```agda
      sS : CS.S
      sS = keyOf (suc k) χ
```

The table `T` is the satisfaction table of `χ` at arity `suc k`, the set in which satisfying extensions are collected.

```agda
      T : CS.S
      T = Tof (suc k) χ
```

The seven-entry environment `γ₇` assembles the whole picture: the table, the extension by the least witness, the parameter environment, the key, the numeral of the arity, the packaged witness, and the base set `Z`.

```agda
      γ₇ : CS.S ^ 7
      γ₇ = Env T (ext a) e sS (nn k) aS Z
```

The first clause records that the numeral of the arity belongs to the internal `ω`, the length of an environment being a natural number.

```agda
      c1 : ⟨ γ₇ ⊨ (var i4 ∈̇ con ωʟ) ⟩
      c1 = #∈ω k
```

The key clause says that the key belongs to the code set and pairs the successor numeral with the code of `χ`; the code is a free code, and free codes live in the limit stage of `ω`.

```agda
      c2 : ⟨ γ₇ ⊨ keyIn i3 i4 ⟩
      c2 = KeyIn.keyIn-in i3 i4 γ₇ k refl
        (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) (sym (keyOf-fst (suc k) χ)) (freeCode-in (suc k) χ))
        (fst (limitCode χ)) (keyOf-fst (suc k) χ)
```

The environment clause says that the parameter environment is an environment of length `nn k` over `Z`, with the values `g′`; it is transported from the environment lemma of `e` to the seven-entry context.

```agda
      c3 : ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
      c3 = envOverAt-transport (Z ∷ nn k ∷ e ∷ []) γ₇ i2 i1 i0 i2 i4 i6 refl refl refl
             (envOver Z g)
```

The extension equation repeats that the extension by the least witness is the graph of the witness consed onto the parameter values.

```agda
      c4 : fst (ext a) ≡ env (cons (fst a) g′)
      c4 = ext-graph a
```

The pair of the key and the table belongs to the pairs of the table family, which is how the table is indexed by its key.

```agda
      c5 : ⟨ pr (fst sS) (fst T) ∈ˢ fst SM.pairs ⟩
      c5 = Tof-pair (suc k) χ
```

The extension by the least witness belongs to the table: the table's membership equation reads it as satisfaction of `χ`, and the leastness data supplies exactly that satisfaction.

```agda
      c6 : ⟨ fst (ext a) ∈ˢ fst T ⟩
      c6 = transport (sym (cong ⟨_⟩ (ext-sat a))) (a-least .fst)
```

The least witness belongs to the stage `Lset lam`; in the internal presentation `A = LsetS lam ordλ`, this is exactly the membership proof carried by `a`.

```agda
      c7 : ⟨ fst aS ∈ˢ fst A ⟩
      c7 = snd a
```

The minimality clause excludes every candidate `w'` in `Lset lam` whose extended environment belongs to the table: its packaged form cannot lie strictly below the chosen witness. This is precisely the leastness property of `a`.

```agda
      c8 : BodyRd.Min T (ext a) e sS (nn k) aS Z g′
      c8 w' w'∈ e'' q hm hr = a-least .snd w'S sat lt'
        where
        w'S : SL
        w'S = fst w' , w'∈
```

The internal relation between the smaller candidate and `a` is filled from the ambient well-order restricted to constructible elements, and the candidate satisfies `χ`: its extension belongs to the table, read as satisfaction through the extension equation.

```agda
        lt' : relOf-at w'S a
        lt' = relL-rep lam λ-isL ordλ w'S a hr
        sat : ⟨ (w'S ∷ vs) ⊨₀ χ ⟩
        sat = transport (cong ⟨_⟩ (ext-sat w'S))
                (subst (λ t → ⟨ t ∈ˢ fst T ⟩) (q ∙ sym (ext-graph w'S)) hm)
```

The eight clauses together show that `witFo` holds at `(aS, Z)`: `a` is the least witness of `χ` over the chosen parameters, expressed entirely inside the constructible structure. We next read the same body data outward under the assumption that every member of `Z` lies in `Lset lam`.

```agda
      least : ⟨ (aS ∷ Z ∷ []) ⊨ witFo ⟩
      least = witFo-in aS Z T (ext a) e sS (nn k)
        (BodyRd.b-fill T (ext a) e sS (nn k) aS Z g′ refl c1 c2 c3 c4 c5 c6 c7 c8)
    module Out (Z : CS.S) (Z⊆ : (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
               (w T e' e s k : CS.S) (h : ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩) where
```

A body witness provides eight facts: the arity numeral, key shape, recovered parameter environment, extension equation, indexed table, table membership, stage membership, and minimality. Their outward readings reconstruct the semantic search represented by the code.

```agda
      module Rd = BodyRd T e' e s k w Z
        using ( b-num; b-key; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
```

The stage clause proves that the witnessed set `w` belongs to `Lset lam`. Pairing `w` with this proof gives `wS`, the corresponding element of the stage carrier.

```agda
      wS : SL
      wS = fst w , Rd.b-stage h
```

The arity component of a decoded key belongs to the internal `ω`. Thus, up to propositional truncation, it is some numeral `# n`; fixing such an `n` lets us analyze the key at an ordinary natural-number arity.

```agda
      module AtNum (n : ℕ) (qk : fst k ≡ # n) where
```

Inside this case, the first fact says that the slot component `s` of the key is itself a code, that is, a member of `C₀`. This follows from the key inversion: a key is the ordered pair of an arity numeral and a code, and reading the pair apart exhibits the code.

```agda
        s∈ : ⟨ fst s ∈ˢ fst C₀ ⟩
        s∈ = KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .fst
```

With the arity identified as `n`, the environment clause recovers a function `g : Fin n → ⟪ fst Z ⟫` and proves that the coded parameter environment is the graph of the values named by those indices.

```agda
        module R = Recover Z n (Env T e' e s k w Z) i2 i4 i6 qk refl (Rd.b-env h) using ( g; recovers )
```

The recovered environment lists indices into the starting set. Each index is presented as an ambient element by the embedding of its presentation, giving the vector `g′` of underlying sets.

```agda
        g′ : Fin n → V ℓ
        g′ i = ⟪ fst Z ⟫↪ (R.g i)
```

The vector `vs` collects the same elements as entries of the constructible carrier, pairing each with the proof that it is constructible.

```agda
        vs : Vec SL n
        vs = vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i)))
```

For every position `i`, the first component of `lookup i vs` is `g′ i`. Thus `vs` and `g′` describe the same parameter sequence, once as elements of the stage carrier and once as ambient sets.

```agda
        vs-val : (i : Fin n) → fst (lookup i vs) ≡ g′ i
        vs-val i = cong fst (lookup-vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i))) i)
```

The recovered environment genuinely comes from the starting set: each entry of `vs`, read as a set, is a member of `Z`. This is the `From Z vs` record.

```agda
        from : From Z vs
        from i = subst (λ u → ⟨ u ∈ˢ fst Z ⟩) (sym (vs-val i)) (member (fst Z) (R.g i))
```

The recovery equation identifies the original environment component `e` with `env g′`, the graph formed from the recovered ambient values.

```agda
        hE : fst e ≡ env g′
        hE = R.recovers
```

The witness slot is compared with other candidates by extending the recovered environment by one entry: `ext b` is the environment with `b` prepended to `vs`.

```agda
        ext : SL → CS.S
        ext b = envFor A (b ∷ vs)
```

The underlying environment of this extension computes to the cons of the underlying set of `b` with `g′`: the graph description of the extended environment matches entry by entry.

```agda
        ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′)
        ext-graph b = envFor-graph A (b ∷ vs)
          ∙ cong env (funExt (λ { zero → refl ; (suc i) → vs-val i }))
```

The key's own environment component is identified with `ext wS`: extending the recovered environment by the witness slot is exactly what the key recorded.

```agda
        e'≡ : fst e' ≡ fst (ext wS)
        e'≡ = Rd.b-cons g′ hE h ∙ sym (ext-graph wS)
```

Now choose the formula `χ` decoded from the code component and identify `s` with its canonical key `keyOf (suc n) χ`. The environment, formula, and key then all describe the same satisfaction query.

```agda
        module AtCode (χ : Formula (⊥* {ℓ}) (suc n)) (qs : fst s ≡ fst (keyOf (suc n) χ)) where
```

The predicate `P b` says that `b`, prepended to the recovered environment, satisfies `χ`. It is the property that the least-witness search minimizes over.

```agda
          P : SL → hProp (ℓ-suc ℓ)
          P b = (b ∷ vs) ⊨₀ χ
```

Membership in the satisfaction table of `χ` agrees with `P b`, because the environment of `ext b` computes to the graph of `b ∷ vs`. This converts between the coded and the semantic readings of satisfaction.

```agda
          ext-sat : (b : SL) → ⟨ ext b CS.∈ˢ Tof (suc n) χ ⟩ ≡ ⟨ P b ⟩
          ext-sat b = cong ⟨_⟩ (sat-at (suc n) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs)))
```

The table component of the key is next identified with the satisfaction table of `χ` at the raised arity; with both components decoded, the key's member can be read semantically.

```agda
          module AtTable (qT : fst T ≡ fst (Tof (suc n) χ)) where
```

The witness slot satisfies the recovered formula: the membership recorded in the key is transported along the environment and table identifications into satisfaction of `χ` at the extended environment.

```agda
            sat : ⟨ P wS ⟩
            sat = transport (ext-sat wS)
              (subst2 (λ u t → ⟨ u ∈ˢ t ⟩) e'≡ qT (Rd.b-mem h))
```

Leastness says that no stage element `b` satisfying `χ` lies below `wS`. Satisfaction of `χ` is converted into membership of `ext b` in the recovered table, and the stage well-order is converted into the internal relation required by the body's minimality clause.

```agda
            min : (b : SL) → ⟨ P b ⟩ → relOf-at b wS → Empty.⊥
            min b pb lt = Rd.b-min g′ hE h bS (snd b) (ext b) (ext-graph b) hm
              (relL-fill lam λ-isL ordλ b wS lt)
              where
              bS : CS.S
```

The smaller candidate is packaged as a constructible element `bS`, and its extended environment is shown to lie in the table, which is exactly the membership the minimality of the key refutes.

```agda
              bS = fst b , Lset→isL lam ordλ (fst b) (snd b)
              hm : ⟨ fst (ext b) ∈ˢ fst T ⟩
              hm = subst (λ t → ⟨ fst (ext b) ∈ˢ t ⟩) (sym qT) (transport (sym (ext-sat b)) pb)
```

The two facts combine into a satisfiability witness for `χ` at the recovered environment: the witness slot, together with its satisfaction, is truncated into `Sat`.

```agda
            w₀ : Sat n χ vs
            w₀ = ∣ wS , sat ∣₁
```

The recovered arity `n`, formula `χ`, parameter vector `vs`, and witness `w₀` form a semantic search. Uniqueness of least elements identifies its result `search n χ vs w₀` with the original witnessed set `w`; separately, the table clause begins the proof that the recovered table is the satisfaction table of `χ`.

```agda
            searched : Searched Z (fst w)
            searched = n , χ , vs , w₀ , (from , sym (cong (λ q → fst (fst q))
              (isPropLeastOf wL P (leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀) (wS , (sat , min)))))
          table : ∥ Searched Z (fst w) ∥₁
          table = ∣ AtTable.searched
```

The table clause presents the underlying set of `T` as the value associated with the key `s`. Since `s` has already been identified with the canonical key of `χ` at arity `suc n`, uniqueness of the value at that key yields `fst T ≡ fst (Tof (suc n) χ)`.

```agda
            (snd p ∙ cong fst (valOf-same s (fst p) (suc n) χ qs)) ∣₁
            where
            p : Σ[ m ∈ ⟨ s CS.∈ˢ AllCodes A ⟩ ] (fst T ≡ fst (SM.valOf s m))
            p = SM.pairs-out s T (Rd.b-tab h)
```

To decode the code component `s`, `freeCode-out` supplies a formula `χ` whose free code is that component. The equation for the slot, the decoded code equation, and the computation of `keyOf` then identify `s` with the canonical key of `χ`.

```agda
        code : ∥ Searched Z (fst w) ∥₁
        code = PT.rec squash₁
          (λ { (c , qc) → PT.rec squash₁
            (λ { (χ , ec) → AtCode.table χ
                   (qc ∙ cong (pr (# (suc n))) ec ∙ sym (keyOf-fst (suc n) χ)) })
```

The key equation supplies the final link between the coded slot and the decoded formula. Consequently this numeral case yields a truncated `Searched Z (fst w)`: the witnessed set is exactly the least-witness search result for parameters recovered from `Z`.

```agda
            (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) qc s∈)) })
          (KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .snd)
```

Since the arity recorded in every body witness belongs to the internal `ω`, numeral decoding turns the preceding analysis into a truncated semantic search for every such witness. For separation, choose the bound `Bnd Z = Z ∪ A`, where `A` is the internal presentation of `Lset lam`.

```agda
      searched : ∥ Searched Z (fst w) ∥₁
      searched = PT.rec squash₁ (λ { (n , qk) → AtNum.code n qk }) (ω-num k (Rd.b-num h))
    Bnd : CS.S → CS.S
    Bnd Z = cupʟ Z A
```

Members of `Z` lie in the bound by the left inclusion of the union.

```agda
    bnd-Z : (Z z : CS.S) → ⟨ fst z ∈ˢ fst Z ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩
    bnd-Z Z z = cupʟ-inl Z A (fst z)
```

Every member of `Lset lam` lies in `Bnd Z` through the right inclusion. The one-step closure condition then has three cases: an old member of `Z`, the empty set used when no witness exists, or a set `w` satisfying `witFo` with base `Z`.

```agda
    bnd-L : (Z z : CS.S) → ⟨ fst z ∈ˢ Lset lam ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩
    bnd-L Z z = cupʟ-inr Z A (fst z)
    Body : CS.S → CS.S → Type (ℓ-suc ℓ)
    Body Z w = ⟨ fst w ∈ˢ fst Z ⟩ ⊎ ((fst w ≡ ∅) ⊎ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩)
```

In the third case, the stage clause encoded by `witFo` proves directly that `w ∈ Lset lam`. Thus every newly adjoined least witness lies inside the fixed stage.

```agda
    wit-L : (Z w : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ → ⟨ fst w ∈ˢ Lset lam ⟩
    wit-L Z w hw = PT.rec (snd (fst w ∈ˢ Lset lam))
      (λ { (T , e' , e , s , k , h) → BodyRd.b-stage T e' e s k w Z h })
      (witFo-out w Z hw)
    opaque
```

The separation formula expresses these three cases inside the constructible structure: membership in `Z`, equality with the empty set, or the renamed formula `witFo`. The renaming places its two free variables in the slots created by the existential wrapper.

```agda
      sepFo : CS.S → Formula CS.S 1
      sepFo Z = (var i0 ∈̇ con Z)
              ∨̇ ( (var i0 ≐ con ∅ʟ)
                ∨̇ ∃̇ ( (var i0 ≐ con Z) ∧̇ renameFo ρs witFo ) )
```

The renaming merely exchanges the two environment entries. Hence evaluating the renamed `witFo` at `(Z'', w)` has the same truth value as evaluating the original `witFo` at `(w, Z'')`.

```agda
      private
        rs : (Z'' w : CS.S)
           → ⟨ (Z'' ∷ w ∷ []) ⊨ renameFo ρs witFo ⟩ ≡ ⟨ (w ∷ Z'' ∷ []) ⊨ witFo ⟩
        rs Z'' w = cong ⟨_⟩ (Ren.⊨-rename ρs witFo (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ []) (ags Z'' w))
```

Satisfaction of the separation formula decomposes into the three truncated cases of the body: membership in `Z`, equality with the empty set, or an existential whose witness identifies the domain.

```agda
      sep-out : (Z w : CS.S) → ⟨ (w ∷ []) ⊨ sepFo Z ⟩ → ∥ Body Z w ∥₁
      sep-out Z w = PT.rec squash₁ (λ
        { (inl hz) → ∣ inl hz ∣₁
        ; (inr h') → PT.rec squash₁ (λ
          { (inl e) → ∣ inr (inl e) ∣₁
```

In the existential case, its witness `Z''` is equal to the fixed parameter `Z`. Transporting along this equality and then along the renaming path yields `witFo` at `(w, Z)`.

```agda
          ; (inr hw) → PT.map (λ { (Z'' , (eZ , hr)) → inr (inr
              (subst (λ u → ⟨ (w ∷ u ∷ []) ⊨ witFo ⟩) (S≡ {x = Z''} {y = Z} eZ)
                (transport (rs Z'' w) hr))) }) hw }) h' })
```

Conversely, each of the three cases of the body produces the corresponding satisfaction of the separation formula, re-wrapping the renaming where needed.

```agda
      sep-in : (Z w : CS.S) → Body Z w → ⟨ (w ∷ []) ⊨ sepFo Z ⟩
      sep-in Z w (inl hz) = ∣ inl hz ∣₁
      sep-in Z w (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁
      sep-in Z w (inr (inr hw)) = ∣ inr ∣ inr ∣ Z , (refl , transport (sym (rs Z w)) hw) ∣₁ ∣₁ ∣₁
```

Separation inside `L` selects from `Bnd Z` exactly the sets satisfying `sepFo Z`; call the resulting constructible set `Φ Z`. Its membership path identifies membership in `Φ Z` with membership in the bound together with satisfaction of the formula.

```agda
    opaque
      Φ : CS.S → CS.S
      Φ Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .fst
```

The membership specification reads: `w` belongs to `Φ Z` exactly when `w` belongs to the bound and satisfies the separation formula.

```agda
      Φ-mem : (Z w : CS.S) → (w CS.∈ˢ Φ Z) ≡ ((w CS.∈ˢ Bnd Z) ⊓ ((w ∷ []) ⊨ sepFo Z))
      Φ-mem Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .snd
```

Every body case lands in `Φ Z`. The membership case enters through the bound; the proof packages the bound membership produced from each disjunct together with its separation satisfaction.

```agda
    Φ-in : (Z w : CS.S) → Body Z w → ⟨ fst w ∈ˢ fst (Φ Z) ⟩
    Φ-in Z w b = subst ⟨_⟩ (sym (Φ-mem Z w)) (bnd b , sep-in Z w b)
      where
      bnd : Body Z w → ⟨ w CS.∈ˢ Bnd Z ⟩
      bnd (inl hz) = bnd-Z Z w hz
```

The empty-set case lies in the bound because `∅ ∈ Lset lam`. The witness case lies there because the stage clause of `witFo` proves its value belongs to `Lset lam`.

```agda
      bnd (inr (inl e)) = bnd-L Z w (subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym e) HSH.∅∈Lsetα)
      bnd (inr (inr hw)) = bnd-L Z w (wit-L Z w hw)
```

Conversely, membership in `Φ Z` yields a truncated body case, by the membership specification and the separation reading. For the biconditional formula, the body is then rewritten in a three-slot arrangement.

```agda
    Φ-out : (Z w : CS.S) → ⟨ fst w ∈ˢ fst (Φ Z) ⟩ → ∥ Body Z w ∥₁
    Φ-out Z w h = sep-out Z w (subst ⟨_⟩ (Φ-mem Z w) h .snd)
    opaque
      bodyF : Formula CS.S 3
      bodyF = (var i0 ∈̇ var i2) ∨̇ ((var i0 ≐ con ∅ʟ) ∨̇ renameFo ρf witFo)
```

The graph formula `ΦFo` quantifies over a fresh set `w` and states both implications between `w ∈ Z'` and the three-case condition `Body Z w`. Thus `(Z', Z)` satisfies `ΦFo` exactly when `Z'` has the same members as `Φ Z`.

```agda
      ΦFo : Formula CS.S 2
      ΦFo = ∀̇ ( ((var i0 ∈̇ var i1) ⇒̇ bodyF) ∧̇ (bodyF ⇒̇ (var i0 ∈̇ var i1)) )
```

The renaming equivalence for the graph is proved like the earlier one: the renaming permutes the environment, and satisfaction transfers along the permutation.

```agda
      private
        rf : (w Z' Z : CS.S)
           → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ renameFo ρf witFo ⟩ ≡ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
        rf w Z' Z = cong ⟨_⟩ (Ren.⊨-rename ρf witFo (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ []) (agf w Z' Z))
```

The body transfers across the three-slot arrangement in both directions: membership in `Z` is direct, and the remaining disjuncts are mapped through the truncation.

```agda
        bodyF-out : (w Z' Z : CS.S) → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩ → ∥ Body Z w ∥₁
        bodyF-out w Z' Z = PT.rec squash₁ (λ
          { (inl hz) → ∣ inl hz ∣₁
          ; (inr h') → PT.map (λ
            { (inl e) → inr (inl e)
```

In the witness case, the renaming path converts satisfaction of the three-slot formula back to `witFo` at `(w, Z)`, completing the forward implication from the graph body to `Body Z w`.

```agda
            ; (inr hw) → inr (inr (transport (rf w Z' Z) hw)) }) h' })
```

The converse assembles the three cases into the three-slot reading, transporting the witness disjunct against the renaming.

```agda
        bodyF-in : (w Z' Z : CS.S) → Body Z w → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩
        bodyF-in w Z' Z (inl hz) = ∣ inl hz ∣₁
        bodyF-in w Z' Z (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁
        bodyF-in w Z' Z (inr (inr hw)) = ∣ inr ∣ inr (transport (sym (rf w Z' Z)) hw) ∣₁ ∣₁
```

The definability clause is then proved: the pair `(Φ Z, Z)` satisfies the graph formula. Each direction of the biconditional is the corresponding membership direction composed with the body transfer.

```agda
      Φ-defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩
      Φ-defines Z w =
          (λ h → PT.rec (snd ((w ∷ Φ Z ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in w (Φ Z) Z) (Φ-out Z w h))
        , (λ h → PT.rec (snd (fst w ∈ˢ fst (Φ Z))) (Φ-in Z w) (bodyF-out w (Φ Z) Z h))
```

Uniqueness of the graph is proved by extensionality of the constructible structure: for any `Z'` whose pair with `Z` satisfies the graph formula, every member of `Z'` satisfies the body, and `Φ-in` places it in `Φ Z`.

```agda
      Φ-only : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
      Φ-only Z Z' h = extensionalL (λ v → ⇔toPath (fwd v) (bwd v))
        where
        fwd : (v : CS.S) → ⟨ fst v ∈ˢ fst Z' ⟩ → ⟨ fst v ∈ˢ fst (Φ Z) ⟩
        fwd v hv = PT.rec (snd (fst v ∈ˢ fst (Φ Z))) (Φ-in Z v) (bodyF-out v Z' Z (h v .fst hv))
```

The backward direction of the extensionality argument reads each member of `Φ Z` as a truncated body case and applies the graph formula at that member.

```agda
        bwd : (v : CS.S) → ⟨ fst v ∈ˢ fst (Φ Z) ⟩ → ⟨ fst v ∈ˢ fst Z' ⟩
        bwd v hv = h v .snd
          (PT.rec (snd ((v ∷ Z' ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in v Z' Z) (Φ-out Z v hv))
```

We have therefore obtained a definable one-step operation `Φ`: the formula `ΦFo` characterizes its graph, and extensionality proves that any set satisfying that graph condition is equal to `Φ Z`.

```agda
    pack : StepPack
    pack = record
      { Φ       = Φ
      ; ΦFo     = ΦFo
      ; defines = Φ-defines
```

This step contains every old member of `Z`, always contains the empty set, and contains the least witness for every satisfiable formula with parameters from `Z`. Conversely, its members arise only from these three cases, so `Φ` is exactly the desired one-step closure.

```agda
      ; only    = Φ-only
      ; grows   = λ Z z hz → Φ-in Z (z , isL-trans {x = fst Z} {y = z} hz (snd Z)) (inl hz)
      ; junk    = λ Z → Φ-in Z ∅ʟ (inr (inl refl))
      ; least   = λ Z k χ vs from w₀ →
                    Φ-in Z (Least.aS Z k χ vs from w₀) (inr (inr (Least.least Z k χ vs from w₀)))
```

Assume every member of `Z` lies in `Lset lam`. If `z ∈ Φ Z`, the membership characterization gives three possibilities: `z` was already in `Z`, `z = ∅`, or `witFo` holds at `(z, Z)`. In the third case, decoding the body reconstructs a semantic search from parameters in `Z` whose result is `z`.

```agda
      ; out     = λ Z Z⊆ z hz → PT.rec squash₁ (λ
          { (inl h') → ∣ inl h' ∣₁
          ; (inr (inl e)) → ∣ inr (inl e) ∣₁
          ; (inr (inr hw)) → PT.rec squash₁
              (λ { (T , e' , e , s , k , hb) →
```

In the witness case, `z ∈ Φ Z` first makes `z` constructible, so it can be read as an element of the constructible carrier. The decoded body then proves `Searched Z z`, identifying `z` with the least-witness search determined by the recovered formula and parameters.

```agda
                 PT.map (λ sr → inr (inr sr)) (Out.searched Z Z⊆ (zS Z z hz) T e' e s k hb) })
              (witFo-out (zS Z z hz) Z hw) })
          (Φ-out Z (zS Z z hz) hz) }
      where
      zS : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → CS.S
```

Since `Φ Z` is constructible and constructibility is transitive, every member `z` of `Φ Z` is constructible.

```agda
      zS Z z hz = z , isL-trans {x = fst (Φ Z)} {y = z} hz (snd (Φ Z))
```

## Supplying the constructibility premise for condensation

This supplies the carrier element needed in the preceding decoding and completes the construction of the definable one-step closure.

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

Assume that the hull `M` is itself constructible. This turns `M` into a constructible carrier, so the preceding collapse argument applies without requiring the hull to be transitive.

```agda
  (M-isL : ⟨ isL (HullStage.M lam ordλ succλ X X⊆L ∅∈λ) ⟩) where
```

Regarded as a constructible carrier, `M` has a collapse image `πX`. Every member of this image is the collapse value of some member of `M`, and the constructible-carrier theorem proves that such values belong to `L`.

```agda
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
  module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX )
  module P = PiIn (HS.M , M-isL) using ( πX-isL )
```

Consequently, every `x ∈ πX` is constructible. We now return to the hull generated from `X` inside `Lset λ`, assuming that `λ` is an ordinal closed under successors and that every member of `X` lies in this stage.

```agda
  pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩
  pixL = P.πX-isL
module Condense′ (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
```

We also assume that `∅ ∈ λ`, that the hull frame generated by `X` is elementary, that `λ` is superadequate, and that `X` itself is constructible. The last assumption supplies the base of the internal finite iteration; elementarity and superadequacy supply the hypotheses needed for condensation.

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  where
```

The construction has three connected parts. Codes name the initial elements and the values selected by later searches, using the empty set when a search has no witness; one definable operation `Φ` performs a closure step; and finite iteration of `Φ`, followed by union, builds a constructible set that will be identified with the Skolem hull.

```agda
  module T = Telescope lam ordλ succλ X X⊆L ∅∈λ using ( Code; val; Reads; module StepPack )
  module TB = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ using ( pack; Φ )
  module HI = Telescope.HullIter lam ordλ succλ X X⊆L ∅∈λ X-isL TB.pack
    using ( hullL; hullL-spec; hullStep; hullStep-suc; hullStep-in; hullStep⊆Hull; depth; M-isL )
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
```

The union of the finite closure stages is already an element `hullL` of the constructible universe. The next equality shows that its underlying set is precisely the externally defined hull `M`; this will supply the constructibility premise used above for the collapse image.

```agda
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX )
  module D = Discharge lam ordλ succλ X X⊆L ∅∈λ HI.M-isL using ( pixL )
  hullL : CS.S
  hullL = HI.hullL
```

The underlying set of `hullL` is exactly `M`. Hence the external characterization of the Skolem hull and the constructible set obtained by iteration describe the same members, while `hullL` additionally carries a proof of constructibility.

```agda
  hullL-spec : fst hullL ≡ HS.M
  hullL-spec = HI.hullL-spec
```

The closure stages of the hull are indexed by natural numbers: `hullStep n` is the stage reached after `n` applications of the closure step.

```agda
  hullStep : ℕ → CS.S
  hullStep = HI.hullStep
```

At a successor index, the next stage is `Φ` applied to the current one. This operation retains the current members, includes the empty set, and adjoins the least witness for each coded search whose parameters are already present.

```agda
  hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ TB.Φ (hullStep n)
  hullStep-suc = HI.hullStep-suc
```

Each code has a finite depth, and the value it denotes belongs to the closure stage at that depth. Since every hull member is represented by a code, this gives a finite stage containing it, without choosing a canonical code for the member.

```agda
  hullStep-in : (c : T.Code) → ⟨ fst (T.val c) ∈ˢ fst (hullStep (HI.depth c)) ⟩
  hullStep-in = HI.hullStep-in
```

Conversely, every member of every finite closure stage belongs to `M`. Together with the coded description of hull members, this proves that the union of the stages and the Skolem hull have exactly the same elements.

```agda
  hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ HS.M ⟩
  hullStep⊆Hull = HI.hullStep⊆Hull
```

The union of the stages is constructible: the hull stage `M` is an element of `L`. This is the first of the two membership facts the chapter set out to prove.

```agda
  M-isL : ⟨ isL HS.M ⟩
  M-isL = HI.M-isL
```

The second follows through the discharge: every value of the collapse `πX` of the hull stage is constructible, because the carrier `M` is.

```agda
  pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩
  pixL = D.pixL
```

Condensation now yields an ordinal `β` for which the collapse image is exactly `Lset β`. The earlier memberwise constructibility statement is thereby strengthened to an identification of the whole image with one stage of the constructible hierarchy. The conclusion asserts this equality and the ordinality of `β`; it makes no further comparison between `β` and `λ`.

```agda
  condenses′ : Σ[ β ∈ S ] (IsOrd β × (HSC.πX ≡ Lset β))
  condenses′ = Condense.condenses lam ordλ succλ X X⊆L ∅∈λ elem sup D.pixL
```