---
title: "通过凝聚搬运结构"
module: L.GCH.CondensationTransfer
lang: zh
site: "Bedrock"
description: "通过凝聚搬运结构"
stage: "证明 GCH"
reading_order: 107
canonical: https://bedrock.institute/zh/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/en/L.GCH.CondensationTransfer.md, https://bedrock.institute/ja/L.GCH.CondensationTransfer.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 通过凝聚搬运结构

本章研究初等 Skolem 壳经过 Mostowski 塌缩后会变成什么。在序数索引 `lam` 处给定所需假设后，塌缩像将被认同为某个序数 `β` 所索引的 `Lset β`。这个结论不比较 `β` 与 `lam`，不选取最小的此类索引，也不给出基数估计。证明首先用一条有界一阶公式描述可构造层关系，使这项关系能在塌缩前后读取。

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

定理以 `ℓ-suc ℓ` 层级上的排中律为参数。这一条经典假设被传给前文关于序数层、Skolem 壳、层级描述与充分层的结果。本章的论证不引入选择原理：存在公式的满足以及超充分性给出的局部层见证都保持为命题截断，因此只能在目标仍是命题时使用。

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

现在固定宇宙层级与这一个经典参数。下文所有集合都属于层级 `ℓ` 上的外围累积层级；可构造层、Skolem 壳与塌缩像也是同一累积层级中的集合。完整初等性负责搬运带无界存在量词的公式。由层绝对性、初等性与塌缩同构构成的有界接口，则对外提供沿塌缩的 Δ₀ 搬运。区分这两种用法，是凝聚证明的关键。

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

下文两条查询只需对象语言中的隶属、相等、合取与无界存在量词。公式在外围层级、层与 Skolem 壳之间移动时，其常元字母表会随之改变。运算 `mapFo` 重标已有常元，而 `embed` 把一条无常元公式视为新常元字母表上的公式；两者都不改变公式的变元位置与逻辑结构。

```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 ( 𝒮ᵥ )
```

可构造层级要求始终区分序数索引 `d` 与它所索引的层 `Lset d`。当 `lam` 是序数时，`Lset lam` 的成员都是可构造的。反过来，若序数 `d` 属于 `Lset lam`，则秩比较把 `d` 放入 `lam`。向下刻画 `Lset-out` 只说一层的成员仅仅来自某个 `c ∈ lam` 处的 `𝒟ₒ (Lset c)`，并不保留选定的出生层。若有严格的索引关系 `β ∈ α`，单调性再把 `Lset β` 中的成员搬到 `Lset α`。

```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 )
```

这里的核心公式是 `levelFo(a,p,z)`。它的 Δ₀ 证书允许使用有界绝对性，并可沿塌缩搬运。可靠性说明：当 `a`、`p`、`z` 都可构造时，满足该公式可推出 `a ≡ Lset p`；辅助界 `z` 不必唯一。完备性则在 `γ` 充分、`p` 是序数且 `p ∈ γ` 时，给出特定三元组 `(Lset p,p,Lset γ)` 对公式的满足。周围理论提供 Skolem 壳上的搬运，以及构造这类三元组所需的局部充分索引。

```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 )
```

有穷向量记录公式求值所用的环境，乘积则组合证明中需要的隶属事实与相等事实。本章有若干存在性处于命题截断之下。构造子 `∣_∣₁` 把一份显式的局部见证放入截断；`PT.rec` 与 `PT.map` 随后只能用它产生另一个命题。特别地，超充分性给出的局部充分索引不会变成一族全局选定的数据。

```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₁ )
```

当 `d` 是序数时，集合论后继 `sucV d` 是下一个序数索引；后继层等式 `Lset (sucV d) ≡ 𝒟ₒ (Lset d)` 也使用这个索引。这两项事实彼此相关，但后继索引与该索引处的层仍是不同的集合。空集另行出现，是因为 Skolem 壳构造需要一个已经属于外围索引的回退成员。

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

打开取值为命题的层级结构后，载体 `S` 与外围隶属记号 `_∈ˢ_` 得到固定。尖括号 `⟨_⟩` 取出一个真值所承载的证明类型。因此，`d ∈ˢ lam`、可构造层中的隶属以及塌缩像中的隶属，都是外围集合论陈述，应与公式内部的对象语言原子 `_∈̇_` 区分。

```agda
open hPropStructure 𝒮ᵥ
```

外围语义给出长度为 `n` 的环境记号 `S ^ n`。公式的槽位从这种向量中读取；每个新绑定的存在见证都放在向量前端，把旧槽位向外推移。因此，后文三层嵌套的见证虽然从外到内依次引入 `z`、`p`、`a`，最终却按 `(a,p,z)` 的顺序读取。

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

## 识别层见证的公式

公式 `isOrd-at-p` 只使用三项环境的中间槽位。它的第一个合取支说明 `p` 传递，第二个合取支说明 `p` 的每个成员都传递。这里的两个函数把这两条有界子句拆成 `IsOrd p` 的两个字段。相邻的 `a` 与 `z` 在这条引理中不起作用；该引理既不读取 `levelFo` 的其余部分，也不把 `a` 认同为某个可构造层。

```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₁ )
```

## 沿塌缩搬运层级信息

固定序数 `lam`，以及容纳 Skolem 壳的外围可构造层 `Lset lam`。该索引对集合论后继封闭，生成集 `X` 的每个成员都属于这一层，而 `∅ ∈ lam` 提供构造 Skolem 壳时所需的默认元素。这组假设的最后一项是完整初等性：只要参数来自 Skolem 壳，每条公式在壳中与外围层中便有相同真值，其中也包括带无界量词的公式。

```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 ∅∈λ)
```

另外两项假设分别提供局部层与可构造的塌缩值。`Superadequate lam` 说明：每个 `d ∈ lam` 仅仅包含于某个满足 `γ ∈ lam` 的充分序数索引 `γ`；命题截断既不保留选定的 `γ`，也不保留最小者。假设 `pixL` 是逐点的：塌缩像的每个成员都可构造。它尚未说明塌缩像本身是可构造集，更没有把该像认同为某个特定的层。

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

下面同时使用三个结构：`Lset lam` 上的外围结构、以 Skolem 壳成员为载体的结构，以及传递的塌缩像。一个壳元素同时携带底层集合及其属于 `M` 的证明。有界公式可以在前两个结构之间读取，也可以沿塌缩双向搬运；单条成员关系同样可以推过塌缩。这些 Δ₀ 接口只在完整初等性处理完无界存在查询以后使用。

```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)
```

包含 `Hull⊆L` 是从 Skolem 壳成员通往外围层的基本桥梁：若 `x ∈ M`，则 `x ∈ Lset lam`。这条事实提供 `A.inL` 所需的层隶属证据，稍后还会经由 `isLλ` 把壳中返回的每个见证转为可构造集。它是 Skolem 壳逐点包含于该层的陈述，并不说明壳本身是该层的元素。

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

以 `M` 表示由前述数据确定的 Skolem 壳。由 `Hull⊆L`，它的每个成员都属于 `Lset lam`；但这项记号本身既不说明整个 `M` 可构造，也不增添任何封闭性质。因此，后文每次使用塌缩时都会保留「其自变量属于 `M`」这一前提。

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

以 `π` 表示 Mostowski 塌缩映射，以 `πX` 表示它的传递像。在 Skolem 壳成员上，`π` 保持成员关系，并把有界真值认同为它们在像中的读法。接下来的问题是为 `πX` 证明足够的层闭合性质与覆盖性质，从而说明这个传递集恰好是某一层 `Lset β`。

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

由于 `lam` 是序数，属于 `Lset lam` 足以推出可构造性。辅助函数 `isLλ` 恰好封装这条蕴涵。Skolem 壳查询返回三个分量后，证明会在调用 `level-sound` 之前分别对三者应用它，因为仅仅满足 `levelFo` 并不会给出可靠性定理所要求的可构造性假设。

```agda
  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` 是集合之间的隶属关系，并非一层逐点包含于另一层。

```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)
```

若 `d` 还是序数，则 `ord∈Lset-suc` 把索引 `d` 本身放入 `Lset (sucV d)`，再由同一次单调性搬运进入 `Lset lam`。两条引理合起来给出两个不同的层成员，即 `d` 与 `Lset d`。在外围层中见证层公式时，二者都要使用；它们的隶属都不能与推导起点的索引关系 `d ∈ lam` 混同。

```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)
```

对 Skolem 壳成员 `d`，序数性可以正向穿过塌缩。`Amb.isOrdAt-in` 用无常元有界公式 `isOrdAt` 表达 `IsOrd d`；`Cy.push` 把这个 Δ₀ 真值从壳环境搬到含有 `π d` 的环境；`Amb.isOrdAt-out` 再把结果读成 `IsOrd (π d)`。有界性证书控制这次搬运，而 `Cy.push` 所封装的比较最终依赖 Skolem 壳的初等包含与塌缩同构。

```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))
```

同一条有界描述也能反向搬运。从 `IsOrd (π d)` 出发，`Cy.pull` 把 `isOrdAt` 的真值带回原来的 Skolem 壳成员，再读成 `IsOrd d`。因此，塌缩在 `M` 的成员上保持并反映序数性。这是带有假设 `d ∈ M` 的局部等价，并不说明 `π` 对任意外围集合如何作用。

```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))
```

第一条存在查询用于在 Skolem 壳中找回指定的层 `Lset d`。它的三个无界存在量词产生环境 `(a,d′,z)`。嵌入的核心要求 `levelFo(a,d′,z)`，第二个合取支中的等式则把返回的中间坐标固定为 `d′ ≡ dM`。只有 `levelFo` 是 Δ₀；外围查询 `findA` 并非有界公式，因此要把见证从外围层带入 Skolem 壳，必须使用完整初等性，不能仅靠 Δ₀ 绝对性。正是这条等式把 `findA` 与稍后的查询 `findP` 区分开来；后者返回的索引 `p′` 不必等于外围预备的 `p`。

```agda
  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` 见证；这里没有声称 `γ` 是最小者。

```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γ∈ =
```

外围见证分别是充分界 `Lset γ`、指定索引 `d` 及其所索引的层 `Lset d`。它们最终组成环境 `(Lset d,d,Lset γ)`，因此完备性给出层描述这一合取支。等式合取支需要 `sym ed`：查询要求返回索引等于 `dM` 的解释，而 `ed` 把该解释认同为 `d`。每个存在见证都被放在命题截断之下，所以这里只保留三元组的存在性，并未把这一个三元组选作典范数据。

```agda
    ∣ (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` 上的结构中读取同一条 Δ₀ 事实。

```agda
    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` 所需的嵌入核心；完整初等性要等整个无界查询装配完毕后才会使用。

```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)
```

第二条查询同样寻找满足层描述的三元组 `(u,a,z)`，但附加条件不同。它不把中间坐标认同为指定索引，而是要求名为 `yM` 的 Skolem 壳元素属于第一坐标 `u`。因此，它寻找的是某个包含 `y` 且得到正确描述的可构造层，而该层的索引保持未定。这正是覆盖论证所需的条件。

```agda
  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′`。

```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γ∈ =
```

同一个外围三元组 `(Lset p,p,Lset γ)` 见证层描述，但最后的合取支现在记录 `yM` 的解释属于 `Lset p`。这种平行构造凸显两条查询的数学差别：`findA` 保留指定索引，`findP` 则保留指定点的成员关系。因此，在第二种情形中，完整初等性可以返回另一个内部索引。

```agda
    ∣ (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`，也不使稍后得到的内部索引唯一。

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

与前一条查询相同，此处的搬运只发生在外围层级与 `Lset lam` 上的层结构之间。反向使用 `Cy.atL`，凭 `levelFo` 的 Δ₀ 证书，把三个底层集合处的外围满足读成它们的层代表处的满足。路径 `embed-map` 再把无常元核心放进外围 Skolem 壳查询的常元域。所得正是 `stageP` 所需的第一个合取支；这次有界搬运并未搬运任何无界量词。

```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)
```

余下的合取支断言 `yM` 的解释属于 `Lset p`。它的底层集合是 `fst yM`，而路径 `ey : fst yM ≡ y` 可把给定的成员关系 `y ∈ Lset p` 反向搬到这个解释上。正是这次小改写把指定的点放进查询，同时不固定索引。初等性稍后返回三元组 `(u,p′,z)` 时，保留下来的结论将是 `y ∈ u`，并没有 `p′` 与此处 `p` 之间的等式。

```agda
    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`。保留命题截断已经足以支持后面取命题值的闭合与等式结论，也避免把充分界误当作选定的数据。

```agda
  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` 可以使用这份被命题截断的供给。

```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
```

为了恢复索引成员关系，对 `d ∈ Lset lam` 应用层反映引理。它的前提准确揭示这一步为何成立：模块参数说明 `lam` 是序数，调用方则说明 `d` 是序数。只有在这两项序数性前提下，`d` 属于 `lam` 处之层才能推出 `d ∈ lam`。这是序数索引之间的比较，并非任意集合都适用的一般秩原理。

```agda
    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 γ` 的成员资格要等超充分性给出 `γ` 后另行推出。

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

超充分性在命题截断下返回一个索引 `γ`，满足 `γ ∈ lam`、`d ∈ γ` 与 `Adequate γ`。对任意这样的三元组，`step1` 都会构造 `Witness d`：先在外围层中建立整条查询，再用初等性取得该查询在 Skolem 壳中的被截断存在回答，最后只把这个回答消去到被截断的见证目标。因此，证明可以在消去器内部临时使用 `γ`，却不会让某个 `γ` 的选择逸出成为定理数据。

```agda
    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` 的完备性见证。这里既不需要 `γ` 最小，也不需要它唯一确定。

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

固定索引查询所命名的常元必须是 Skolem 壳载体的元素，不能只是一个外围集合。把 `d` 与给定的 `d ∈ M` 证明配对，得到 `dM : A.SM`。它的底层集合依定义就是 `d`，所以传给 `stageA` 的等式证明是自反性。这次打包既不产生新的代表，也不调用塌缩；它只是把已有的 Skolem 壳成员呈现在初等性所使用的语言中。

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

现在对 `findA` 使用完整初等性。前面对 `stageA` 的调用证明了改名后的查询在 `Lset lam` 上的层结构中成立；`elem` 的对称方向把这份满足搬到 Skolem 壳结构。因为 `elem` 适用于任意公式，这一步可以连同三个无界存在量词一起搬运。因此必须把它与 `Cy.atL` 区分开，后者只用于 Δ₀ 核心 `levelFo`。所得 `hullSat` 只说明 Skolem 壳中存在合适的三元组。

```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λ)
```

为了把 `findA` 的回答转成所需见证，先设它外面的两个坐标 `z` 与 `d′` 已在消去器中展开。最内层存在量词于是给出 Skolem 壳元素 `a`、嵌入核心在 `(a,d′,z)` 处的满足，以及等式 `fst d′ ≡ d`。辅助函数 `finishA` 把这个未截断的分支转换成三项数据：`M` 中的一个界、指定的 `Lset d` 对 `M` 的成员资格，以及 `(Lset d,d,fst z)` 处的外围满足。这次转换依赖可靠性，并不依赖存在见证的唯一性。

```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 ⟩
```

首先把嵌入核心读回外围层级。由于 `levelFo` 是 Δ₀，有界比较 `Cy.atM` 把它在 Skolem 壳结构中于 `(a,d′,z)` 处的满足，认同为它在底层集合 `(fst a,fst d′,fst z)` 处的外围满足。这次有界步骤只作用于存在见证已经展开后取得的核心；它既不消去无界查询，也不会独自把第一坐标认同为可构造层。

```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
```

`levelFo` 的可靠性定理要求三个底层集合分别可构造。三者都是 Skolem 壳的成员，所以由 `Hull⊆L` 分别属于 `Lset lam`；又因为 `lam` 是序数，`isLλ` 把这三条成员关系转成所需的可构造性证明。将这些独立前提与外围满足 `amb` 一同交给 `level-sound`，便得到 `fst a` 与 `Lset (fst d′)` 的认同。仅有公式满足并不足以推出这项认同。

```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
```

现在，`findA` 的等式合取支兑现了它的用途。可靠性已经给出 `fst a ≡ Lset (fst d′)`；把 `Lset` 作用于 `ed : fst d′ ≡ d`，又得到 `Lset (fst d′) ≡ Lset d`。复合两条路径便得 `ea : fst a ≡ Lset d`。因此，返回的第一坐标正是原先指定索引处的层。若没有这个等式合取支，同样的可靠性论证只能把它认同为某个返回索引处的层。

```agda
             ∙ cong Lset ed
```

返回的坐标 `a` 已经带有 `snd a`，即它属于 Skolem 壳的证明。沿 `ea` 搬运这个命题，得到 `Lset d ∈ M`。这就是对指定 Skolem 壳序数 `d` 所需的闭合事实。它由超充分性、完整初等性、有界绝对性与层描述的可靠性共同推出，并未为 `M` 另设闭合公理；这部分论证也尚未使用 Mostowski 塌缩。

```agda
        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` 合在一起，形成一个未截断分支，随后再放回命题截断之下。

```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)
```

固定 `z` 与 `d′` 后，最内层存在量词只保留某个合适的 `a` 仅仅存在。每个显式的 `a` 都可经 `finishA` 产生所需的 `d` 的截断见证，因此在截断内部作映射恰好保留了所需的存在性。构造不会暴露一个选定的 `a`，其余坐标也将服从同样的命题性限制。

```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
```

最外层见证 `z` 已经固定以后，下一层截断隐藏的是中间坐标 `d′`。把它消去到命题 `Witness d`，就是把每个局部的 `d′` 交给前面的构造。`step1` 中已经出现的外层消去则处理见证 `z`。因此，超充分性以及三个存在量词给出的见证都只局限于命题结论；充分界与壳中三元组都没有被选成全局数据。

```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
```

现在可以陈述塌缩与可构造层之间的局部相容性。若 `d` 是 Skolem 壳中的序数，则 `commute` 同时证明 `Lset d` 仍在壳中，并且塌缩这一层得到 `Lset (π d)`。证明把 `Witness d` 消去到两个命题的乘积中。壳成员关系取值于命题，而两个外围集合之间的等式也是命题，因为外围累积层级是 h-集合。因此，两者的乘积是消去命题截断的合法目标。

```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)
```

在局部打开见证后，其中关于 `Lset d` 的壳成员资格原样给出第一个结论。其余两项数据，即壳成员 `z` 与 `levelFo(Lset d,d,z)` 的满足关系，则留给等式证明使用。这一区分正好对应 `commute` 的两个结论：Skolem 壳在由 `d` 索引的层处闭合，直接来自 `Witness d`；而该层与塌缩的相容性，仍须由这层的有界描述推出。

```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
```

等式证明首先把有界描述沿塌缩搬运。环境由三个 Skolem 壳成员 `Lset d`、`d`、`z` 及其成员资格证明组成。由于 `levelFo` 是无常元的 Δ₀ 公式，`Cy.push` 可把每个坐标换成其塌缩值，得到 `levelFo(π (Lset d),π d,π z)` 的满足关系。这与前文搬运序数性时使用的是同一种局部 Δ₀ 搬运，只是此处施用于描述可构造层的三变元公式。

```agda
      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` 用于验证这项描述，但不出现在所得等式中。

```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))
```

搬运后的满足关系是上述可靠性论证的最后一个前提。读取其结论时必须保留 `commute` 的假设：该等式只对属于 Skolem 壳的序数 `d` 成立。它不是运算 `π` 与 `Lset` 之间的全局等式。这样的局部性已经足够，因为下面两处应用都会先找回一个相关的壳中序数，然后才调用这条相容等式。

```agda
             pushed
```

抽象凝聚论证要求的第一项性质，是塌缩像在自身序数处的层闭合。给定塌缩像中的序数 `δ`，`levelIn` 必须证明 `Lset δ` 也属于该像。成员刻画 `πX-member` 在命题截断下给出一个 Skolem 壳成员 `d`，满足 `π d ≡ δ`。目标本身是成员命题 `Lset δ ∈ πX`，所以可以在局部打开这个带命题截断的原像。

```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 ⟩
```

取得这样的原像 `d` 后，所求的像成员资格将来自 `Lset d`。确实，若有 `Lset d` 属于 Skolem 壳的证明，`πX-intro` 就给出 `π (Lset d)` 属于塌缩像的证明。最后依次沿相容等式 `π (Lset d) ≡ Lset (π d)`，以及把 `Lset` 施于原像等式 `π d ≡ δ` 所得的等式作传输。余下要说明的是 `d` 为序数，并且 `Lset d` 属于壳。

```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
```

调用相容引理之前，先恢复原像的序数性。沿 `π d ≡ δ` 反向传输假设 `IsOrd δ`，得到 `IsOrd (π d)`；`ord-pull` 再把这项事实穿过塌缩反映为 `IsOrd d`。这里的论证次序不可省略：原像刻画本身只说明 `d` 是 Skolem 壳成员；它的序数性来自 `δ` 的序数性与有界序数公式的反映性。

```agda
      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 δ`。这里没有对非序数或像外序数作闭合断言。

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

第二项性质是覆盖。对每个 Skolem 壳成员 `y`，它只要求塌缩像中仅仅存在一个序数 `γ`，使 `π y ∈ Lset γ`。该序数、它属于塌缩像的证明以及这条层成员关系，都保留在同一个命题截断之下。因此，每个 `y` 都有覆盖层，但定理没有选出这样的一族层，也不断言其索引最小或与 `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 ℓ)
```

目标 `Goal` 本身就是命题截断。这一点会使用两次：`Lset-out` 给出的 `y` 的分解，以及超充分性给出的充分索引，都能在局部使用，因为它们共同到达一个命题。两步都不固定最终的覆盖索引；该索引将来自成员查询 `findP` 的内部回答。

```agda
    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 壳随后返回的索引。

```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
```

第一项辅助事实把 `lam` 的后继闭合假设施于 `c ∈ lam`，从而对 `p = sucV c` 得到 `p ∈ lam`。这项关系有两类用途：一方面要在 `p` 处调用超充分性，另一方面，稍后的外围见证必须把序数 `p` 与层 `Lset p` 都放入 `Lset lam`。关于索引的这一条闭合假设支撑了所有这些步骤。

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

预备的索引还必须是序数。由于 `lam` 是序数且 `c ∈ lam`，`mem-ord` 给出 `IsOrd c`；序数对 von Neumann 后继的闭合再给出 `IsOrd (sucV c)`，也就是 `IsOrd p`。这里区分了后继的两种用途：`succλ` 把后继放入外围索引，`suc-ord` 则证明该后继本身是序数。

```agda
      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` 需要的是对某个可构造层的普通成员关系。

```agda
      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` 之成员关系的查询，而不是前面固定指定索引的查询。

```agda
      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` 属于某个被正确描述的层。

```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λ γ γ∈λ))
```

在局部打开内部断言，得到三个 Skolem 壳元素 `u`、`a`、`z`。它们的底层集合满足 `levelFo(fst u,fst a,fst z)`，同一回答还记录 `y ∈ fst u`。现在要由这些事实取得塌缩像中的一个序数，使其所索引的层包含 `π y`。构造可以为每份局部回答形成显式依值和，但这份依值和立即被送回命题截断之下，所以覆盖索引不会作为选定数据逸出。

```agda
        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′)`。要得到它，必须先在外围层级中读取公式回答，再把成员关系与局部相容等式结合起来。

```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 ⟩
```

内部满足关系证明讨论的是壳结构中的 `embed levelFo`。由于其核心 `levelFo` 是 Δ₀ 公式，`Cy.atM` 把这项证明读成 `levelFo` 在同三个底层集合 `(fst u,fst a,fst z)` 处的外围满足关系。此步没有塌缩任何坐标；它的作用是离开 Skolem 壳的内部语义，恢复一条可供 `isOrd-at-p-out` 与 `level-sound` 使用的外围陈述。

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

令 `p′ = fst a` 为 Skolem 壳内部返回的中间坐标。它不必等于外围预备的后继 `p = sucV c`。外围三元组证明 `findP yM` 可满足，但 `findP` 只固定 `yM` 对第一坐标的成员关系，其中没有固定中间坐标的等式。因此，完整初等性只在命题截断下给出某个内部索引 `p′`，余下证明使用的是这个返回的索引。

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

不过，仍可证明返回的索引是序数。外围满足关系 `amb` 的第一个合取支，是在中间坐标处读取的三槽序数描述。把读式引理 `isOrd-at-p-out` 施于该合取支，便得到 `IsOrd p′`。这一结论讨论的是内部原像索引 `p′`；`Goal` 中使用的序数是它的塌缩 `π p′`，后者的序数性另由 `ord-push` 得到。

```agda
          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` 之间的等式；可靠性只凭返回的序数索引确定层的取值。

```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
```

可靠性等式 `u≡` 把返回的层值 `fst u` 认同为 `Lset p′`。沿这条等式搬运已取得的成员关系 `y∈u`，便得到 `y ∈ Lset p′`。这里仅替换成员关系右侧的集合，并未在返回指标 `p′` 与先前预备的指标 `p` 之间建立任何关系。

```agda
          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′)`。该定理只针对壳中的序数，而这里已经满足这一适用条件。

```agda
          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` 所需的覆盖见证。

```agda
          π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′)`。在命题截断内部作这项映射，便保留覆盖序数的存在性，而不选定查询的某份特定回答。

```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
```

余下两层存在量词服从同一限制。固定 `z` 后，可以使用中间见证 `a`，因为目标 `Goal` 是命题；外层消去以同样方式处理 `z`。因此，内部回答的三个坐标都只能在局部使用。所得结论证明每个 Skolem 壳成员都有覆盖序数，却不产生选择这类序数的函数。

```agda
        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 β`。

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

于是得到显式集合 `β`，并有 `IsOrd β` 与 `HS.C.πX ≡ Lset β`。这个见证不在命题截断之下，因为它就是塌缩像的所有序数成员所成的集合。该结论使用 `Condense` 的全部结构性假设，而其唯一的经典参数是 `LEM (ℓ-suc ℓ)`。它不比较 `β` 与外层索引 `lam`，也不给出基数估计或单射；这些结论还需要后续章节中的附加构造。

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