---
title: "Transferring structure through condensation"
module: L.GCH.CondensationTransfer
lang: en
site: "Bedrock"
description: "Transferring structure through condensation"
stage: "Proving GCH"
reading_order: 107
canonical: https://bedrock.institute/en/L.GCH.CondensationTransfer.html
html: L.GCH.CondensationTransfer.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CondensationTransfer.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Semantics, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.GCH.SkolemHull, L.GCH.HierarchyDescription, L.GCH.AdequateStages]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.CondensationTransfer.md, https://bedrock.institute/ja/L.GCH.CondensationTransfer.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Transferring structure through condensation

This chapter asks what becomes of an elementary Skolem hull after its Mostowski collapse. Under the stated hypotheses at an ordinal index `lam`, the collapse image is identified with `Lset β` for some ordinal `β`. No comparison between `β` and `lam`, no least such index, and no cardinal estimate is part of this conclusion. The proof begins by giving the constructible-stage relation a bounded first-order description that can be read before and after the collapse.

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

The theorem is parameterized by excluded middle at `ℓ-suc ℓ`. That single classical hypothesis is passed to the preceding results about ordinal stages, hulls, hierarchy descriptions, and adequate stages. The present argument introduces no choice principle: existential satisfaction and the local stage witnesses supplied by superadequacy remain propositionally truncated, so they may be used only when the target is again a proposition.

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

Fix the universe level and this classical parameter. All sets below belong to the ambient cumulative hierarchy at level `ℓ`; the constructible stages, the hull, and the collapse image are sets in that same hierarchy. Full elementarity transports the formulas with unbounded existential quantifiers. The bounded interfaces, built from stage absoluteness, elementarity, and the collapse isomorphism, expose Δ₀ transport through the collapse. Keeping these two uses separate is essential to the condensation proof.

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

The object language needs only membership, equality, conjunction, and unbounded existence for the two queries built below. Its constant alphabet changes as a formula moves between the ambient hierarchy, the stage, and the hull. The operation `mapFo` relabels existing constants, while `embed` regards a constant-free formula as a formula over a new constant alphabet. Neither operation changes the variable positions or logical structure of the formula.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; embed )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

The constructible hierarchy requires a persistent distinction between an ordinal index `d` and the stage `Lset d` that it indexes. A member of `Lset lam` is constructible when `lam` is ordinal. Conversely, if an ordinal `d` is a member of `Lset lam`, rank comparison places `d` in `lam`. The downward description `Lset-out` says only that a member of a stage merely comes from `𝒟ₒ (Lset c)` for some `c` in its index; it retains no chosen birth stage. Monotonicity then transports membership from `Lset β` to `Lset α` when the strict index relation `β ∈ α` is available.

```agda
open import L.Constructible {ℓ} using
  ( IsOrd; isL; Lset; Lset-out; Lset-mono; Lset→isL; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc; ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
```

The central formula is `levelFo(a,p,z)`. Its Δ₀ certificate allows bounded absoluteness and transport through the collapse. Soundness says that, when `a`, `p`, and `z` are constructible, satisfaction implies `a ≡ Lset p`; the auxiliary bound `z` need not be uniquely determined. Completeness supplies satisfaction at the particular triple `(Lset p,p,Lset γ)` when `γ` is adequate, `p` is ordinal, and `p ∈ γ`. The surrounding theory provides the hull transfer and the local adequate indices required to construct such triples.

```agda
open import L.GCH.SkolemHull {ℓ} lem using
  ( module HullStage; Δ₀-isOrdAt; module Amb
  ; module Frame; _⊨ₚ_; embed-map; isOrd-at-p )
open import L.GCH.HierarchyDescription {ℓ} lem using ( levelFo; Δ₀-levelFo; level-sound; level-complete )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate; Adequate; Lset∈suc )
```

Finite vectors record the environments in which formulas are evaluated, while products combine the membership and equality facts used in the proof. Several existences in this chapter are propositionally truncated. The constructor `∣_∣₁` places an explicit local witness under truncation; `PT.rec` and `PT.map` may then use it only to produce another proposition. In particular, the local adequate indices supplied by superadequacy never become a globally chosen family.

```agda
open import Cubical.Data.Vec using ( _∷_; [] )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

The set-theoretic successor `sucV d` is the next ordinal index when `d` is ordinal, and it is also the index used by the successor-stage equation `Lset (sucV d) ≡ 𝒟ₒ (Lset d)`. These are related facts, but the successor index and the stage at that index remain different sets. The empty set appears separately because the hull construction requires a fallback member already present in the ambient index.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

Opening the proposition-valued hierarchy structure fixes the carrier `S` and the ambient membership notation `_∈ˢ_`. Brackets `⟨_⟩` expose the type of proofs carried by one of its truth values. Thus `d ∈ˢ lam`, membership in a constructible stage, and membership in the collapse image are ambient set-theoretic statements, distinct from the object-language atom `_∈̇_` used inside a formula.

```agda
open hPropStructure 𝒮ᵥ
```

The ambient semantics supplies the notation `S ^ n` for environments of length `n`. Formula slots are read from such vectors; each newly bound existential witness is placed at the front, shifting the older slots outward. This convention explains why the three nested witnesses used later are finally read in the order `(a,p,z)`, even though they are introduced from the outside as `z`, then `p`, then `a`.

```agda
module SemVᵃ = FOL.Semantics 𝒮ᵥ
open SemVᵃ using ( _^_ )
```

## Formulas that identify the level witnesses

The formula `isOrd-at-p` uses only the middle slot of a three-entry environment. Its first conjunct says that `p` is transitive, and its second says that every member of `p` is transitive. The two functions displayed here unpack those bounded clauses into the two fields of `IsOrd p`. The neighbouring values `a` and `z` play no role in this lemma, and the lemma does not read the rest of `levelFo` or identify `a` with a constructible stage.

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

## Transferring hierarchy information through the collapse

Fix an ordinal `lam` and the ambient constructible stage `Lset lam` that contains the hull. The index is closed under set-theoretic successor, every generator in `X` belongs to this stage, and `∅ ∈ lam` supplies the default element needed in the hull construction. The last hypothesis in this first group is full elementarity: every formula, including formulas with unbounded quantifiers, has the same truth value in the hull and in the surrounding stage when its parameters come from the hull.

```agda
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 ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
```

Two further hypotheses provide local stages and constructible collapse values. `Superadequate lam` says that every `d ∈ lam` is merely contained in some adequate ordinal index `γ` with `γ ∈ lam`; propositional truncation retains neither a selected `γ` nor a least one. The hypothesis `pixL` is pointwise: each member of the collapse image is constructible. It does not yet say that the collapse image itself is a constructible set, much less identify that image with a particular stage.

```agda
  (sup : Superadequate lam)
  (pixL : (x : S) → ⟨ x ∈ˢ HullStage.C.πX lam ordλ succλ X X⊆L ∅∈λ ⟩
        → ⟨ isL x ⟩)
  where
```

Three structures are now used together: the ambient structure on `Lset lam`, the structure whose carrier consists of hull members, and the transitive collapse image. A hull element carries both an underlying set and its proof of membership in `M`. Bounded formulas can be read between the first two structures and can be transported in either direction through the collapse; individual membership facts can also be pushed through the collapse. These Δ₀ interfaces will be used only after the unbounded existential queries have been handled by full elementarity.

```agda
  module F = Frame lam ordλ succλ X X⊆L ∅∈λ using (module A; module Carry; module HS)
  module A = F.A using (SM; module SemM; inL)
  module Mse = A.SemM.At A.SM id using (_⊨_)
  module HS = F.HS using (module ASt; module C; module Condense; module H; M)
  module Cy = F.Carry elem using (atL; atM; member-push; push; pull)
```

The inclusion `Hull⊆L` is the basic bridge from a hull member to the ambient stage: if `x ∈ M`, then `x ∈ Lset lam`. This fact supplies the stage-membership evidence used by `A.inL`, and it will also turn each returned hull witness into a constructible set through `isLλ`. It is a pointwise inclusion of the hull in the stage, not a statement that the hull itself is an element of that stage.

```agda
  open HS.H using ( Hull⊆L )
```

Let `M` denote the Skolem hull determined by the preceding data. Its members lie in `Lset lam` by `Hull⊆L`, but neither the constructibility of `M` as a whole nor any additional closure property follows from this notation. Every later use of the collapse will therefore keep the premise that its argument belongs to `M`.

```agda
  M : S
  M = HS.M
```

Let `π` be the Mostowski collapse map and let `πX` be its transitive image. On hull members, `π` preserves the membership relation and identifies bounded truths with their readings in the image. The problem is now to prove enough closure and covering for `πX` to show that this transitive set is exactly one stage `Lset β`.

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

Because `lam` is ordinal, membership in `Lset lam` supplies constructibility. The helper `isLλ` packages exactly this implication. It will be applied to all three entries returned by a hull query before `level-sound` is invoked, since satisfaction of `levelFo` alone does not provide the constructibility assumptions required by its soundness theorem.

```agda
  isLλ : (x : S) → ⟨ x ∈ˢ Lset lam ⟩ → ⟨ isL x ⟩
  isLλ = Lset→isL lam ordλ
```

Two elementary membership lemmas now prepare witnesses for the ambient stage. First suppose `d ∈ lam`. Successor closure gives `sucV d ∈ lam`; the entire stage `Lset d` is an element of `Lset (sucV d)`; and `Lset-mono` transports that single element into `Lset lam`. The conclusion `Lset d ∈ Lset lam` is membership between sets, not the pointwise inclusion of one stage in another.

```agda
  Lset∈Lλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ Lset d ∈ˢ Lset lam ⟩
  Lset∈Lλ d d∈λ = Lset-mono {α = lam} {β = sucV d} (succλ d d∈λ) (Lset∈suc d)
```

If `d` is also ordinal, then `ord∈Lset-suc` places the index `d` itself in `Lset (sucV d)`, and the same monotonicity step carries it into `Lset lam`. Together, the two lemmas provide two distinct stage elements, `d` and `Lset d`. Both are needed when the level formula is witnessed inside the ambient stage, and neither membership should be confused with the index relation `d ∈ lam` from which it was derived.

```agda
  ord∈Lλ : (d : S) → IsOrd d → ⟨ d ∈ˢ lam ⟩ → ⟨ d ∈ˢ Lset lam ⟩
  ord∈Lλ d od d∈λ =
    Lset-mono {α = lam} {β = sucV d} (succλ d d∈λ) (ord∈Lset-suc d od)
```

For a hull member `d`, ordinality can be sent through the collapse. `Amb.isOrdAt-in` expresses `IsOrd d` by the constant-free bounded formula `isOrdAt`; `Cy.push` transports that Δ₀ truth from the hull environment to the environment containing `π d`; and `Amb.isOrdAt-out` reads the result as `IsOrd (π d)`. The boundedness certificate controls this transfer, while the comparison embodied in `Cy.push` ultimately rests on the elementary hull inclusion and the collapse isomorphism.

```agda
  ord-push : (d : S) (d∈M : ⟨ d ∈ˢ M ⟩) → IsOrd d → IsOrd (π d)
  ord-push d d∈M od =
    Amb.isOrdAt-out (π d)
      (Cy.push Δ₀-isOrdAt ((d , d∈M) ∷ []) (Amb.isOrdAt-in d od))
```

The same bounded description also travels backward. Starting from `IsOrd (π d)`, `Cy.pull` returns truth of `isOrdAt` at the original hull member, which is then read as `IsOrd d`. Hence the collapse preserves and reflects ordinality on members of `M`. This is a local equivalence with the hypothesis `d ∈ M`; it says nothing about the behaviour of `π` on arbitrary ambient sets.

```agda
  ord-pull : (d : S) (d∈M : ⟨ d ∈ˢ M ⟩) → IsOrd (π d) → IsOrd d
  ord-pull d d∈M oπd =
    Amb.isOrdAt-out d
      (Cy.pull Δ₀-isOrdAt ((d , d∈M) ∷ []) (Amb.isOrdAt-in (π d) oπd))
```

The first existential query is designed to recover the particular stage `Lset d` inside the hull. Its three unbounded existential quantifiers produce an environment `(a,d′,z)`. The embedded core requires `levelFo(a,d′,z)`, while the equation in the second conjunct fixes the returned middle coordinate by `d′ ≡ dM`. Only `levelFo` is Δ₀. The surrounding query `findA` is not bounded, so full elementarity, rather than Δ₀ absoluteness alone, will be used to bring its witnesses from the ambient stage into the hull. This equality is the feature that distinguishes `findA` from the later query `findP`, whose returned index `p′` need not equal the externally prepared `p`.

```agda
  findA : A.SM → Formula A.SM 0
  findA dM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))))
```

The lemma `stageA` builds the ambient witness that elementarity will later pull into the hull. It takes an adequate index `γ` containing the ordinal `d`, a hull representative `dM` whose underlying set is `d`, and separate evidence that `d`, `Lset d`, and `Lset γ` are elements of `Lset lam`. Completeness supplies `levelFo(Lset d,d,Lset γ)`. Bounded absoluteness reads this core in the stage structure, and the object-language equality uses the path from `dM` to `d`. The three unbounded existential clauses are then witnessed, under propositional truncation, by `Lset γ`, `d`, and `Lset d`; no claim that `γ` is least is made.

```agda
  stageA : (d γ : S) (od : IsOrd d) (adγ : Adequate γ) (d∈γ : ⟨ d ∈ˢ γ ⟩)
         → (dM : A.SM) → fst dM ≡ d
         → ⟨ d ∈ˢ Lset lam ⟩ → ⟨ Lset d ∈ˢ Lset lam ⟩ → ⟨ Lset γ ∈ˢ Lset lam ⟩
         → ⟨ [] HS.ASt.AbsL.⊨ᵐ mapFo A.inL (findA dM) ⟩
  stageA d γ od adγ d∈γ dM ed d∈ Ld∈ Lγ∈ =
```

The external witnesses are the adequate bound `Lset γ`, the prescribed index `d`, and its stage `Lset d`. Their final environment is `(Lset d,d,Lset γ)`, so completeness supplies the level-description conjunct. The equality conjunct needs `sym ed`: the query asks for the returned index to equal the interpretation of `dM`, whereas `ed` identifies that interpretation with `d`. Each existential witness is placed under propositional truncation, preserving existence without designating this triple as a canonical choice.

```agda
    ∣ (Lset γ , Lγ∈) , ∣ (d , d∈) , ∣ (Lset d , Ld∈) , (sat , sym ed) ∣₁ ∣₁ ∣₁
    where
    δ : HS.ASt.SL ^ 3
    δ = (Lset d , Ld∈) ∷ (d , d∈) ∷ (Lset γ , Lγ∈) ∷ []
```

Completeness of the level description supplies the mathematical core. Since `γ` is adequate, `d` is ordinal, and `d ∈ γ`, the triple `(Lset d,d,Lset γ)` satisfies `levelFo` in the ambient hierarchy. The adequate-stage hypothesis places the tables used by the description inside the common bound, ordinality makes `d` a legitimate stage index, and `d ∈ γ` places that index below the bound. The remaining task is to read this same Δ₀ fact in the structure on `Lset lam`.

```agda
    amb : ⟨ (Lset d ∷ d ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩
    amb = level-complete γ adγ d od d∈γ
```

The ambient truth must next be expressed in the stage structure on
`Lset lam`, not yet in the hull. Used backward, `Cy.atL` reads the Δ₀ formula
`levelFo` at the three displayed members of that stage. The path `embed-map`
then identifies its vacuous constant relabelling with `embed levelFo`:
`levelFo` has an empty constant domain, although the surrounding query uses
hull elements as constants. Thus `sat` supplies exactly the embedded core
needed by `stageA`; full elementarity will act only after the complete
unbounded query has been assembled.

```agda
    sat : ⟨ δ HS.ASt.AbsL.⊨ᵐ mapFo A.inL (embed levelFo) ⟩
    sat = subst (λ ψ → ⟨ δ HS.ASt.AbsL.⊨ᵐ ψ ⟩) (sym (embed-map A.inL levelFo))
            (subst ⟨_⟩ (sym (Cy.atL Δ₀-levelFo δ)) amb)
```

The second query also asks for a triple `(u,a,z)` satisfying the level description, but it imposes a different additional condition. Instead of identifying the middle coordinate with a prescribed index, it requires the named hull element `yM` to belong to the first coordinate `u`. Thus it asks for some correctly described constructible stage containing `y`. Its index remains free, which is exactly what the covering argument needs.

```agda
  findP : A.SM → Formula A.SM 0
  findP yM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))))
```

The lemma `stageP` prepares an ambient witness to this membership query. It
starts with an ordinal `p`, an adequate `γ` containing `p`, a hull element
`yM` naming `y`, and the fact `y ∈ Lset p`. Separate membership hypotheses
place `p`, `Lset p`, and `Lset γ` inside `Lset lam`, so all three existential
witnesses are available in the stage structure. Here `p` serves only to
construct one external witness. Because `findP` contains no equation fixing
its middle coordinate, the internal index later returned by elementarity may
be a different `p′`.

```agda
  stageP : (y p γ : S) (op : IsOrd p) (adγ : Adequate γ) (p∈γ : ⟨ p ∈ˢ γ ⟩)
         → (yM : A.SM) → fst yM ≡ y → ⟨ y ∈ˢ Lset p ⟩
         → ⟨ p ∈ˢ Lset lam ⟩ → ⟨ Lset p ∈ˢ Lset lam ⟩ → ⟨ Lset γ ∈ˢ Lset lam ⟩
         → ⟨ [] HS.ASt.AbsL.⊨ᵐ mapFo A.inL (findP yM) ⟩
  stageP y p γ op adγ p∈γ yM ey y∈Lp p∈ Lp∈ Lγ∈ =
```

The same external triple `(Lset p,p,Lset γ)` witnesses the level description, but the final conjunct now records that `yM` is interpreted by an element of `Lset p`. This parallel construction isolates the mathematical difference between the queries: `findA` preserves a prescribed index, whereas `findP` preserves the membership of a prescribed point. Full elementarity may therefore return a different internal index in the second case.

```agda
    ∣ (Lset γ , Lγ∈) , ∣ (p , p∈) , ∣ (Lset p , Lp∈) , (sat , mem) ∣₁ ∣₁ ∣₁
    where
    δ : HS.ASt.SL ^ 3
    δ = (Lset p , Lp∈) ∷ (p , p∈) ∷ (Lset γ , Lγ∈) ∷ []
```

Completeness supplies the common core. Since `γ` is adequate, `p` is ordinal,
and `p ∈ γ`, completeness proves that `(Lset p,p,Lset γ)` satisfies `levelFo` in
the ambient hierarchy. Notice what completeness does and does not establish:
it validates this particular externally prepared triple, but it neither says
that every satisfying triple uses `p` nor makes the later internal index
unique.

```agda
    amb : ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩
    amb = level-complete γ adγ p op p∈γ
```

As before, the transfer at this point is only between the ambient hierarchy
and the structure on `Lset lam`. The backward direction of `Cy.atL` uses the
Δ₀ certificate for `levelFo` to read ambient satisfaction at the three
underlying sets as satisfaction at their stage representatives. The
`embed-map` path then puts the constant-free core into the constant domain of
the surrounding hull query. The result is the first conjunct required by
`stageP`; no unbounded quantifier has been transported by this bounded step.

```agda
    sat : ⟨ δ HS.ASt.AbsL.⊨ᵐ mapFo A.inL (embed levelFo) ⟩
    sat = subst (λ ψ → ⟨ δ HS.ASt.AbsL.⊨ᵐ ψ ⟩) (sym (embed-map A.inL levelFo))
            (subst ⟨_⟩ (sym (Cy.atL Δ₀-levelFo δ)) amb)
```

The remaining conjunct says that the interpretation of `yM` belongs to
`Lset p`. Its underlying set is `fst yM`, and the path `ey : fst yM ≡ y`
allows the given membership `y ∈ Lset p` to be transported backward to that
interpretation. This small rewrite is what places the fixed point into the
query while leaving the index unfixed. When elementarity later returns a
triple `(u,p′,z)`, the retained conclusion will be `y ∈ u`, with no equation
between `p′` and the present `p`.

```agda
    mem : ⟨ fst (A.inL yM) ∈ˢ Lset p ⟩
    mem = subst (λ w → ⟨ w ∈ˢ Lset p ⟩) (sym ey) y∈Lp
```

For a set `d`, `Witness d` records under propositional truncation three
facts: some bound `z` belongs to the hull, the prescribed stage `Lset d`
belongs to the hull, and `(Lset d,d,z)` satisfies `levelFo` in the ambient
hierarchy. The type itself can be formed for any `d`; the construction below
requires both `IsOrd d` and `d ∈ M`. Keeping the package truncated is enough
for the later proposition-valued closure and equality conclusions, and it
prevents the proof from treating the adequate bound as chosen data.

```agda
  Witness : S → Type (ℓ-suc ℓ)
  Witness d = ∥ Σ[ z ∈ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
                           × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ ) ∥₁
```

The construction first places the hull member `d` in the ambient stage:
`Hull⊆L` gives `d ∈ Lset lam`. Superadequacy, however, is indexed by members
of the ordinal `lam`, rather than by arbitrary members of its constructible
stage. The local fact `d∈λ` established next bridges precisely this gap.
Once it is available, `sup d d∈λ` merely supplies an adequate stage above `d`;
the outer `PT.rec` may use that truncated supply because its target
`Witness d` is itself a proposition.

```agda
  witness : (d : S) → IsOrd d → ⟨ d ∈ˢ M ⟩ → Witness d
  witness d od d∈M = PT.rec squash₁ step1 (sup d d∈λ)
    where
    d∈Lλ : ⟨ d ∈ˢ Lset lam ⟩
    d∈Lλ = Hull⊆L d d∈M
```

To recover index membership, apply the stage reflection lemma to
`d ∈ Lset lam`. Its hypotheses expose the exact reason the step works:
`lam` is ordinal by the module parameter and `d` is ordinal by the caller.
Only under those ordinal hypotheses does membership of `d` in the stage at
`lam` imply `d ∈ lam`. This is a comparison of ordinal indices, not a general
rank principle for arbitrary sets.

```agda
    d∈λ : ⟨ d ∈ˢ lam ⟩
    d∈λ = ord∈Lset→∈ lam ordλ d od d∈Lλ
```

Now successor closure converts the index relation into the second stage
membership needed by `stageA`. From `d ∈ lam`, the earlier lemma
`Lset∈Lλ` yields `Lset d ∈ Lset lam`, with the whole stage occurring as one
element of the outer stage. Together with `d∈Lλ`, this prepares the two
coordinates tied to `d`. Membership of the eventual bound `Lset γ` will be
derived separately after superadequacy supplies `γ`.

```agda
    Ld∈Lλ : ⟨ Lset d ∈ˢ Lset lam ⟩
    Ld∈Lλ = Lset∈Lλ d d∈λ
```

Superadequacy returns, under propositional truncation, an index `γ` with
`γ ∈ lam`, `d ∈ γ`, and `Adequate γ`. For any such triple, `step1` will build
`Witness d`: it first constructs the full query in the ambient stage, uses
elementarity to obtain its truncated existential answer in the hull, and
eliminates that answer only into the truncated witness goal. Thus the proof
may reason with a temporary `γ` inside the eliminator, but no choice of `γ`
escapes into the theorem's data.

```agda
    step1 : Σ[ γ ∈ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ d ∈ˢ γ ⟩ × Adequate γ) → Witness d
    step1 (γ , γ∈λ , d∈γ , adγ) =
      PT.rec squash₁ takeZ hullSat
      where
      Lγ∈Lλ : ⟨ Lset γ ∈ˢ Lset lam ⟩
```

The supplied relation `γ ∈ lam` gives the last ambient-stage membership.
Applying `Lset∈Lλ` at `γ` yields `Lset γ ∈ Lset lam`. The three entries
`Lset d`, `d`, and `Lset γ` are now all legitimate elements of the stage
structure, so the completeness witness from `stageA` can be stated there.
This use of `γ` needs no claim that it is least or uniquely determined.

```agda
      Lγ∈Lλ = Lset∈Lλ γ γ∈λ
```

The constant named by the fixed-index query must be an element of the hull's
carrier, not merely an ambient set. Pairing `d` with the given proof
`d ∈ M` produces `dM : A.SM`. Its underlying set is definitionally `d`, so
the equality argument passed to `stageA` is reflexivity. This packaging does
not create a new representative or invoke the collapse; it presents the
existing hull member in the language in which elementarity is stated.

```agda
      dM : A.SM
      dM = d , d∈M
```

Full elementarity now acts on `findA`. The preceding call to `stageA` proves
the relabelled query in the stage structure on `Lset lam`; the symmetric
direction of `elem` transports that satisfaction to the hull structure.
This step may carry the three unbounded existential quantifiers because
`elem` applies to arbitrary formulas. It must therefore be distinguished
from `Cy.atL`, which was used only on the Δ₀ core `levelFo`. The result
`hullSat` says merely that a suitable triple exists in the hull.

```agda
      hullSat : ⟨ [] Mse.⊨ findA dM ⟩
      hullSat = subst ⟨_⟩ (sym (elem 0 (findA dM) []))
        (stageA d γ od adγ d∈γ dM refl d∈Lλ Ld∈Lλ Lγ∈Lλ)
```

To turn an answer to `findA` into the desired witness, suppose its outer two
coordinates `z` and `d′` have been exposed. The innermost existential then
provides a hull element `a`, satisfaction of the embedded core at
`(a,d′,z)`, and the equation `fst d′ ≡ d`. The helper `finishA` converts this
untruncated branch into a bound in `M`, membership of the prescribed
`Lset d` in `M`, and ambient satisfaction at `(Lset d,d,fst z)`. The
conversion will rely on soundness, not on uniqueness of the existential
witnesses.

```agda
      finishA : (z d' : A.SM)
              → Σ[ a ∈ A.SM ]
                  ( ⟨ (a ∷ d' ∷ z ∷ []) Mse.⊨ embed levelFo ⟩
                  × (fst d' ≡ d) )
              → Σ[ w ∈ S ] ( ⟨ w ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
```

The embedded core is first read back in the ambient hierarchy. Because
`levelFo` is Δ₀, the bounded comparison `Cy.atM` identifies its satisfaction in the hull structure
at `(a,d′,z)` with ambient satisfaction at the underlying sets
`(fst a,fst d′,fst z)`. This bounded step acts only on the core
already obtained after the existential witnesses were exposed. It does not
eliminate the unbounded query or by itself identify the first coordinate as
a constructible stage.

```agda
                           × ⟨ (Lset d ∷ d ∷ w ∷ []) ⊨ₚ levelFo ⟩ )
      finishA z d' (a , sat , ed) = fst z , snd z , Ld∈M , amb'
        where
        amb : ⟨ (fst a ∷ fst d' ∷ fst z ∷ []) ⊨ₚ levelFo ⟩
        amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (a ∷ d' ∷ z ∷ [])) sat
```

The soundness theorem for `levelFo` requires all three underlying sets to be
constructible. Each is a member of the hull, hence belongs to `Lset lam` by
`Hull⊆L`; since `lam` is ordinal, `isLλ` turns those three memberships into
the required constructibility proofs. With these separate hypotheses and
the ambient satisfaction `amb`, `level-sound` identifies
`fst a` with `Lset (fst d′)`. Satisfaction alone would not justify this
identification.

```agda
        ea : fst a ≡ Lset d
        ea = level-sound (fst a) (fst d') (fst z)
               (isLλ (fst a) (Hull⊆L (fst a) (snd a)))
               (isLλ (fst d') (Hull⊆L (fst d') (snd d')))
               (isLλ (fst z) (Hull⊆L (fst z) (snd z))) amb
```

The equality conjunct of `findA` now does the work for which it was designed.
Soundness gave `fst a ≡ Lset (fst d′)`, and applying `Lset` to
`ed : fst d′ ≡ d` gives `Lset (fst d′) ≡ Lset d`. Composing the two paths
yields `ea : fst a ≡ Lset d`. Thus the returned first coordinate is the
stage at the original prescribed index. Without the equality conjunct, the
same soundness argument would identify it only as the stage at some returned
index.

```agda
             ∙ cong Lset ed
```

The returned coordinate `a` already carries `snd a`, its membership in the
hull. Transporting that proposition along `ea` yields
`Lset d ∈ M`. This is the closure fact sought for the prescribed hull
ordinal `d`. It is derived from the hypothesis `sup`, full elementarity, bounded
absoluteness, and soundness of the level description; no additional closure
axiom for `M` is assumed, and the Mostowski collapse has not yet entered this
part of the argument.

```agda
        Ld∈M : ⟨ Lset d ∈ˢ M ⟩
        Ld∈M = subst (λ w → ⟨ w ∈ˢ M ⟩) ea (snd a)
```

The witness package also retains a correctly oriented copy of the level
description. Starting with ambient satisfaction at
`(fst a,fst d′,fst z)`, transport the middle coordinate along `ed` and the
first coordinate along `ea`. The result is satisfaction at
`(Lset d,d,fst z)`, exactly the third field of `Witness d`. Together with
`snd z` and the newly obtained `Lset d ∈ M`, it forms the untruncated branch
that will be placed back under propositional truncation.

```agda
        amb' : ⟨ (Lset d ∷ d ∷ fst z ∷ []) ⊨ₚ levelFo ⟩
        amb' = subst (λ v → ⟨ (v ∷ d ∷ fst z ∷ []) ⊨ₚ levelFo ⟩) ea
          (subst (λ p → ⟨ (fst a ∷ p ∷ fst z ∷ []) ⊨ₚ levelFo ⟩) ed amb)
```

After `z` and `d′` are fixed, the innermost existential asserts only the mere existence of a suitable `a`. Every explicit `a` determines, through `finishA`, the desired truncated witness for `d`; mapping under the truncation therefore preserves exactly the existence needed. The construction never exposes a selected `a`, and the remaining coordinates will be treated with the same propositional restriction.

```agda
      takeD : (z : A.SM)
            → Σ[ d' ∈ A.SM ]
                ⟨ (d' ∷ z ∷ []) Mse.⊨ ∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM)) ⟩
            → Witness d
      takeD z (d' , hd) = PT.map (finishA z d') hd
```

With the outer witness `z` already fixed, the next truncation hides the middle coordinate `d′`. Eliminating it into the proposition `Witness d` passes each local `d′` to the preceding construction. The enclosing elimination, already used in `step1`, handles the outer witness `z`. Consequently the witnesses from superadequacy and all three existential quantifiers remain local to propositional conclusions; neither an adequate bound nor a triple of hull witnesses is selected as global data.

```agda
      takeZ : Σ[ z ∈ A.SM ]
                ⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))) ⟩
            → Witness d
      takeZ (z , hz) = PT.rec squash₁ (takeD z) hz
```

We can now state the local compatibility between the collapse and constructible stages. If `d` is an ordinal in the hull, `commute` proves both that `Lset d` is again in the hull and that collapsing this stage gives `Lset (π d)`. The proof eliminates `Witness d` into a product of propositions. Hull membership is proposition-valued, and equality between the two ambient sets is a proposition because the ambient cumulative hierarchy is an h-set. Their product is therefore a valid target for eliminating propositional truncation.

```agda
  commute : (d : S) → IsOrd d → (d∈M : ⟨ d ∈ˢ M ⟩)
          → ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d))
  commute d od d∈M =
    PT.rec (isProp× (snd (Lset d ∈ˢ M)) (isSetS (π (Lset d)) (Lset (π d))))
           go (witness d od d∈M)
```

After opening the witness locally, its hull-membership component for `Lset d` supplies the first conclusion unchanged. The other two pieces, a hull member `z` and satisfaction of `levelFo(Lset d,d,z)`, are retained for the equality. This division mirrors the two conclusions of `commute`: closure of the hull at the stage indexed by `d` comes directly from `Witness d`, whereas compatibility with the collapse still has to be proved from the bounded description of that stage.

```agda
    where
    go : Σ[ z ∈ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
                    × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ )
       → ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d))
    go (z , z∈M , Ld∈M , amb) = Ld∈M , eq
```

The equality proof first transports the bounded description through the collapse. The environment consists of the three hull members `Lset d`, `d`, and `z`, together with their membership proofs. Since `levelFo` is Δ₀ and has no constants, `Cy.push` replaces every coordinate by its collapsed value and yields satisfaction of `levelFo(π (Lset d),π d,π z)`. This is the same local Δ₀ transport used earlier for ordinality, now applied to the three-variable description of a constructible stage.

```agda
      where
      pushed : ⟨ (π (Lset d) ∷ π d ∷ π z ∷ []) ⊨ₚ levelFo ⟩
      pushed = Cy.push Δ₀-levelFo ((Lset d , Ld∈M) ∷ (d , d∈M) ∷ (z , z∈M) ∷ []) amb
```

To read this transported formula by soundness, all three collapsed coordinates must be constructible. Each coordinate belongs to the collapse image by `πX-intro`, since it is the collapse of a hull member; the pointwise hypothesis `pixL` then supplies the required constructibility proofs. Soundness can therefore identify the first collapsed coordinate with the constructible stage indexed by the second:

`π (Lset d) ≡ Lset (π d)`.

The auxiliary value `π z` is needed to validate the description, but it does not occur in the resulting equality.

```agda
      eq : π (Lset d) ≡ Lset (π d)
      eq = level-sound (π (Lset d)) (π d) (π z)
             (pixL (π (Lset d)) (HS.C.πX-intro (Lset d) Ld∈M))
             (pixL (π d) (HS.C.πX-intro d d∈M))
             (pixL (π z) (HS.C.πX-intro z z∈M))
```

The transported satisfaction is the final premise of that soundness argument. Its conclusion must be read with the hypotheses of `commute`: the equation holds for an ordinal `d` that belongs to the hull. It is not a global equation between the two operations `π` and `Lset`. This precise locality is sufficient, because the two applications below first recover a relevant hull ordinal and only then invoke the compatibility equation.

```agda
             pushed
```

The first property required by the abstract condensation argument is closure at the image's own ordinals. Given an ordinal `δ` in the collapse image, `levelIn` must show that `Lset δ` also belongs to that image. The membership description `πX-member` provides, under propositional truncation, a hull member `d` with `π d ≡ δ`. Since the target is itself the membership proposition `Lset δ ∈ πX`, this truncated preimage may be opened locally.

```agda
  levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ HS.C.πX ⟩ → ⟨ Lset δ ∈ˢ HS.C.πX ⟩
  levelIn δ oδ δ∈πX =
    PT.rec (snd (Lset δ ∈ˢ HS.C.πX)) go (HS.C.πX-member δ δ∈πX)
    where
    go : Σ[ d ∈ S ] (⟨ d ∈ˢ M ⟩ × (π d ≡ δ)) → ⟨ Lset δ ∈ˢ HS.C.πX ⟩
```

Once such a preimage `d` is available, the desired image membership will come from `Lset d`. Indeed, `πX-intro` sends a proof that `Lset d` lies in the hull to a proof that `π (Lset d)` lies in the image. The final transport follows the compatibility equation `π (Lset d) ≡ Lset (π d)` and then applies `Lset` to the preimage equation `π d ≡ δ`. What remains is to justify that `d` is an ordinal and that `Lset d` lies in the hull.

```agda
    go (d , d∈M , e) =
      subst (λ w → ⟨ w ∈ˢ HS.C.πX ⟩) (cm .snd ∙ cong Lset e)
            (HS.C.πX-intro (Lset d) (cm .fst))
      where
      od : IsOrd d
```

Ordinality is recovered before the compatibility lemma is used. Transporting the assumed `IsOrd δ` backward along `π d ≡ δ` gives `IsOrd (π d)`, and `ord-pull` reflects this fact through the collapse to `IsOrd d`. Notice the order of the argument: the preimage description alone says only that `d` is a hull member. Its ordinality comes from the ordinality of `δ` together with reflection for the bounded ordinal formula.

```agda
      od = ord-pull d d∈M (subst IsOrd (sym e) oδ)
```

The hypotheses for `commute` are now complete. Its first component places `Lset d` in the hull, and its second gives `π (Lset d) ≡ Lset (π d)`. Composing the latter with `cong Lset e`, where `e : π d ≡ δ`, identifies this collapsed stage with `Lset δ`; transport then gives the required image membership. Hence the collapse image contains `Lset δ` for every ordinal `δ` that it contains. No closure claim is made for nonordinals or for ordinals outside the image.

```agda
      cm : ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d))
      cm = commute d od d∈M
```

The second property is covering. For every hull member `y`, it asks merely for an ordinal `γ` in the collapse image such that `π y ∈ Lset γ`. The ordinal, its membership in the image, and this level membership remain under one propositional truncation. Thus a covering stage exists for each `y`, but the theorem chooses no family of such stages and asserts neither minimality nor any comparison of their indices with `lam`.

```agda
  cover : (y : S) → ⟨ y ∈ˢ M ⟩
        → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁
  cover y y∈M = PT.rec squash₁ go (Lset-out lam y (Hull⊆L y y∈M))
    where
    Goal : Type (ℓ-suc ℓ)
```

The target `Goal` is itself a propositional truncation. This matters twice: the decomposition of `y` supplied by `Lset-out` and the adequate index supplied by superadequacy can both be used locally because their common destination is a proposition. Neither step fixes the final covering index. That index will instead come from the internal answer to the membership query `findP`.

```agda
    Goal = ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁
```

The construction starts by locating `y` in the constructible hierarchy. Since every hull member lies in `Lset lam`, `Lset-out` yields, under propositional truncation, an index `c ∈ lam` such that `y` is a definable subset of `Lset c`. Set `p = sucV c`. After successor closure puts `p` back in `lam`, superadequacy supplies, again only under truncation, an adequate `γ ∈ lam` containing `p`. The prepared index `p` provides an external stage that contains `y`; it is not yet the index that the hull will return.

```agda
    go : Σ[ c ∈ S ] (⟨ c ∈ˢ lam ⟩ × ⟨ y ∈ˢ 𝒟ₒ (Lset c) ⟩) → Goal
    go (c , c∈λ , y∈D) = PT.rec squash₁ go₂ (sup p p∈λ)
      where
      p : S
      p = sucV c
```

The first auxiliary fact applies the assumed successor closure of `lam` to `c ∈ lam`. It yields `p ∈ lam` for `p = sucV c`. This relation is needed twice: superadequacy is invoked at `p`, and the later ambient witness must place both the ordinal `p` and the stage `Lset p` inside `Lset lam`. The one closure hypothesis on indices supports all of these uses.

```agda
      p∈λ : ⟨ p ∈ˢ lam ⟩
      p∈λ = succλ c c∈λ
```

The prepared index must also be ordinal. Because `lam` is ordinal and `c ∈ lam`, `mem-ord` gives `IsOrd c`; closure of ordinals under von Neumann successor then gives `IsOrd (sucV c)`, hence `IsOrd p`. This proof keeps two uses of successor distinct: `succλ` places the successor inside the outer index, while `suc-ord` proves that the successor is itself an ordinal.

```agda
      op : IsOrd p
      op = suc-ord (mem-ord {A = lam} ordλ c c∈λ)
```

The birth-stage information says `y ∈ 𝒟ₒ (Lset c)`. The successor-stage equation identifies this definable-power-set stage with `Lset (sucV c)`, so transport gives `y ∈ Lset p`. This is the reason for passing from `c` to its successor: the decomposition locates `y` as a definable subset over the stage at `c`, while `findP` needs ordinary membership in a constructible stage.

```agda
      y∈Lp : ⟨ y ∈ˢ Lset p ⟩
      y∈Lp = subst (λ w → ⟨ y ∈ˢ w ⟩) (sym (Lset-suc c)) y∈D
```

Opening the superadequacy witness locally gives an index `γ ∈ lam` with `p ∈ γ` and `Adequate γ`. These are precisely the hypotheses needed for completeness at the externally prepared index `p`. The pair `yM = (y,y∈M)` now regards `y` as an element of the hull's carrier, so it can occur as the constant parameter of `findP`. From this point onward the construction uses the query that fixes membership of `y`, rather than the earlier query that fixed a prescribed index.

```agda
      go₂ : Σ[ γ ∈ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ p ∈ˢ γ ⟩ × Adequate γ) → Goal
      go₂ (γ , γ∈λ , p∈γ , adγ) = PT.rec squash₁ takeZ hullSat
        where
        yM : A.SM
        yM = y , y∈M
```

Completeness at the adequate `γ` constructs an ambient answer to `findP` using the triple `(Lset p,p,Lset γ)`, and the previously proved membership places `y` in its first coordinate. The three required carrier memberships are supplied by `ord∈Lλ p`, `Lset∈Lλ p`, and `Lset∈Lλ γ`. Since `findP` contains unbounded existential quantifiers, the passage of this whole answer into the hull uses full elementarity. The result is an internal existential assertion that `yM` belongs to some correctly described stage.

```agda
        hullSat : ⟨ [] Mse.⊨ findP yM ⟩
        hullSat = subst ⟨_⟩ (sym (elem 0 (findP yM) []))
          (stageP y p γ op adγ p∈γ yM refl y∈Lp
            (ord∈Lλ p op p∈λ) (Lset∈Lλ p p∈λ) (Lset∈Lλ γ γ∈λ))
```

Opening the internal assertion locally gives three hull elements `u`, `a`, and `z`. Their underlying sets satisfy `levelFo(fst u,fst a,fst z)`, and the same answer records `y ∈ fst u`. From these facts one must obtain an ordinal in the collapse image whose level contains `π y`. The construction may form an explicit dependent sum for each local answer, but that sum is immediately returned beneath propositional truncation, so no covering index escapes as chosen data.

```agda
        finishP : (z a : A.SM)
                → Σ[ u ∈ A.SM ]
                    ( ⟨ (u ∷ a ∷ z ∷ []) Mse.⊨ embed levelFo ⟩
                    × ⟨ y ∈ˢ fst u ⟩ )
                → Σ[ β ∈ S ] (IsOrd β × ⟨ β ∈ˢ HS.C.πX ⟩
```

The output witness is chosen locally as `β = π p′`, where `p′` is the underlying set of the middle hull coordinate `a`. Once `p′` is shown ordinal, `ord-push` proves that `π p′` is ordinal, and `πX-intro` places it in the collapse image because `a` certifies `p′ ∈ M`. The remaining component is `π y ∈ Lset (π p′)`. Establishing it requires first reading the formula answer in the ambient hierarchy and then relating membership to the local compatibility equation.

```agda
                              × ⟨ π y ∈ˢ Lset β ⟩)
        finishP z a (u , sat , y∈u) =
          π p′ , ord-push p′ (snd a) op′ , HS.C.πX-intro p′ (snd a) , πy∈
          where
          amb : ⟨ (fst u ∷ fst a ∷ fst z ∷ []) ⊨ₚ levelFo ⟩
```

The internal satisfaction proof concerns `embed levelFo` in the hull structure. Because its core `levelFo` is Δ₀, `Cy.atM` reads that proof as ambient satisfaction of `levelFo` at the same three underlying sets `(fst u,fst a,fst z)`. No coordinate is collapsed in this step. Its role is to leave the internal semantics of the hull and recover an ambient statement to which `isOrd-at-p-out` and `level-sound` can be applied.

```agda
          amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (u ∷ a ∷ z ∷ [])) sat
```

Let `p′ = fst a` be the middle coordinate returned inside the hull. It need not equal the externally prepared successor `p = sucV c`. The external triple established that `findP yM` was satisfiable, but `findP` fixes only the membership of `yM` in its first coordinate; it contains no equation fixing the middle coordinate. Full elementarity therefore supplies merely some internal index `p′` under propositional truncation, and the remainder of the proof uses this returned index.

```agda
          p′ : S
          p′ = fst a
```

The returned index is nevertheless known to be ordinal. The ambient satisfaction `amb` contains, as the first conjunct of `levelFo`, the three-slot ordinal description at its middle coordinate. Applying the reading lemma `isOrd-at-p-out` to that conjunct gives `IsOrd p′`. This conclusion concerns the internal preimage index `p′`; the ordinal used in `Goal` is its collapse `π p′`, whose ordinality is obtained separately by `ord-push`.

```agda
          op′ : IsOrd p′
          op′ = isOrd-at-p-out (fst u) p′ (fst z) (amb .fst)
```

Soundness now identifies the first coordinate of the internal answer. Since `u`, `a`, and `z` are hull elements, `Hull⊆L` places their underlying sets in `Lset lam`, and `isLλ` proves each one constructible. Together with `amb`, these three premises give `fst u ≡ Lset p′`. Thus the recorded fact `y ∈ fst u` can be transported to `y ∈ Lset p′`. The auxiliary bound `fst z` need not be unique, and no equality between `p′` and the prepared `p` is used; soundness determines the stage value solely from the returned ordinal index.

```agda
          u≡ : fst u ≡ Lset p′
          u≡ = level-sound (fst u) p′ (fst z)
                 (isLλ (fst u) (Hull⊆L (fst u) (snd u)))
                 (isLλ p′ (Hull⊆L p′ (snd a)))
                 (isLλ (fst z) (Hull⊆L (fst z) (snd z))) amb
```

The returned level value `fst u` is identified with `Lset p′` by `u≡`. Transporting the recorded membership `y∈u` along this equality therefore gives `y ∈ Lset p′`. This step uses only substitution in the set being joined; it does not impose any relation between the returned index `p′` and the previously prepared index `p`.

```agda
          y∈Lp′ : ⟨ y ∈ˢ Lset p′ ⟩
          y∈Lp′ = subst (λ v → ⟨ y ∈ˢ v ⟩) u≡ y∈u
```

The returned middle coordinate supplies exactly the data needed by the local commutation theorem. Its underlying set is `p′`; `op′` proves that this set is an ordinal, and `snd a` proves that it belongs to the hull. Hence `commute p′ op′ (snd a)` yields both `Lset p′ ∈ M` and the equation `π (Lset p′) ≡ Lset (π p′)`. The theorem is local to ordinals in the hull, which is precisely the situation established here.

```agda
          cm : ⟨ Lset p′ ∈ˢ M ⟩ × (π (Lset p′) ≡ Lset (π p′))
          cm = commute p′ op′ (snd a)
```

Both endpoints of `y∈Lp′` are hull members: `y∈M` gives the first, while `cm .fst` gives the second for `Lset p′`. The collapse therefore preserves this membership, producing `π y ∈ π (Lset p′)` through `member-push`. Substitution along `cm .snd` then changes the containing set to `Lset (π p′)`. Together with the preceding ordinal and image-membership proofs for `π p′`, this is the covering witness required by `finishP`.

```agda
          πy∈ : ⟨ π y ∈ˢ Lset (π p′) ⟩
          πy∈ = subst (λ w → ⟨ π y ∈ˢ w ⟩) (cm .snd)
                  (Cy.member-push (Lset p′) y (cm .fst) y∈M y∈Lp′)
```

For fixed `z` and `a`, the last existential states merely that a suitable `u` exists. Every explicit answer determines the ordinal `π p′`, its membership in the collapse image, and the proof `π y ∈ Lset (π p′)` constructed above. Mapping this construction under propositional truncation preserves the existence of a covering ordinal without selecting a particular answer to the query.

```agda
        takeA : (z : A.SM)
              → Σ[ a ∈ A.SM ]
                  ⟨ (a ∷ z ∷ []) Mse.⊨ ∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero)) ⟩
              → Goal
        takeA z (a , ha) = PT.map (finishP z a) ha
```

The two remaining existential layers obey the same restriction. After `z` is fixed, the middle witness `a` may be used because the destination `Goal` is a proposition; the enclosing elimination treats `z` in the same way. All three coordinates of the internal answer are therefore available only locally. The result proves a covering ordinal exists for each hull member, without producing a choice function of such ordinals.

```agda
        takeZ : Σ[ z ∈ A.SM ]
                  ⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))) ⟩
              → Goal
        takeZ (z , hz) = PT.rec squash₁ (takeA z) hz
```

The two established properties now determine the collapse image. Let `β` be the set of its ordinal members. Transitivity of the image, together with the fact that members of ordinals are ordinal, makes `β` an ordinal. If `x ∈ πX`, covering places `x` in some `Lset γ` with the ordinal `γ ∈ πX`; hence `γ ∈ β`, and monotonicity gives `x ∈ Lset β`. Conversely, decompose `x ∈ Lset β` at some `δ ∈ β`. Applying covering to the image member `δ` yields an ordinal `γ ∈ β` with `δ ∈ γ`. Then `x ∈ Lset γ`, while `levelIn` places `Lset γ` in the transitive image, so `x ∈ πX`. Extensionality gives `πX ≡ Lset β`.

```agda
  module Cn = HS.Condense levelIn cover using (condenses)
```

Thus there is an explicit set `β` with `IsOrd β` and `HS.C.πX ≡ Lset β`. The witness is not propositionally truncated: it is the set of ordinal members of the collapse image. This conclusion uses all the structural hypotheses of `Condense`, while its only classical parameter is `LEM (ℓ-suc ℓ)`. It makes no comparison between `β` and the outer index `lam`, and gives no cardinal estimate or injection; those require the additional constructions of later chapters.

```agda
  condenses : Σ[ β ∈ S ] (IsOrd β × (HS.C.πX ≡ Lset β))
  condenses = Cn.condenses
```