Bedrock通过凝聚搬运结构
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图本章研究初等 Skolem 壳经过 Mostowski 塌缩后会变成什么。在序数索引 lam 处给定所需假设后，塌缩像将被认同为某个序数 β 所索引的 Lset β。这个结论不比较 β 与 lam，不选取最小的此类索引，也不给出基数估计。证明首先用一条有界一阶公式描述可构造层关系，使这项关系能在塌缩前后读取。
{-# OPTIONS --cubical --safe --guardedness #-}
定理以 ℓ-suc ℓ 层级上的排中律为参数。这一条经典假设被传给前文关于序数层、Skolem 壳、层级描述与充分层的结果。本章的论证不引入选择原理：存在公式的满足以及超充分性给出的局部层见证都保持为命题截断，因此只能在目标仍是命题时使用。
open import Base.Prelude open import Base.Classical using ( LEM )
现在固定宇宙层级与这一个经典参数。下文所有集合都属于层级 ℓ 上的外围累积层级；可构造层、Skolem 壳与塌缩像也是同一累积层级中的集合。完整初等性负责搬运带无界存在量词的公式。由层绝对性、初等性与塌缩同构构成的有界接口，则对外提供沿塌缩的 Δ₀ 搬运。区分这两种用法，是凝聚证明的关键。
module L.GCH.CondensationTransfer {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
下文两条查询只需对象语言中的隶属、相等、合取与无界存在量词。公式在外围层级、层与 Skolem 壳之间移动时，其常元字母表会随之改变。运算 mapFo 重标已有常元，而 embed 把一条无常元公式视为新常元字母表上的公式；两者都不改变公式的变元位置与逻辑结构。
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 ( 𝒮ᵥ )
可构造层级要求始终区分序数索引 d 与它所索引的层 Lset d。当 lam 是序数时，Lset lam 的成员都是可构造的。反过来，若序数 d 属于 Lset lam，则秩比较把 d 放入 lam。向下刻画 Lset-out 只说一层的成员仅仅来自某个 c ∈ lam 处的 𝒟ₒ (Lset c)，并不保留选定的出生层。若有严格的索引关系 β ∈ α，单调性再把 Lset β 中的成员搬到 Lset α。
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 )
这里的核心公式是 levelFo(a,p,z)。它的 Δ₀ 证书允许使用有界绝对性，并可沿塌缩搬运。可靠性说明：当 a、p、z 都可构造时，满足该公式可推出 a ≡ Lset p；辅助界 z 不必唯一。完备性则在 γ 充分、p 是序数且 p ∈ γ 时，给出特定三元组 (Lset p,p,Lset γ) 对公式的满足。周围理论提供 Skolem 壳上的搬运，以及构造这类三元组所需的局部充分索引。
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 )
有穷向量记录公式求值所用的环境，乘积则组合证明中需要的隶属事实与相等事实。本章有若干存在性处于命题截断之下。构造子 ∣_∣₁ 把一份显式的局部见证放入截断；PT.rec 与 PT.map 随后只能用它产生另一个命题。特别地，超充分性给出的局部充分索引不会变成一族全局选定的数据。
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₁ )
当 d 是序数时，集合论后继 sucV d 是下一个序数索引；后继层等式 Lset (sucV d) ≡ 𝒟ₒ (Lset d) 也使用这个索引。这两项事实彼此相关，但后继索引与该索引处的层仍是不同的集合。空集另行出现，是因为 Skolem 壳构造需要一个已经属于外围索引的回退成员。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; module InfinitySet ) open InfinitySet {ℓ} using ( sucV )
打开取值为命题的层级结构后，载体 S 与外围隶属记号 _∈ˢ_ 得到固定。尖括号 ⟨_⟩ 取出一个真值所承载的证明类型。因此，d ∈ˢ lam、可构造层中的隶属以及塌缩像中的隶属，都是外围集合论陈述，应与公式内部的对象语言原子 _∈̇_ 区分。
open hPropStructure 𝒮ᵥ
外围语义给出长度为 n 的环境记号 S ^ n。公式的槽位从这种向量中读取；每个新绑定的存在见证都放在向量前端，把旧槽位向外推移。因此，后文三层嵌套的见证虽然从外到内依次引入 z、p、a，最终却按 (a,p,z) 的顺序读取。
module SemVᵃ = FOL.Semantics 𝒮ᵥ open SemVᵃ using ( _^_ )
识别层见证的公式
公式 isOrd-at-p 只使用三项环境的中间槽位。它的第一个合取支说明 p 传递，第二个合取支说明 p 的每个成员都传递。这里的两个函数把这两条有界子句拆成 IsOrd p 的两个字段。相邻的 a 与 z 在这条引理中不起作用；该引理既不读取 levelFo 的其余部分，也不把 a 认同为某个可构造层。
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₁ )
沿塌缩搬运层级信息
固定序数 lam，以及容纳 Skolem 壳的外围可构造层 Lset lam。该索引对集合论后继封闭，生成集 X 的每个成员都属于这一层，而 ∅ ∈ lam 提供构造 Skolem 壳时所需的默认元素。这组假设的最后一项是完整初等性：只要参数来自 Skolem 壳，每条公式在壳中与外围层中便有相同真值，其中也包括带无界量词的公式。
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 ∅∈λ)
另外两项假设分别提供局部层与可构造的塌缩值。Superadequate lam 说明：每个 d ∈ lam 仅仅包含于某个满足 γ ∈ lam 的充分序数索引 γ；命题截断既不保留选定的 γ，也不保留最小者。假设 pixL 是逐点的：塌缩像的每个成员都可构造。它尚未说明塌缩像本身是可构造集，更没有把该像认同为某个特定的层。
(sup : Superadequate lam) (pixL : (x : S) → ⟨ x ∈ˢ HullStage.C.πX lam ordλ succλ X X⊆L ∅∈λ ⟩ → ⟨ isL x ⟩) where
下面同时使用三个结构：Lset lam 上的外围结构、以 Skolem 壳成员为载体的结构，以及传递的塌缩像。一个壳元素同时携带底层集合及其属于 M 的证明。有界公式可以在前两个结构之间读取，也可以沿塌缩双向搬运；单条成员关系同样可以推过塌缩。这些 Δ₀ 接口只在完整初等性处理完无界存在查询以后使用。
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)
包含 Hull⊆L 是从 Skolem 壳成员通往外围层的基本桥梁：若 x ∈ M，则 x ∈ Lset lam。这条事实提供 A.inL 所需的层隶属证据，稍后还会经由 isLλ 把壳中返回的每个见证转为可构造集。它是 Skolem 壳逐点包含于该层的陈述，并不说明壳本身是该层的元素。
open HS.H using ( Hull⊆L )
以 M 表示由前述数据确定的 Skolem 壳。由 Hull⊆L，它的每个成员都属于 Lset lam；但这项记号本身既不说明整个 M 可构造，也不增添任何封闭性质。因此，后文每次使用塌缩时都会保留「其自变量属于 M」这一前提。
M : S M = HS.M
以 π 表示 Mostowski 塌缩映射，以 πX 表示它的传递像。在 Skolem 壳成员上，π 保持成员关系，并把有界真值认同为它们在像中的读法。接下来的问题是为 πX 证明足够的层闭合性质与覆盖性质，从而说明这个传递集恰好是某一层 Lset β。
π : S → S π = HS.C.π
由于 lam 是序数，属于 Lset lam 足以推出可构造性。辅助函数 isLλ 恰好封装这条蕴涵。Skolem 壳查询返回三个分量后，证明会在调用 level-sound 之前分别对三者应用它，因为仅仅满足 levelFo 并不会给出可靠性定理所要求的可构造性假设。
isLλ : (x : S) → ⟨ x ∈ˢ Lset lam ⟩ → ⟨ isL x ⟩ isLλ = Lset→isL lam ordλ
下面两条基本隶属引理为外围层准备见证。先设 d ∈ lam。后继封闭给出 sucV d ∈ lam；整个层 Lset d 作为一个元素属于 Lset (sucV d)；Lset-mono 再把这个元素搬入 Lset lam。结论 Lset d ∈ Lset lam 是集合之间的隶属关系，并非一层逐点包含于另一层。
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)
若 d 还是序数，则 ord∈Lset-suc 把索引 d 本身放入 Lset (sucV d)，再由同一次单调性搬运进入 Lset lam。两条引理合起来给出两个不同的层成员，即 d 与 Lset d。在外围层中见证层公式时，二者都要使用；它们的隶属都不能与推导起点的索引关系 d ∈ lam 混同。
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)
对 Skolem 壳成员 d，序数性可以正向穿过塌缩。Amb.isOrdAt-in 用无常元有界公式 isOrdAt 表达 IsOrd d；Cy.push 把这个 Δ₀ 真值从壳环境搬到含有 π d 的环境；Amb.isOrdAt-out 再把结果读成 IsOrd (π d)。有界性证书控制这次搬运，而 Cy.push 所封装的比较最终依赖 Skolem 壳的初等包含与塌缩同构。
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))
同一条有界描述也能反向搬运。从 IsOrd (π d) 出发，Cy.pull 把 isOrdAt 的真值带回原来的 Skolem 壳成员，再读成 IsOrd d。因此，塌缩在 M 的成员上保持并反映序数性。这是带有假设 d ∈ M 的局部等价，并不说明 π 对任意外围集合如何作用。
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))
第一条存在查询用于在 Skolem 壳中找回指定的层 Lset d。它的三个无界存在量词产生环境 (a,d′,z)。嵌入的核心要求 levelFo(a,d′,z)，第二个合取支中的等式则把返回的中间坐标固定为 d′ ≡ dM。只有 levelFo 是 Δ₀；外围查询 findA 并非有界公式，因此要把见证从外围层带入 Skolem 壳，必须使用完整初等性，不能仅靠 Δ₀ 绝对性。正是这条等式把 findA 与稍后的查询 findP 区分开来；后者返回的索引 p′ 不必等于外围预备的 p。
findA : A.SM → Formula A.SM 0 findA dM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))))
引理 stageA 构造一个外围见证，稍后由初等性把它拉回 Skolem 壳。它接收一个包含序数 d 的充分索引 γ、一个底层集合等于 d 的壳代表 dM，以及 d、Lset d、Lset γ 分别属于 Lset lam 的证据。完备性给出 levelFo(Lset d,d,Lset γ)；有界绝对性在层结构中读取这个核心，对象语言中的等式则使用从 dM 底层集合到 d 的路径。随后，三个无界存在子句在命题截断下分别由 Lset γ、d、Lset d 见证；这里没有声称 γ 是最小者。
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γ∈ =
外围见证分别是充分界 Lset γ、指定索引 d 及其所索引的层 Lset d。它们最终组成环境 (Lset d,d,Lset γ)，因此完备性给出层描述这一合取支。等式合取支需要 sym ed：查询要求返回索引等于 dM 的解释，而 ed 把该解释认同为 d。每个存在见证都被放在命题截断之下，所以这里只保留三元组的存在性，并未把这一个三元组选作典范数据。
∣ (Lset γ , Lγ∈) , ∣ (d , d∈) , ∣ (Lset d , Ld∈) , (sat , sym ed) ∣₁ ∣₁ ∣₁ where δ : HS.ASt.SL ^ 3 δ = (Lset d , Ld∈) ∷ (d , d∈) ∷ (Lset γ , Lγ∈) ∷ []
层描述的完备性给出这里的数学核心。由于 γ 充分、d 是序数且 d ∈ γ，三元组 (Lset d,d,Lset γ) 在外围层级中满足 levelFo。充分性把描述所用的各张表放进共同的界，序数性使 d 成为合法的层索引，而 d ∈ γ 则把该索引置于界下。余下的问题，是在 Lset lam 上的结构中读取同一条 Δ₀ 事实。
amb : ⟨ (Lset d ∷ d ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩ amb = level-complete γ adγ d od d∈γ
接下来必须把外围真值改写成 Lset lam 上的层结构中的真值，此时还没有进入 Skolem 壳。反向使用 Cy.atL，可在该层的三个已给成员处读取 Δ₀ 公式 levelFo。随后，路径 embed-map 把无内容的常元改名认同为 embed levelFo：levelFo 的常元域为空，尽管外围查询以 Skolem 壳元素为常元。这样，sat 恰好给出 stageA 所需的嵌入核心；完整初等性要等整个无界查询装配完毕后才会使用。
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)
第二条查询同样寻找满足层描述的三元组 (u,a,z)，但附加条件不同。它不把中间坐标认同为指定索引，而是要求名为 yM 的 Skolem 壳元素属于第一坐标 u。因此，它寻找的是某个包含 y 且得到正确描述的可构造层，而该层的索引保持未定。这正是覆盖论证所需的条件。
findP : A.SM → Formula A.SM 0 findP yM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))))
引理 stageP 为这条成员查询准备外围见证。它从序数 p、包含 p 的充分层 γ、命名 y 的 Skolem 壳元素 yM，以及 y ∈ Lset p 出发。另有三条成员关系分别把 p、Lset p 与 Lset γ 放进 Lset lam，从而使三个存在见证都能在层结构中使用。这里的 p 只用于构造一份外围见证。由于 findP 没有用等式固定中间坐标，初等性稍后返回的内部索引可以是另一个 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γ∈ =
同一个外围三元组 (Lset p,p,Lset γ) 见证层描述，但最后的合取支现在记录 yM 的解释属于 Lset p。这种平行构造凸显两条查询的数学差别：findA 保留指定索引，findP 则保留指定点的成员关系。因此，在第二种情形中，完整初等性可以返回另一个内部索引。
∣ (Lset γ , Lγ∈) , ∣ (p , p∈) , ∣ (Lset p , Lp∈) , (sat , mem) ∣₁ ∣₁ ∣₁ where δ : HS.ASt.SL ^ 3 δ = (Lset p , Lp∈) ∷ (p , p∈) ∷ (Lset γ , Lγ∈) ∷ []
完备性给出两条查询共用的核心。由 γ 的充分性、p 的序数性与 p ∈ γ，它证明 (Lset p,p,Lset γ) 在外围层级中满足 levelFo。这里应区分完备性给出什么与不给出什么：它验证这一个在外围备好的三元组，却不声称每个满足公式的三元组都使用 p，也不使稍后得到的内部索引唯一。
amb : ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩ amb = level-complete γ adγ p op p∈γ
与前一条查询相同，此处的搬运只发生在外围层级与 Lset lam 上的层结构之间。反向使用 Cy.atL，凭 levelFo 的 Δ₀ 证书，把三个底层集合处的外围满足读成它们的层代表处的满足。路径 embed-map 再把无常元核心放进外围 Skolem 壳查询的常元域。所得正是 stageP 所需的第一个合取支；这次有界搬运并未搬运任何无界量词。
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)
余下的合取支断言 yM 的解释属于 Lset p。它的底层集合是 fst yM，而路径 ey : fst yM ≡ y 可把给定的成员关系 y ∈ Lset p 反向搬到这个解释上。正是这次小改写把指定的点放进查询，同时不固定索引。初等性稍后返回三元组 (u,p′,z) 时，保留下来的结论将是 y ∈ u，并没有 p′ 与此处 p 之间的等式。
mem : ⟨ fst (A.inL yM) ∈ˢ Lset p ⟩ mem = subst (λ w → ⟨ w ∈ˢ Lset p ⟩) (sym ey) y∈Lp
对集合 d，Witness d 在命题截断下记录三项事实：某个界 z 属于 Skolem 壳，指定的层 Lset d 属于 Skolem 壳，并且 (Lset d,d,z) 在外围层级中满足 levelFo。这个类型可对任意 d 写下，但下文的构造同时需要 IsOrd d 与 d ∈ M。保留命题截断已经足以支持后面取命题值的闭合与等式结论，也避免把充分界误当作选定的数据。
Witness : S → Type (ℓ-suc ℓ) Witness d = ∥ Σ[ z ∈ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩ × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ ) ∥₁
构造首先把 Skolem 壳成员 d 放进外围层：Hull⊆L 给出 d ∈ Lset lam。然而，超充分性接收的是序数 lam 的成员，而不是其可构造层的任意成员。下一步建立的局部事实 d∈λ 恰好跨过这道差别。得到它以后，sup d d∈λ 只在 d 之上给出一个充分层；由于目标 Witness d 本身是命题，外层 PT.rec 可以使用这份被命题截断的供给。
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
为了恢复索引成员关系，对 d ∈ Lset lam 应用层反映引理。它的前提准确揭示这一步为何成立：模块参数说明 lam 是序数，调用方则说明 d 是序数。只有在这两项序数性前提下，d 属于 lam 处之层才能推出 d ∈ lam。这是序数索引之间的比较，并非任意集合都适用的一般秩原理。
d∈λ : ⟨ d ∈ˢ lam ⟩
d∈λ = ord∈Lset→∈ lam ordλ d od d∈Lλ
现在，后继封闭把索引关系转成 stageA 所需的第二条层成员关系。由 d ∈ lam，前面的引理 Lset∈Lλ 给出 Lset d ∈ Lset lam，这里整个 Lset d 是外层的一个元素。它与 d∈Lλ 合起来备好与 d 有关的两个坐标。最终的界 Lset γ 的成员资格要等超充分性给出 γ 后另行推出。
Ld∈Lλ : ⟨ Lset d ∈ˢ Lset lam ⟩ Ld∈Lλ = Lset∈Lλ d d∈λ
超充分性在命题截断下返回一个索引 γ，满足 γ ∈ lam、d ∈ γ 与 Adequate γ。对任意这样的三元组，step1 都会构造 Witness d：先在外围层中建立整条查询，再用初等性取得该查询在 Skolem 壳中的被截断存在回答，最后只把这个回答消去到被截断的见证目标。因此，证明可以在消去器内部临时使用 γ，却不会让某个 γ 的选择逸出成为定理数据。
step1 : Σ[ γ ∈ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ d ∈ˢ γ ⟩ × Adequate γ) → Witness d step1 (γ , γ∈λ , d∈γ , adγ) = PT.rec squash₁ takeZ hullSat where Lγ∈Lλ : ⟨ Lset γ ∈ˢ Lset lam ⟩
给定的关系 γ ∈ lam 产生最后一条外围层成员关系。在 γ 处应用 Lset∈Lλ，得到 Lset γ ∈ Lset lam。至此，Lset d、d 与 Lset γ 都是层结构中的合法元素，因而可在该结构中陈述 stageA 的完备性见证。这里既不需要 γ 最小，也不需要它唯一确定。
Lγ∈Lλ = Lset∈Lλ γ γ∈λ
固定索引查询所命名的常元必须是 Skolem 壳载体的元素，不能只是一个外围集合。把 d 与给定的 d ∈ M 证明配对，得到 dM : A.SM。它的底层集合依定义就是 d，所以传给 stageA 的等式证明是自反性。这次打包既不产生新的代表，也不调用塌缩；它只是把已有的 Skolem 壳成员呈现在初等性所使用的语言中。
dM : A.SM dM = d , d∈M
现在对 findA 使用完整初等性。前面对 stageA 的调用证明了改名后的查询在 Lset lam 上的层结构中成立；elem 的对称方向把这份满足搬到 Skolem 壳结构。因为 elem 适用于任意公式，这一步可以连同三个无界存在量词一起搬运。因此必须把它与 Cy.atL 区分开，后者只用于 Δ₀ 核心 levelFo。所得 hullSat 只说明 Skolem 壳中存在合适的三元组。
hullSat : ⟨ [] Mse.⊨ findA dM ⟩ hullSat = subst ⟨_⟩ (sym (elem 0 (findA dM) [])) (stageA d γ od adγ d∈γ dM refl d∈Lλ Ld∈Lλ Lγ∈Lλ)
为了把 findA 的回答转成所需见证，先设它外面的两个坐标 z 与 d′ 已在消去器中展开。最内层存在量词于是给出 Skolem 壳元素 a、嵌入核心在 (a,d′,z) 处的满足，以及等式 fst d′ ≡ d。辅助函数 finishA 把这个未截断的分支转换成三项数据：M 中的一个界、指定的 Lset d 对 M 的成员资格，以及 (Lset d,d,fst z) 处的外围满足。这次转换依赖可靠性，并不依赖存在见证的唯一性。
finishA : (z d' : A.SM) → Σ[ a ∈ A.SM ] ( ⟨ (a ∷ d' ∷ z ∷ []) Mse.⊨ embed levelFo ⟩ × (fst d' ≡ d) ) → Σ[ w ∈ S ] ( ⟨ w ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
首先把嵌入核心读回外围层级。由于 levelFo 是 Δ₀，有界比较 Cy.atM 把它在 Skolem 壳结构中于 (a,d′,z) 处的满足，认同为它在底层集合 (fst a,fst d′,fst z) 处的外围满足。这次有界步骤只作用于存在见证已经展开后取得的核心；它既不消去无界查询，也不会独自把第一坐标认同为可构造层。
× ⟨ (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
levelFo 的可靠性定理要求三个底层集合分别可构造。三者都是 Skolem 壳的成员，所以由 Hull⊆L 分别属于 Lset lam；又因为 lam 是序数，isLλ 把这三条成员关系转成所需的可构造性证明。将这些独立前提与外围满足 amb 一同交给 level-sound，便得到 fst a 与 Lset (fst d′) 的认同。仅有公式满足并不足以推出这项认同。
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
现在，findA 的等式合取支兑现了它的用途。可靠性已经给出 fst a ≡ Lset (fst d′)；把 Lset 作用于 ed : fst d′ ≡ d，又得到 Lset (fst d′) ≡ Lset d。复合两条路径便得 ea : fst a ≡ Lset d。因此，返回的第一坐标正是原先指定索引处的层。若没有这个等式合取支，同样的可靠性论证只能把它认同为某个返回索引处的层。
∙ cong Lset ed
返回的坐标 a 已经带有 snd a，即它属于 Skolem 壳的证明。沿 ea 搬运这个命题，得到 Lset d ∈ M。这就是对指定 Skolem 壳序数 d 所需的闭合事实。它由超充分性、完整初等性、有界绝对性与层描述的可靠性共同推出，并未为 M 另设闭合公理；这部分论证也尚未使用 Mostowski 塌缩。
Ld∈M : ⟨ Lset d ∈ˢ M ⟩ Ld∈M = subst (λ w → ⟨ w ∈ˢ M ⟩) ea (snd a)
见证包还要保留一份方向正确的层描述。从 (fst a,fst d′,fst z) 处的外围满足出发，先沿 ed 搬运中间坐标，再沿 ea 搬运第一坐标，得到 (Lset d,d,fst z) 处的满足，恰是 Witness d 的第三个字段。它与 snd z 以及刚得到的 Lset d ∈ M 合在一起，形成一个未截断分支，随后再放回命题截断之下。
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)
固定 z 与 d′ 后，最内层存在量词只保留某个合适的 a 仅仅存在。每个显式的 a 都可经 finishA 产生所需的 d 的截断见证，因此在截断内部作映射恰好保留了所需的存在性。构造不会暴露一个选定的 a，其余坐标也将服从同样的命题性限制。
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
最外层见证 z 已经固定以后，下一层截断隐藏的是中间坐标 d′。把它消去到命题 Witness d，就是把每个局部的 d′ 交给前面的构造。step1 中已经出现的外层消去则处理见证 z。因此，超充分性以及三个存在量词给出的见证都只局限于命题结论；充分界与壳中三元组都没有被选成全局数据。
takeZ : Σ[ z ∈ A.SM ]
⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))) ⟩
→ Witness d
takeZ (z , hz) = PT.rec squash₁ (takeD z) hz
现在可以陈述塌缩与可构造层之间的局部相容性。若 d 是 Skolem 壳中的序数，则 commute 同时证明 Lset d 仍在壳中，并且塌缩这一层得到 Lset (π d)。证明把 Witness d 消去到两个命题的乘积中。壳成员关系取值于命题，而两个外围集合之间的等式也是命题，因为外围累积层级是 h-集合。因此，两者的乘积是消去命题截断的合法目标。
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)
在局部打开见证后，其中关于 Lset d 的壳成员资格原样给出第一个结论。其余两项数据，即壳成员 z 与 levelFo(Lset d,d,z) 的满足关系，则留给等式证明使用。这一区分正好对应 commute 的两个结论：Skolem 壳在由 d 索引的层处闭合，直接来自 Witness d；而该层与塌缩的相容性，仍须由这层的有界描述推出。
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
等式证明首先把有界描述沿塌缩搬运。环境由三个 Skolem 壳成员 Lset d、d、z 及其成员资格证明组成。由于 levelFo 是无常元的 Δ₀ 公式，Cy.push 可把每个坐标换成其塌缩值，得到 levelFo(π (Lset d),π d,π z) 的满足关系。这与前文搬运序数性时使用的是同一种局部 Δ₀ 搬运，只是此处施用于描述可构造层的三变元公式。
where pushed : ⟨ (π (Lset d) ∷ π d ∷ π z ∷ []) ⊨ₚ levelFo ⟩ pushed = Cy.push Δ₀-levelFo ((Lset d , Ld∈M) ∷ (d , d∈M) ∷ (z , z∈M) ∷ []) amb
要用可靠性读取搬运后的公式，三个塌缩坐标都必须可构造。每个坐标都是某个 Skolem 壳成员的塌缩，故由 πX-intro 属于塌缩像；逐点假设 pixL 随即给出所需的可构造性证明。因此，可靠性可把第一个塌缩坐标认同为由第二个坐标索引的可构造层：
π (Lset d) ≡ Lset (π d)。
辅助值 π z 用于验证这项描述，但不出现在所得等式中。
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))
搬运后的满足关系是上述可靠性论证的最后一个前提。读取其结论时必须保留 commute 的假设：该等式只对属于 Skolem 壳的序数 d 成立。它不是运算 π 与 Lset 之间的全局等式。这样的局部性已经足够，因为下面两处应用都会先找回一个相关的壳中序数，然后才调用这条相容等式。
pushed
抽象凝聚论证要求的第一项性质，是塌缩像在自身序数处的层闭合。给定塌缩像中的序数 δ，levelIn 必须证明 Lset δ 也属于该像。成员刻画 πX-member 在命题截断下给出一个 Skolem 壳成员 d，满足 π d ≡ δ。目标本身是成员命题 Lset δ ∈ πX，所以可以在局部打开这个带命题截断的原像。
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 ⟩
取得这样的原像 d 后，所求的像成员资格将来自 Lset d。确实，若有 Lset d 属于 Skolem 壳的证明，πX-intro 就给出 π (Lset d) 属于塌缩像的证明。最后依次沿相容等式 π (Lset d) ≡ Lset (π d)，以及把 Lset 施于原像等式 π d ≡ δ 所得的等式作传输。余下要说明的是 d 为序数，并且 Lset d 属于壳。
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
调用相容引理之前，先恢复原像的序数性。沿 π d ≡ δ 反向传输假设 IsOrd δ，得到 IsOrd (π d)；ord-pull 再把这项事实穿过塌缩反映为 IsOrd d。这里的论证次序不可省略：原像刻画本身只说明 d 是 Skolem 壳成员；它的序数性来自 δ 的序数性与有界序数公式的反映性。
od = ord-pull d d∈M (subst IsOrd (sym e) oδ)
此时 commute 的各项前提已经齐备。它的第一分量把 Lset d 放入 Skolem 壳，第二分量给出 π (Lset d) ≡ Lset (π d)。把后一个等式与 cong Lset e 复合，其中 e : π d ≡ δ，便把这个塌缩层认同为 Lset δ；再作传输即得所求的像成员资格。因此，塌缩像对其所含的每个序数 δ 都包含 Lset δ。这里没有对非序数或像外序数作闭合断言。
cm : ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d)) cm = commute d od d∈M
第二项性质是覆盖。对每个 Skolem 壳成员 y，它只要求塌缩像中仅仅存在一个序数 γ，使 π y ∈ Lset γ。该序数、它属于塌缩像的证明以及这条层成员关系，都保留在同一个命题截断之下。因此，每个 y 都有覆盖层，但定理没有选出这样的一族层，也不断言其索引最小或与 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 ℓ)
目标 Goal 本身就是命题截断。这一点会使用两次：Lset-out 给出的 y 的分解，以及超充分性给出的充分索引，都能在局部使用，因为它们共同到达一个命题。两步都不固定最终的覆盖索引；该索引将来自成员查询 findP 的内部回答。
Goal = ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁
构造先在可构造层级中定位 y。每个 Skolem 壳成员都属于 Lset lam，所以 Lset-out 在命题截断下给出一个索引 c ∈ lam，使 y 是 Lset c 的可定义子集。令 p = sucV c。后继闭合把 p 放回 lam 后，超充分性再次仅在命题截断下给出一个包含 p 的充分索引 γ ∈ lam。预备的索引 p 提供一个含有 y 的外围层；它尚不是 Skolem 壳随后返回的索引。
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
第一项辅助事实把 lam 的后继闭合假设施于 c ∈ lam，从而对 p = sucV c 得到 p ∈ lam。这项关系有两类用途：一方面要在 p 处调用超充分性，另一方面，稍后的外围见证必须把序数 p 与层 Lset p 都放入 Lset lam。关于索引的这一条闭合假设支撑了所有这些步骤。
p∈λ : ⟨ p ∈ˢ lam ⟩
p∈λ = succλ c c∈λ
预备的索引还必须是序数。由于 lam 是序数且 c ∈ lam，mem-ord 给出 IsOrd c；序数对 von Neumann 后继的闭合再给出 IsOrd (sucV c)，也就是 IsOrd p。这里区分了后继的两种用途：succλ 把后继放入外围索引，suc-ord 则证明该后继本身是序数。
op : IsOrd p op = suc-ord (mem-ord {A = lam} ordλ c c∈λ)
诞生层信息给出 y ∈ 𝒟ₒ (Lset c)。后继层等式把这个可定义幂集层认同为 Lset (sucV c)，因此传输得到 y ∈ Lset p。这正是从 c 转到其后继的原因：分解把 y 定位为 c 处之层上的可定义子集，而 findP 需要的是对某个可构造层的普通成员关系。
y∈Lp : ⟨ y ∈ˢ Lset p ⟩ y∈Lp = subst (λ w → ⟨ y ∈ˢ w ⟩) (sym (Lset-suc c)) y∈D
在局部打开超充分性见证，得到索引 γ ∈ lam、关系 p ∈ γ 与性质 Adequate γ。这些正是对外围预备索引 p 使用完备性所需的前提。二元组 yM = (y,y∈M) 此时把 y 视为壳载体的元素，使其能作为常元参数出现在 findP 中。从这里起，构造使用的是固定 y 之成员关系的查询，而不是前面固定指定索引的查询。
go₂ : Σ[ γ ∈ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ p ∈ˢ γ ⟩ × Adequate γ) → Goal go₂ (γ , γ∈λ , p∈γ , adγ) = PT.rec squash₁ takeZ hullSat where yM : A.SM yM = y , y∈M
在充分索引 γ 处，完备性以三元组 (Lset p,p,Lset γ) 构造 findP 的外围回答，而前一步所得的成员关系把 y 放入其第一坐标。所需的三项载体成员资格分别由 ord∈Lλ p、Lset∈Lλ p 与 Lset∈Lλ γ 给出。由于 findP 含有无界存在量词，把整个回答送入 Skolem 壳必须使用完整初等性。所得结论是一条内部存在断言：yM 属于某个被正确描述的层。
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λ γ γ∈λ))
在局部打开内部断言，得到三个 Skolem 壳元素 u、a、z。它们的底层集合满足 levelFo(fst u,fst a,fst z)，同一回答还记录 y ∈ fst u。现在要由这些事实取得塌缩像中的一个序数，使其所索引的层包含 π y。构造可以为每份局部回答形成显式依值和，但这份依值和立即被送回命题截断之下，所以覆盖索引不会作为选定数据逸出。
finishP : (z a : A.SM) → Σ[ u ∈ A.SM ] ( ⟨ (u ∷ a ∷ z ∷ []) Mse.⊨ embed levelFo ⟩ × ⟨ y ∈ˢ fst u ⟩ ) → Σ[ β ∈ S ] (IsOrd β × ⟨ β ∈ˢ HS.C.πX ⟩
输出见证在局部取为 β = π p′，其中 p′ 是中间壳坐标 a 的底层集合。一旦证明 p′ 为序数，ord-push 就证明 π p′ 为序数，而 a 所带的证明给出 p′ ∈ M，故 πX-intro 把 π p′ 放入塌缩像。余下的分量是 π y ∈ Lset (π p′)。要得到它，必须先在外围层级中读取公式回答，再把成员关系与局部相容等式结合起来。
× ⟨ π 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 ⟩
内部满足关系证明讨论的是壳结构中的 embed levelFo。由于其核心 levelFo 是 Δ₀ 公式，Cy.atM 把这项证明读成 levelFo 在同三个底层集合 (fst u,fst a,fst z) 处的外围满足关系。此步没有塌缩任何坐标；它的作用是离开 Skolem 壳的内部语义，恢复一条可供 isOrd-at-p-out 与 level-sound 使用的外围陈述。
amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (u ∷ a ∷ z ∷ [])) sat
令 p′ = fst a 为 Skolem 壳内部返回的中间坐标。它不必等于外围预备的后继 p = sucV c。外围三元组证明 findP yM 可满足，但 findP 只固定 yM 对第一坐标的成员关系，其中没有固定中间坐标的等式。因此，完整初等性只在命题截断下给出某个内部索引 p′，余下证明使用的是这个返回的索引。
p′ : S p′ = fst a
不过，仍可证明返回的索引是序数。外围满足关系 amb 的第一个合取支，是在中间坐标处读取的三槽序数描述。把读式引理 isOrd-at-p-out 施于该合取支，便得到 IsOrd p′。这一结论讨论的是内部原像索引 p′；Goal 中使用的序数是它的塌缩 π p′，后者的序数性另由 ord-push 得到。
op′ : IsOrd p′ op′ = isOrd-at-p-out (fst u) p′ (fst z) (amb .fst)
现在由可靠性识别内部回答的第一坐标。由于 u、a、z 都是 Skolem 壳元素，Hull⊆L 把它们的底层集合放入 Lset lam，isLλ 再分别证明三者可构造。结合 amb，这三个前提给出 fst u ≡ Lset p′。因此，回答中记录的 y ∈ fst u 可以传输为 y ∈ Lset p′。辅助界 fst z 不必唯一，证明也没有使用 p′ 与预备索引 p 之间的等式；可靠性只凭返回的序数索引确定层的取值。
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
可靠性等式 u≡ 把返回的层值 fst u 认同为 Lset p′。沿这条等式搬运已取得的成员关系 y∈u，便得到 y ∈ Lset p′。这里仅替换成员关系右侧的集合，并未在返回指标 p′ 与先前预备的指标 p 之间建立任何关系。
y∈Lp′ : ⟨ y ∈ˢ Lset p′ ⟩
y∈Lp′ = subst (λ v → ⟨ y ∈ˢ v ⟩) u≡ y∈u
返回的中间坐标恰好给出局部交换定理所需的数据。它的底层集合是 p′，op′ 证明该集合是序数，snd a 证明它属于壳。因此，commute p′ op′ (snd a) 同时给出 Lset p′ ∈ M 与等式 π (Lset p′) ≡ Lset (π p′)。该定理只针对壳中的序数，而这里已经满足这一适用条件。
cm : ⟨ Lset p′ ∈ˢ M ⟩ × (π (Lset p′) ≡ Lset (π p′)) cm = commute p′ op′ (snd a)
关系 y∈Lp′ 的两端都是壳成员：y∈M 给出 y 的壳成员资格，cm .fst 给出 Lset p′ 的壳成员资格。于是 member-push 保持这条成员关系，得到 π y ∈ π (Lset p′)；再沿 cm .snd 替换右侧集合，便得到 π y ∈ Lset (π p′)。结合前面关于 π p′ 的序数性与像中成员资格，这正是 finishP 所需的覆盖见证。
πy∈ : ⟨ π y ∈ˢ Lset (π p′) ⟩ πy∈ = subst (λ w → ⟨ π y ∈ˢ w ⟩) (cm .snd) (Cy.member-push (Lset p′) y (cm .fst) y∈M y∈Lp′)
固定 z 与 a 后，最后一个存在量词只断言某个合适的 u 仅仅存在。每份显式回答都确定上面构造出的序数 π p′、它对塌缩像的成员资格，以及证明 π y ∈ Lset (π p′)。在命题截断内部作这项映射，便保留覆盖序数的存在性，而不选定查询的某份特定回答。
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
余下两层存在量词服从同一限制。固定 z 后，可以使用中间见证 a，因为目标 Goal 是命题；外层消去以同样方式处理 z。因此，内部回答的三个坐标都只能在局部使用。所得结论证明每个 Skolem 壳成员都有覆盖序数，却不产生选择这类序数的函数。
takeZ : Σ[ z ∈ A.SM ]
⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))) ⟩
→ Goal
takeZ (z , hz) = PT.rec squash₁ (takeA z) hz
已经证明的两项性质现在确定塌缩像。令 β 为该像的序数成员所成的集合。像的传递性，加上序数成员的成员仍为序数这一事实，使 β 成为序数。若 x ∈ πX，覆盖性质把 x 放入某个 Lset γ，其中序数 γ ∈ πX；于是 γ ∈ β，单调性给出 x ∈ Lset β。反过来，把 x ∈ Lset β 分解到某个 δ ∈ β 处。对像中成员 δ 使用覆盖性质，得到序数 γ ∈ β 且 δ ∈ γ。于是 x ∈ Lset γ，而 levelIn 把 Lset γ 放进传递的塌缩像，故 x ∈ πX。外延性最终给出 πX ≡ Lset β。
module Cn = HS.Condense levelIn cover using (condenses)
于是得到显式集合 β，并有 IsOrd β 与 HS.C.πX ≡ Lset β。这个见证不在命题截断之下，因为它就是塌缩像的所有序数成员所成的集合。该结论使用 Condense 的全部结构性假设，而其唯一的经典参数是 LEM (ℓ-suc ℓ)。它不比较 β 与外层索引 lam，也不给出基数估计或单射；这些结论还需要后续章节中的附加构造。
condenses : Σ[ β ∈ S ] (IsOrd β × (HS.C.πX ≡ Lset β)) condenses = Cn.condenses