BedrockTransferring structure through condensation
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapThis 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(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.
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.
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.
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 β.
π : 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.
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.
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.
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.
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.
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.
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.
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.
∣ (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.
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.
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.
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′.
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.
∣ (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.
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.
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.
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.
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.
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.
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 γ.
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.
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.
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.
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.
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.
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.
× ⟨ (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.
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.
∙ 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
× ⟨ π 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.
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.
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.
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.
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.
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.
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.
π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.
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.
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 β.
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.
condenses : Σ[ β ∈ S ] (IsOrd β × (HS.C.πX ≡ Lset β)) condenses = Cn.condenses