---
title: "构造并塌缩 Skolem 壳"
module: L.GCH.SkolemHull
lang: zh
site: "Bedrock"
description: "构造并塌缩 Skolem 壳"
stage: "证明 GCH"
reading_order: 105
canonical: https://bedrock.institute/zh/L.GCH.SkolemHull.html
html: L.GCH.SkolemHull.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/SkolemHull.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Absoluteness, FOL.Manipulation.ConstantOccurrences, FOL.Semantics, FOL.Manipulation.ParameterAbstraction, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.Renaming, V.Hierarchy, V.Presentation, V.Collapse, V.Smallness, L.Axioms.Basic, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Rank, L.WellOrder.Base, L.Choice.StageOrders, L.Coding.CodeConstructibility]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.SkolemHull.md, https://bedrock.institute/ja/L.GCH.SkolemHull.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 构造并塌缩 Skolem 壳

本章在可构造层内对起始集合作 Skolem 壳，证明壳在层中初等，再经保持隶属的双射把它塌缩到传递集上，并整理满足关系与有界公式如何跨过这次塌缩。关键区别是：壳本身只是编码所得的像；传递性只在 Mostowski 塌缩之后出现。

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

本章依赖经典逻辑，假设在此引入。壳的构造要判定查询的可满足性，外延性证明要双向判定隶属，初等性移送要消去双重否定；这些步骤都在消耗排中律。

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

模块把宇宙层级固定为 `ℓ`，并按本书的固定形式陈述经典假设：排中律以显式参数在 `ℓ-suc ℓ` 处领取，从不全局假设，因此本章每条定理都准确记录所用的是哪个层级的实例。

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

对象语言即本书的一阶语言：公式由项经等词与隶属构成，对命题联结词、非有界量词与有界量词封闭。谓词 `Δ₀` 挑出全部量词都有界的公式。

```agda
open import FOL.ZFStructure using ( ZFStructure; module hPropStructure; _↾_ )
open import FOL.Syntax using
  ( Formula; Term; con; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊥̇
  ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
```

谓词 `Δ₀` 是沿公式结构定义的归纳证书：其构造子覆盖原子式、联结词与有界量词，而无界量词没有对应构造子。这种证书支撑后文的绝对性论证；`countFo` 与 `constantsFo` 记录常元的每次出现。

```agda
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Absoluteness
import FOL.Manipulation.ConstantOccurrences
import FOL.Semantics
open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo )
```

参数抽象用额外的环境变元替换常元出现；常元映射与常元改名在保持语义的同时改变常元字母表；`renameTm` 则沿语境映射改名变元槽，由此得到下文以 `suc` 实现的弱化。外围层级连同其外延性一同打开，外延性即成员相同的集合相等。

```agda
open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm; mapFo-comp; embed )
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀; ⊨-map )
open import FOL.Manipulation.Renaming using ( renameTm )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
```

呈现用一个带嵌入的小类型索引集合的元素，其纤维为被呈现元素命名。塌缩对任意载体 `X` 构造一个传递像；要使塌缩映射在 `X` 上单射，还需受限隶属关系满足外延性。Δ₀ 小性把有界可定义的类分离成集合。空集属于每个可定义性后继，而 `Lset-suc` 把后继指标处的层认同为前一层的可定义幂集。

```agda
open import V.Presentation {ℓ} using ( member; fiber )
open import V.Collapse {ℓ} using ( module Collapse; isExt; isTrans )
open import V.Smallness {ℓ} using ( separateFromSmall; module Δ₀Small )
open import L.Axioms.Basic {ℓ} using ( ∅∈𝒟ₒ; Lset-suc )
open import L.Constructible {ℓ}
```

可构造层 `Lset α` 是传递的，且其构造对指数单调，故更大的指数给出更大的层。壳论证中反复用到的序数事实有：序数的成员是序数、`ω` 是序数、数码属于 `ω`、空集是序数。

```agda
  using ( 𝒮ʟ; isTransV; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ
        ; layer-trans; Lset-layer )
open import L.Ordinal {ℓ} using ( mem-ord; ω-ord; #∈ω; ∅-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈; rank-Lset )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
```

良序自带最小元选择器：从「存在某元素满足谓词」的截断陈述出发，它返回一个满足谓词且在良序下最小的元素。层隶属的秩刻画与限制到层载体的层序为该选择器供给输入，而并与单点的编码则构造后文使用的有限起始集合。

```agda
open import L.Rank {ℓ} using ( rank-fix )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; leastOf )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt )
open import L.Coding.CodeConstructibility {ℓ} using ( cup-out; cup-inl; cup-inr; sgl-out )
```

本章的环境是载体元素构成的向量，其运算逐分量进行：把函数映射到环境上、按索引查找、添入一个元素、以及拼接。第二分量为命题的对把元素与永不区分的证书一并记录。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( Vec; map; lookup; _∷_; []; _++_ )
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_; _,_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
```

空类型表示矛盾：`Empty.rec` 可把其元素消去到任意目标，而 `isProp⊥` 使目标为矛盾时可以消去命题截断。存在公式的满足以及呈现集合中的隶属用命题截断表达，因而保留存在性而不选定见证。

```agda
import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

累积层级用索引类型与赋值呈现集合。壳以有限树类型 `Code` 为索引类型；公式是见证码中的字段，并不自身充当码。构造部分供给空集、并、无序对与单点集构造，以及无穷序数及其后继。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; _∪_; ⁅_,_⁆; ⁅_⁆s; union-ax; pairing-ax; module InfinitySet
        ; SetPackage; SingletonPackage )  -- lint-agda: keep (SetPackage via record projection)
open InfinitySet using ( ω; sucV )
```

小隶属关系 `_∈ₛ_` 及其与外围隶属 `_∈ˢ_` 之间的桥 `∈∈ₛ`，把一个集合的呈现读法与它在层级中的读法连接起来：呈现内部所记录的，恰是宇宙中成立的。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; extensionality )
```

打开外围结构后，无修饰的等号与隶属符号固定表示外围关系；下文的受限结构仍各有自己的语义解释。

```agda
open hPropStructure 𝒮ᵥ
```

`SemV` 给出下文实例化满足关系时使用的定长外围环境。对常元取自 `𝒮ʟ` 的公式，出现次数计数识别无常元情形；`erase` 随后把不可能出现的常元域换为空类型，而不改变满足关系。

```agda
module SemV = FOL.Semantics 𝒮ᵥ using ( _^_; module At )
open SemV using ( _^_ )
module CS = hPropStructure 𝒮ʟ using ( S )
module Cnt = FOL.Manipulation.ConstantOccurrences.ZeroOccurrences CS.S using ( erase; erase-inv )
```

在空常元域上，`Δ₀-small` 证明每个有界公式在每个环境中的真值都等价于低一层宇宙中的命题；要得到分离还需另行应用 `separateFromSmall`。项代数随之开始：它以一个结构、把其载体映入外围宇宙的映射，以及该载体上的良序为参数。

```agda
module D0 = Δ₀Small {ℓc = ℓ-suc ℓ} {K = ⊥* {ℓ-suc ℓ}} (λ b → Empty.rec* b)
  using ( Δ₀-small )
module TermAlgebra (𝒮 : ZFStructure (ℓ-suc ℓ))
                   (toSet : ZFStructure.S 𝒮 → V ℓ)
                   (wo : SWO (ZFStructure.S 𝒮))
```

其余参数是默认元素 `junk` 与以 `K` 为索引的基生成元族；只有后文的壳实例把 `K` 认同为起始集合的一个呈现。垃圾值只是簿记装置，下文的构造从不检视它。

```agda
                   (junk : ZFStructure.S 𝒮)
                   {K : Type ℓ} (emb : K → ZFStructure.S 𝒮) where
```

这里只隐藏参数结构中未加限定的 Agda 名 `_∈ˢ_`；满足关系 `_⊨₀_` 仍用 `𝒮` 解释原子隶属。为载体改名，则使本章对外围载体的指称保持无歧义。

```agda
  open ZFStructure 𝒮 hiding ( _∈ˢ_ ) renaming ( S to S𝒮 )
```

项代数的满足在平凡为空的常元域上陈述：被求值的公式恰是无常元符号构成的那些，即纯粹的隶属与相等语言，且满足取值于命题。本节的每条查询与闭合陈述都采用这一读法。

```agda
  private module Sem = FOL.Semantics 𝒮
  open Sem using () renaming ( _^_ to _^𝒮_ )
  module At0 = Sem.At (⊥* {ℓ}) Empty.rec* using ( _⊨_ )
  _⊨₀_ : {n : ℕ} → S𝒮 ^𝒮 n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
  _⊨₀_ = At0._⊨_
```

码构成基生成元上的有限树代数：基码指名一个生成元；见证码记录一个元数为 `suc k` 的查询连同 `k` 个参数码。由于 `Code` 是归纳类型，每个码都是有限树；`cs` 的分量是当前码的直接参数子码，每个子码都可再是基码或见证码。

```agda
  data Code : Type ℓ where
    base : K → Code
    wit  : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec Code k → Code
```

`Sat k ψ vs` 是「存在元素在任意参数向量 `vs` 处满足 `ψ`」的仅仅存在；闭合定理随后把 `vs` 特化为码的取值。可满足性被陈述为截断的存在：它断言见证存在，而不产出见证。

```agda
  Sat : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec S𝒮 k → Type (ℓ-suc ℓ)
  Sat k ψ vs = ∥ Σ[ a ∈ S𝒮 ] ⟨ (a ∷ vs) ⊨₀ ψ ⟩ ∥₁
```

有了这条截断存在，`search` 就参数 `wo` 所供给的特定严格良序返回一个最小的满足元素。「最小」指该良序下的最小；它既不是关于隶属的极小，也不是秩的比较。

```agda
  search : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
         → Sat k ψ vs → S𝒮
  search k ψ vs w = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vs) ⊨₀ ψ) w .fst
```

码向量逐分量求值，与单个码的求值相互定义：见证码的参数取值即其分量码的取值。

```agda
  mutual
    vals : {m : ℕ} → Vec Code m → Vec S𝒮 m
    vals [] = []
    vals (c ∷ cs') = val c ∷ vals cs'
```

可满足的见证码求值为最小的满足元素；不可满足的见证码求值为 `junk`。由于每个码都向像贡献一个值，`junk` 可能出现在壳中；而 `val-wit` 表明，一旦给出可满足性，`junk` 便无关紧要。

```agda
    val : Code → S𝒮
    val (base m) = emb m
    val (wit k ψ cs) = Sum.rec (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))
```

这条小引理记录：一旦命题目标已知有元素，经典判定如何被使用。若判定落在左支，命题性把其中的元素与 `x` 认同，故消去式等于 `f x`；若落在右支，其中的否定与 `x` 矛盾，因此该情形不可能。

```agda
  sum-stuck : {X : Type (ℓ-suc ℓ)} (x : X) (px : isProp X)
            → (f : X → S𝒮) (g : (X → Empty.⊥) → S𝒮) (s : X ⊎ (X → Empty.⊥))
            → Sum.rec f g s ≡ f x
  sum-stuck x px f g (Sum.inl x') = sym (cong f (px x x'))
  sum-stuck x px f g (Sum.inr h)  = Empty.rec (h x)
```

给定见证码所存查询的可满足性见证，这条引理即可确认：该码的取值就是搜索的最小满足元素；垃圾分支被反驳，有见证的分支运行搜索。

```agda
  val-wit : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
          → (w : Sat k ψ (vals cs)) → val (wit k ψ cs) ≡ search k ψ (vals cs) w
  val-wit k ψ cs w = sum-stuck w squash₁ (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))
```

码向量的求值等同于对其映射求值，由简单递归证明。这使得后文的陈述可以在环境的递归形式与映射形式之间自由通行。

```agda
  vals≡map : {m : ℕ} (cs : Vec Code m) → vals cs ≡ map val cs
  vals≡map [] = refl
  vals≡map (c ∷ cs') = cong₂ _∷_ refl (vals≡map cs')
```

壳的呈现与层级呈现集合的方式相同：一个码族加一个赋值。它是全部码取值的像；由于不同码可能求值相同，呈现可以重复元素。因此壳中的隶属只是「存在某个码」的截断陈述，本章不主张壳传递，也不主张它是最小的闭合集合。

```agda
  Hull : V ℓ
  Hull = sett Code (λ c → toSet (val c))
```

呈现中的隶属是直接的：任何码的取值都是壳的成员，其见证正是该码本身。

```agda
  inHull : (c : Code) → ⟨ toSet (val c) ∈ˢ Hull ⟩
  inHull c = ∣ c , refl ∣₁
```

于是每条可满足的编码查询都在壳中有满足的见证。该定理断言的正是这条闭合性质；它并不把壳的全部成员都刻画为成功的最小见证。

```agda
  closed : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
         → Sat k ψ (vals cs)
         → ∥ Σ[ a ∈ S𝒮 ]
              (⟨ toSet a ∈ˢ Hull ⟩ × ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩) ∥₁
  closed k ψ cs w = ∣ a , a∈H , sat ∣₁
```

见证无需另寻：它就是项代数已赋予的取值，即搜索返回的最小满足元素。

```agda
    where
    a : S𝒮
    a = search k ψ (vals cs) w
```

选择器返回 `a` 以及 `IsLeast` 的两个分量：`a` 满足查询的证明，和不存在严格更小的满足元素的证明；本行投影前一分量。

```agda
    pa : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
    pa = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vals cs) ⊨₀ ψ) w .snd .fst
```

见证属于壳，来自专为该查询构造的见证码：其取值经 `val-wit` 被认同为搜索结果，而每个码的取值都在壳中。

```agda
    a∈H : ⟨ toSet a ∈ˢ Hull ⟩
    a∈H = subst (λ z → ⟨ toSet z ∈ˢ Hull ⟩) (val-wit k ψ cs w)
            (inHull (wit k ψ cs))
```

满足即被记录的分量，闭合子句就此完成。

```agda
    sat : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
    sat = pa
```

## 沿载体映射搬运满足关系

壳已建成并闭合，本章转向第二个任务，即在结构之间搬运满足关系；移送模块就外围载体上的两个谓词陈述。

```agda
module SatTransfer (MA MB : S → hProp (ℓ-suc ℓ)) where
```

源载体把外围载体的每个元素与「它满足第一个谓词」的证明配对；其公式只在这种对上读取。

```agda
  SA : Type (ℓ-suc ℓ)
  SA = Σ[ x ∈ S ] ⟨ MA x ⟩
```

目标载体是第二个谓词上的同一构造；那里的满足是对同一公式的目标读法。

```agda
  SB : Type (ℓ-suc ℓ)
  SB = Σ[ x ∈ S ] ⟨ MB x ⟩
```

源结构在配对载体上读取公式：项词典把变元解释为配对中的元素，满足取值于命题。

```agda
  module SemA = FOL.Semantics (𝒮ᵥ ↾ MA)
    using ( module At )
  module SemB = FOL.Semantics (𝒮ᵥ ↾ MB)
    using ( module At )
  open SemA.At SA id renaming ( _⊨_ to _⊨ᴬ_ ; ⟦_⟧ to ⟦_⟧ᴬ )
```

目标结构在另一侧做同样的事，拥有自己的满足与自己的项词典。

```agda
  open SemB.At SB id renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```

移送由两条原理组织。一致性对每条公式与每个环境陈述命题的相等：左侧的满足等于映射环境上映射公式的满足。接下来陈述的见证原理支撑存在量词的反向：目标侧存在式为真时，只须仅仅给出某个 `q : SA`，使其像满足矩阵。

```agda
  Agree : (SA → SB) → Type (ℓ-suc (ℓ-suc ℓ))
  Agree g = (n : ℕ) (φ : Formula SA n) (δ : SA ^ n)
          → (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
  Witness : (SA → SB) → Type (ℓ-suc ℓ)
  Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : SA ^ n)
```

它不要求该 `q` 是某个既定目标见证的原像；该原理只主张存在某个内部点的像满足矩阵的截断陈述，而这恰是存在量词反向所消耗的形式。

```agda
            → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ φ) ⟩
            → ∥ Σ[ q ∈ SA ] ⟨ (g q ∷ map g δ) ⊨ᴮ mapFo g φ ⟩ ∥₁
```

移送模块收取映射连同原子假设：原子隶属与相等必须沿 `g` 双向一致，如此归纳中的原子隶属与相等才能成为命题的路径。

```agda
  module Along (g : SA → SB)
    (at∈ : (n : ℕ) (t u : Term SA n) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ∈̇ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ∈̇ u)))
    (at≐ : (n : ℕ) (t u : Term SA n) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ≐ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ≐ u)))
```

见证原理是第三条假设，移送的数据就此齐备。

```agda
    (wit : Witness g) where
```

第一条弱化事实在源结构中陈述。沿 `suc` 改名把每个旧变元移过环境中新添的首槽，故在 `x ∷ δ` 处求值还原为在 `δ` 处求值；常元不受影响。

```agda
    private
      renA : {n : ℕ} (t : Term SA n) (x : SA) (δ : SA ^ n)
           → ⟦ renameTm suc t ⟧ᴬ (x ∷ δ) ≡ ⟦ t ⟧ᴬ δ
      renA (con c) x δ = refl
      renA (var i) x δ = refl
```

同样的弱化在目标结构中也成立；下一条陈述开始比较映射与弱化。

```agda
      renB : {n : ℕ} (t : Term SB n) (x : SB) (δ : SB ^ n)
           → ⟦ renameTm suc t ⟧ᴮ (x ∷ δ) ≡ ⟦ t ⟧ᴮ δ
      renB (con c) x δ = refl
      renB (var i) x δ = refl
      mapTm-ren : {n : ℕ} (t : Term SA n)
```

映射与弱化在项上交换，这是定义性的：弱化项的映射逐个弱化被改名的分量。

```agda
                → mapTm g (renameTm suc t) ≡ renameTm suc (mapTm g t)
      mapTm-ren (con c) = refl
      mapTm-ren (var i) = refl
```

被映射的弱化项在任意目标点 `x` 接映射环境处求值，与被映射项在映射环境处的值相同。

```agda
      renG : {n : ℕ} (t : Term SA n) (x : SB) (δ : SA ^ n)
           → ⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ) ≡ ⟦ mapTm g t ⟧ᴮ (map g δ)
      renG t x δ = cong (λ u → ⟦ u ⟧ᴮ (x ∷ map g δ)) (mapTm-ren t)
                 ∙ renB (mapTm g t) x (map g δ)
```

对项的隶属不受弱化影响，其形式恰为有界子句所消耗者；下一条引理陈述边条件的转移本身。

```agda
      memRen : {n : ℕ} (t : Term SA n) (x : SB) (δ : SA ^ n)
             → (fst x ∈ˢ fst (⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ)))
             ≡ (fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memRen t x δ = cong (λ s → fst x ∈ˢ fst s) (renG t x δ)
      memPath : {n : ℕ} (t : Term SA n) (q : SA) (δ : SA ^ n)
```

有界量词的边条件跨越映射转移。链条先在源结构中弱化，再在移位环境处应用原子的隶属假设。

```agda
              → (fst q ∈ˢ fst (⟦ t ⟧ᴬ δ))
              ≡ (fst (g q) ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memPath {n} t q δ =
        cong (λ s → fst q ∈ˢ fst s) (sym (renA t q δ))
        ∙ at∈ (suc n) (var zero) (renameTm suc t) (q ∷ δ)
```

链条以目标结构中的弱化结束。有了它，任何有界子句的边条件都可在映射两侧读取。

```agda
        ∙ memRen t (g q) δ
```

经典步骤被打包一次：对命题而言，双否消去由排中律而来。全称子句的正向先假设目标侧存在反例，把它包装成否定矩阵的存在见证，再用 `Witness` 拉回内部反例并推出矛盾；最后由 `dne` 得到所需的目标侧真值。

```agda
      dne : (P : hProp (ℓ-suc ℓ)) → (((⟨ P ⟩) → Empty.⊥) → Empty.⊥) → ⟨ P ⟩
      dne P h = Sum.rec (λ p → p)
        (λ (np : ⟨ P ⟩ → Empty.⊥) → Empty.rec (h np)) (lem P)
```

归纳现在沿十条子句运行，而它恰从假设所在处开始：两条原子子句正是 `at∈` 与 `at≐`。命题联结词逐分量搬运，因为命题上的合取、析取与蕴含都由其分量决定。

```agda
    agree : Agree g
    agree n (t ∈̇ u) δ = at∈ n t u δ
    agree n (t ≐ u) δ = at≐ n t u δ
    agree n (φ ∧̇ ψ) δ = cong₂ _⊓_ (agree n φ δ) (agree n ψ δ)
    agree n (φ ∨̇ ψ) δ = cong₂ _⊔_ (agree n φ δ) (agree n ψ δ)
```

蕴含同样逐分量搬运，假值恒定，而存在子句以一个双条件开场。其正向陈述：内部对存在式的满足映射为「映射环境上映射存在式」的满足。

```agda
    agree n (φ ⇒̇ ψ) δ = cong₂ _⇒_ (agree n φ δ) (agree n ψ δ)
    agree n ⊥̇ δ = refl
    agree n (∃̇ ψ) δ = ⇔toPath fwd bwd
      where
      fwd : ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩ → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩
```

正向消去内部见证的截断并把见证映射过去；反向正是见证原理发挥作用之处：把外部满足交给见证原理，它返回一个内部点，其像满足矩阵，再由一致把该满足搬回。

```agda
      fwd = PT.rec (snd (map g δ ⊨ᴮ mapFo g (∃̇ ψ)))
        (λ { (q , hq) → ∣ g q , subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hq ∣₁ })
      bwd : ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩ → ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩
      bwd h = PT.map (λ { (q , hq) →
        q , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) hq }) (wit n ψ δ h)
```

全称子句是经典的一支：其正向假设每个内部点都满足矩阵，固定外部点 `x`，并须证明 `x` 在像中满足矩阵。证明从双否消去开始，这正是排中律进入移送之处。

```agda
    agree n (∀̇ ψ) δ = ⇔toPath fwd bwd
      where
      fwd : ((q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x = dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
```

若 `x` 失败，映射环境就会在 `x` 处满足否定矩阵；对该否定施加见证原理，返回一个内部点，其像满足否定，而该内部点处的一致便反驳「每个内部点都满足矩阵」的假设。

```agda
        PT.rec isProp⊥ (λ { (q , hq) →
          lower (hq (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) (h q))) })
          (wit n (¬̇ ψ) δ ∣ x , (λ yes → lift (nx yes)) ∣₁)
      bwd : ((x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
```

反向是直接的，因为每个内部点都映入外部载体。有界全称随之以一条辅助公式开场：它把边条件，即属于改名后的界，与矩阵的否定合取；辅助公式的满足正是「在界内但矩阵不成立」的经典读法。

```agda
      bwd h q = subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (h (g q))
    agree n (∀̇∈ t ψ) δ = ⇔toPath fwd bwd
      where
      mat : Formula SA (suc n)
      mat = (var zero ∈̇ renameTm suc t) ∧̇ ¬̇ ψ
```

正向陈述：若界内的每个内部点都满足矩阵，则每个属于映射后界的外部点都满足映射后的矩阵。证明再次从双否消去开始：假设该外部点失败。

```agda
      fwd : ((q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
          → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x hx =
        dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
```

见证原理被施加于辅助公式，返回内部点 `q`：其像落在界内却反驳矩阵。像在界内的隶属经弱化与 `memPath` 搬回，一致再把内部对矩阵的满足提升到其像处，与失败相矛盾。

```agda
        PT.rec isProp⊥ (λ { (q , hq) →
          lower (hq .snd (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ))
            (h q (subst ⟨_⟩ (sym (memPath t q δ))
                    (subst ⟨_⟩ (memRen t (g q) δ) (hq .fst)))))) })
          (wit n mat δ ∣ x , (subst ⟨_⟩ (sym (memRen t x δ)) hx
```

辅助应用以见证记录收尾，其第二分量是矩阵在像处的失败，即否定矩阵。反向陈述：像处的外部满足加上内部边条件，即得内部对矩阵的满足。

```agda
            , (λ yes → lift (nx yes))) ∣₁)
      bwd : ((x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                   → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
      bwd h q hq =
```

反向在内点的像处施加外部满足，边条件经 `memPath`、矩阵经一致搬运。有界存在随之以其辅助矩阵开场：它合取边条件与矩阵本身。

```agda
        subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ)))
          (h (g q) (subst ⟨_⟩ (memPath t q δ) hq))
    agree n (∃̇∈ t ψ) δ = ⇔toPath fwd bwd
      where
      mat : Formula SA (suc n)
```

辅助矩阵即边条件与矩阵的合取；正向陈述：内部见证对映射为外部见证对。证明只是对截断的一次映射。

```agda
      mat = (var zero ∈̇ renameTm suc t) ∧̇ ψ
      fwd : ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
          → ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
      fwd = PT.map (λ { (q , hq , hψ) →
```

两个分量分别搬运：边条件经 `memPath`，矩阵经一致。反向陈述其逆：外部见证对给出内部见证对。

```agda
        g q , (subst ⟨_⟩ (memPath t q δ) hq ,
               subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hψ) })
      bwd : ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
          → ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
```

反向对以辅助形式读取的外部对运行见证原理，得到内点及其像处的对；两个分量再分别经弱化与 `memPath`、经一致搬回。

```agda
      bwd h = PT.map (λ { (q , hq) →
        q , ( subst ⟨_⟩ (sym (memPath t q δ))
                (subst ⟨_⟩ (memRen t (g q) δ) (hq .fst))
            , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (hq .snd)) })
        (wit n mat δ (PT.map (λ { (x , hx , hψ) →
```

两个分量闭合有界存在的移送，十条子句的归纳随之完成。

```agda
          x , (subst ⟨_⟩ (sym (memRen t x δ)) hx , hψ) }) h))
```

## 层内部的 Tarski-Vaught 判据

对序数指数 `α`，层 `Lset α` 给出外围结构，上述移送将在其中证明初等性。

```agda
module AtStage (α : S) (ordα : IsOrd α) where
```

层是传递的，理由很精确：`Lset-layer α` 证明 `α` 处的层传递，`layer-trans` 由此给出 `Lset α` 的传递性。序数性假设在此并未使用，而是留给下文的良序。

```agda
  Ltr : isTransV (Lset α)
  Ltr = layer-trans (Lset-layer α)
```

传递性保证有界公式在 `Lset α` 内部与全集中绝对一致。因此，层上的受限结构可作为 Tarski-Vaught 论证的外部语义。

```agda
  module AbsL = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ Lset α) Ltr
    using ( SM; 𝒮M; _⊨ᵐ_; ⟦_⟧ᵐ; abs₀ )
```

层载体是属于 `Lset α` 的元素的类型；下文的每个壳成员与每次层读取都居于该类型。

```agda
  SL : Type (ℓ-suc ℓ)
  SL = AbsL.SM
```

前一章的层序限制为该载体上的良序。固定一个包含于该层的载体 `M`；它到该层的包含是所取假设的一部分。

```agda
  wL : SWO SL
  wL = orderAt α ordα
  module AtM (M : S) (M⊆L : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ x ∈ˢ Lset α ⟩) where
```

子结构的载体是外围载体中的元素连同其属于 `M` 的证明；公式只在这种对上读取。

```agda
    SM : Type (ℓ-suc ℓ)
    SM = Σ[ x ∈ S ] ⟨ x ∈ˢ M ⟩
```

子结构的语义是外围语义在 `M` 上的限制：项在限制内部求值，满足取值于命题。

```agda
    module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
      using ( module At )
    open SemM.At SM id renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

到层的包含把载体的每个元素与其层隶属配对，后者由包含假设供给。

```agda
    inL : SM → SL
    inL c = fst c , M⊆L (fst c) (snd c)
```

初等性陈述：对该载体的每条公式与每个环境，满足在包含下不变。它是命题间的路径，两条原子同余与见证原理正是以这种形式与它复合。

```agda
    Elementary : Type (ℓ-suc (ℓ-suc ℓ))
    Elementary = (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
               → (δ ⊨ᵐ φ) ≡ (map inL δ AbsL.⊨ᵐ (mapFo inL φ))
```

Tarski-Vaught 判据是初等性的见证形式：每当层在某个环境的像处满足一个存在式，就有载体的某个元素，其像在该处满足矩阵。由满足的命题值性，仅仅存在即可。

```agda
    TarskiVaught : Type (ℓ-suc ℓ)
    TarskiVaught = (n : ℕ) (φ : Formula SM (suc n)) (δ : SM ^ n)
                 → ⟨ map inL δ AbsL.⊨ᵐ (mapFo inL (∃̇ φ)) ⟩
                 → ∥ Σ[ q ∈ SM ] ⟨ (inL q ∷ map inL δ) AbsL.⊨ᵐ (mapFo inL φ) ⟩ ∥₁
```

逐点包含与环境查找可交换；这正是项的一致性所需的变元情形。

```agda
    private
      lookup-inL : {n : ℕ} (i : Fin n) (δ : SM ^ n)
                 → lookup i (map inL δ) ≡ inL (lookup i δ)
      lookup-inL zero (c ∷ δ) = refl
      lookup-inL (suc i) (c ∷ δ) = lookup-inL i δ
```

项在包含两侧一致：载体的项无论在子结构中读取，还是映射后在层中读取，都求得同一底层元素。常元固定，变元随查找而定。移送机制随即在两个隶属谓词处实例化。

```agda
      tm-agree : (n : ℕ) (t : Term SM n) (δ : SM ^ n)
               → fst (⟦ t ⟧ᵐ δ) ≡ fst (AbsL.⟦ mapTm inL t ⟧ᵐ (map inL δ))
      tm-agree n (con c) δ = refl
      tm-agree n (var i) δ = sym (cong fst (lookup-inL i δ))
    module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ Lset α)
```

初等性由共享归纳实例化而来：两个原子情形由刚证得的满足关系合同性给出，见证原理恰是 Tarski-Vaught 实例，而布尔与量词子句由共享主体搬运。除这两条同余与该判据外，不使用任何关于层的特殊性质。

```agda
    TV→elem : TarskiVaught → Elementary
    TV→elem tv = Tr.Along.agree inL
      (λ n t u δ → cong₂ _∈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
      (λ n t u δ → cong₂ _≈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
      tv
```

## 对最小见证闭合起始集合

假设起始集 `X` 包含于该层，并假设指数 `α` 包含空集。空集属于 `Lset α`，因为 `∅` 位于序数 `α` 中，且在基层有编码。

```agda
  module Hull (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
               (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
    ∅∈Lsetα : ⟨ ∅ ∈ˢ Lset α ⟩
    ∅∈Lsetα = Lset-in α ∅ ∅ ∅∈α (∅∈𝒟ₒ ∅)
```

起始集合呈现的嵌入落入层载体：每个索引指名 `X` 的一个成员，包含假设证明该成员属于层 `Lset α`。

```agda
    inStg : ⟪ X ⟫ → SL
    inStg m = ⟪ X ⟫↪ m , X⊆L (⟪ X ⟫↪ m) (member X m)
```

项代数在层的受限结构处实例化：其载体经第一投影映入宇宙，见证搜索使用层的良序，垃圾值取空集，基码以 `X` 的呈现为索引。壳就此在层内生长。

```agda
    module T = TermAlgebra AbsL.𝒮M fst wL (∅ , ∅∈Lsetα) {K = ⟪ X ⟫} inStg
    open T using ( Code; base; val; Hull; inHull )
```

壳位于层内：每个成员都是某个码的取值，而码的取值依项代数自身的类型都属于层 `Lset α`。证明消去截断的呈现，并沿该同一视搬运。

```agda
    Hull⊆L : (x : S) → ⟨ x ∈ˢ Hull ⟩ → ⟨ x ∈ˢ Lset α ⟩
    Hull⊆L x x∈H = PT.rec (snd (x ∈ˢ Lset α)) go x∈H
      where
      go : Σ[ c ∈ Code ] (fst (val c) ≡ x) → ⟨ x ∈ˢ Lset α ⟩
      go (c , q) = subst (λ z → ⟨ z ∈ˢ Lset α ⟩) q (snd (val c))
```

隶属只能读回为截断的存在：壳的成员是某个码的取值，但没有选定哪个码。这是呈现的诚实形式，因为不同码可能求值相同。

```agda
    hull-member : (x : S) → ⟨ x ∈ˢ Hull ⟩
                → ∥ Σ[ c ∈ Code ] (fst (val c) ≡ x) ∥₁
    hull-member x x∈H = x∈H
```

另一方向无需截断：由呈现自身的引入规则，每个码的取值都是成员。

```agda
    val-in-Hull : (c : Code) → ⟨ fst (val c) ∈ˢ Hull ⟩
    val-in-Hull c = inHull c
```

起始集合逐成员进入壳。`X` 的成员 `x` 由一个索引呈现，呈现它在 `x` 处的纤维返回该索引。

```agda
    module XInM (x : S) (x∈X : ⟨ x ∈ˢ X ⟩) where
      mx : ⟪ X ⟫
      mx = fiber X x∈X .fst
```

纤维携带被呈现元素与 `x` 的同一视，这正是沿之搬运隶属的通道。

```agda
      x≡val : ⟪ X ⟫↪ mx ≡ x
      x≡val = fiber X x∈X .snd
```

该索引处的基码求值为被呈现元素，即 `x`；搬运把 `x` 在壳中的隶属落定。

```agda
      inM : ⟨ x ∈ˢ Hull ⟩
      inM = subst (λ z → ⟨ z ∈ˢ Hull ⟩) x≡val (inHull (base mx))
```

组装一次后，起始集合含于壳即成单条引理。

```agda
    X⊆M : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Hull ⟩
    X⊆M x x∈X = XInM.inM x x∈X
```

## 满足关系在塌缩同构下不变

为比较同构前后的满足关系，固定集合 `M`、`PM`，以及把 `M` 的成员映到 `PM` 的成员的载体映射 `p`。

```agda
module IsoInv (M : S) (PM : S)
  (p : S → S)
  (p∈ : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ p x ∈ˢ PM ⟩)
```

除封闭条件 `p∈` 外，映射 `p` 还满足四条假设。`iso-fwd` 保持隶属，`iso-bwd` 反映隶属，最后两个参数陈述 `M` 上的单射性与到目标 `PM` 上的满射性。

```agda
  (iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
           → ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩)
  (iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
           → ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩)
  (p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
```

映射 `p` 在 `M` 上单射，且仅仅地满射到 `PM`。与保持、反映合在一起，这恰是两个结构之间隶属同构的全部数据。

```agda
          → p x ≡ p y → x ≡ y)
  (surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
        → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (p y ≡ z)) ∥₁)
  where
```

源载体把 `M` 的每个元素与其隶属证明配对，与本章各受限结构相同。

```agda
  SM : Type (ℓ-suc ℓ)
  SM = Σ[ x ∈ S ] ⟨ x ∈ˢ M ⟩
```

目标载体把 `PM` 的每个元素与其隶属证明配对。

```agda
  SPM : Type (ℓ-suc ℓ)
  SPM = Σ[ x ∈ S ] ⟨ x ∈ˢ PM ⟩
```

同构提升到配对载体：对底层元素施加 `p`，并证明其在像中的隶属。

```agda
  g : SM → SPM
  g m = p (fst m) , p∈ (fst m) (snd m)
```

源语义在限制于 `M` 的结构中解释项与公式。

```agda
  module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
    using ( module At )
  module SemPM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ PM))
    using ( module At )
  open module Mse = SemM.At SM id public renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

目标语义在限制于 `PM` 的结构中解释映射后的项与公式。

```agda
  open module Pse = SemPM.At SPM id public renaming ( _⊨_ to _⊨ᵖᵐ_ ; ⟦_⟧ to ⟦_⟧ᵖᵐ )
```

满射提升到配对载体：目标 `PM` 的每个元素都是 `M` 中某点的像，而底层元素的相等因属于 `PM` 是命题而提升为对的相等。

```agda
  surj' : (p' : SPM) → ∥ Σ[ q ∈ SM ] (g q ≡ p') ∥₁
  surj' (z , z∈) = PT.map (λ { (y , y∈ , e) →
    (y , y∈) , Σ≡Prop (λ w → (w ∈ˢ PM) .snd) e }) (surj z z∈)
```

一般的满足关系移送定理现可施用于属于 `M` 与属于 `PM` 的谓词；隶属的保持与反映给出其隶属原子情形。

```agda
  module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ PM)
```

映射 `p` 逐索引地作用于环境，因此查找一次一格化归。

```agda
  private
    lookup-g : {n : ℕ} (i : Fin n) (δ : SM ^ n)
             → p (fst (lookup i δ)) ≡ fst (lookup i (map g δ))
    lookup-g zero (m ∷ δ) = refl
    lookup-g (suc i) (m ∷ δ) = lookup-g i δ
```

项在映射 `p` 下相一致：对 `M` 的项的值施加 `p`，等于在映射环境处求值映射后的项。常元固定，变元随查找而定。隶属原子由此可陈述。

```agda
    tm-agree : {n : ℕ} (t : Term SM n) (δ : SM ^ n)
             → p (fst (⟦ t ⟧ᵐ δ)) ≡ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ))
    tm-agree (con m) δ = refl
    tm-agree (var i) δ = lookup-g i δ
    at∈ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
```

原子项的隶属双向转移：正向把内部隶属沿项等式搬运，再施加保持隶属的 `iso-fwd`。

```agda
        → (δ ⊨ᵐ (t ∈̇ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ∈̇ u))
    at∈ n t u δ = ⇔toPath
      (λ h → subst (λ z → ⟨ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ∈ˢ z ⟩) (tm-agree u δ)
        (subst (λ z → ⟨ z ∈ˢ p (fst (⟦ u ⟧ᵐ δ)) ⟩) (tm-agree t δ)
          (iso-fwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
```

正向搬运落在施加 `p` 后的隶属上；反向经由同构反映该隶属，沿项等式恢复内部的隶属。

```agda
            (snd (⟦ t ⟧ᵐ δ)) h)))
      (λ h → iso-bwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
        (snd (⟦ t ⟧ᵐ δ))
        (subst (λ z → ⟨ p (fst (⟦ t ⟧ᵐ δ)) ∈ˢ z ⟩) (sym (tm-agree u δ))
          (subst (λ z → ⟨ z ∈ˢ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) ⟩)
```

反向闭合隶属子句：经同构、循项同余的反映，恰好返回内部的隶属。相等原子与见证原理由其余假设处理。

```agda
            (sym (tm-agree t δ)) h)))
```

原子项的等式通过把塌缩施加于等式两侧而转移。正向取 `M` 中值的等式，经 `cong` 施加 `p`，再由项同约把两侧分别搬运到映射后的项。

```agda
    at≐ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ (t ≐ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ≐ u))
    at≐ n t u δ = ⇔toPath
      (λ h → subst (λ z → z ≡ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ))) (tm-agree t δ)
        (subst (λ z → p (fst (⟦ t ⟧ᵐ δ)) ≡ z) (tm-agree u δ) (cong p h)))
```

反向正是单射性发挥作用之处：塌缩后的两侧相等，`p-inj` 由此恢复原值的相等。两个方向合起来，把相等原子变成命题之间的路径。

```agda
      (λ h → p-inj (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ)) (snd (⟦ t ⟧ᵐ δ))
        (snd (⟦ u ⟧ᵐ δ))
        (subst (λ z → z ≡ p (fst (⟦ u ⟧ᵐ δ))) (sym (tm-agree t δ))
          (subst (λ z → fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ≡ z)
            (sym (tm-agree u δ)) h)))
```

见证原理由满射产出。像中的外部见证 `p'` 仅仅是 `M` 中某个 `q` 的塌缩；沿该同一视搬运满足，即得内部见证及其在像中的满足。

```agda
    wit : Tr.Witness g
    wit n ψ δ h = PT.rec squash₁
      (λ { (p' , hp) → PT.map
        (λ { (q , gq≡p) →
          q , subst (λ z → ⟨ (z ∷ map g δ) ⊨ᵖᵐ mapFo g ψ ⟩) (sym gq≡p) hp })
```

满射引理供给原像，两次搬运复合成移送的见证原理。

```agda
        (surj' p') }) h
```

原子情形与见证原理就位后，共享归纳证明：环境沿塌缩映射、常元沿 `g` 重标记时，满足关系保持不变。

```agda
  agree : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ φ) ≡ (map g δ ⊨ᵖᵐ mapFo g φ)
  agree = Tr.Along.agree g at∈ at≐ wit
```

一致性以两个单向形式记录备用。正向：内部的满足给出映射环境上映射公式的满足。

```agda
  iso-inv : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
          → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩
  iso-inv n φ δ = subst ⟨_⟩ (agree n φ δ)
```

反向把外部的满足送回内部的满足。随后本章在有外延性的集合 `X` 的塌缩处实例化这一不变性，打开塌缩及其隶属同构与单射性。

```agda
  iso-inv-bwd : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
              → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
  iso-inv-bwd n φ δ = subst ⟨_⟩ (sym (agree n φ δ))
module CollapseIso (X : S) (Xext : isExt X) where
  module C = Collapse X using ( module InjExt; π; πX; πX-intro; πX-member )
```

`X` 的外延性正是塌缩所需：限制后的结构单射，且 `X` 上隶属与塌缩像上隶属之间的同构随即可用。

```agda
  module CI = C.InjExt Xext using ( iso; π-inj )
```

目标载体是塌缩像 `πX`；它的点恰是 `X` 的成员之塌缩值。

```agda
  PM : S
  PM = C.πX
```

映射 `p` 把每个集合送到其 Mostowski 塌缩值。

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

`X` 的成员落入像中，这由塌缩对像自身的引入规则给出。

```agda
  p∈ : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ p x ∈ˢ PM ⟩
  p∈ = C.πX-intro
```

隶属沿塌缩正向保持：若在 `X` 中 `y` 属于 `x`，则 `y` 的塌缩属于 `x` 的塌缩。这是隶属同构的第一个分量。

```agda
  iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
          → ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩
  iso-fwd x y x∈ y∈ = CI.iso x y x∈ y∈ .fst
```

隶属也反向反映：塌缩后的隶属只能来自 `X` 中真实的隶属。两个方向合起来说明塌缩对隶属是忠实的。

```agda
  iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
          → ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩
  iso-bwd x y x∈ y∈ = CI.iso x y x∈ y∈ .snd
```

塌缩在 `X` 上单射：塌缩相等的两个成员相等。对隶属的忠实加上单射性，构成元素层面同构的两半。

```agda
  p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
        → p x ≡ p y → x ≡ y
  p-inj = CI.π-inj
```

像的每点都来自 `X` 的成员：满射是截断的，只主张原像存在而不选定它，这正是见证原理所消耗的形式。

```agda
  surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
       → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (p y ≡ z)) ∥₁
  surj = C.πX-member
```

对外延集合 `X`，塌缩保持并反映隶属，在 `X` 上单射，且覆盖 `πX` 的每个点。

```agda
  module I = IsoInv X PM p p∈ iso-fwd iso-bwd p-inj surj
    using ( SM; SPM; g; surj'; iso-inv; iso-inv-bwd; _⊨ᵐ_; _⊨ᵖᵐ_; ⟦_⟧ᵐ; ⟦_⟧ᵖᵐ )
```

## Skolem 壳是初等的

因此，满足关系可在 `X` 上的结构与 `πX` 上的结构之间双向搬运。

```agda
module HullElemDown (α : S) (ordα : IsOrd α)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩) (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
```

把这一点用于 `Lset α` 内的 Skolem 壳，初等性便归结为 Tarski-Vaught 见证条件。

```agda
  module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
  module H = ASt.Hull X X⊆L ∅∈α
    using ( module T; Hull⊆L; hull-member )
  M : S
  M = H.T.Hull
```

子结构机制在壳处实例化，其公式获得一个外围读法。壳载体的每个元素都有码：码由截断的呈现给出存在，而「取值等于包含」的同一视借层隶属的命题值性提升。

```agda
  module A = ASt.AtM M H.Hull⊆L using ( Elementary; SM; module SemM; TV→elem; inL )
  module Mse = A.SemM.At A.SM id using ( _⊨_ )
  codeOf : (q : A.SM) → ∥ Σ[ c ∈ H.T.Code ] (H.T.val c ≡ A.inL q) ∥₁
  codeOf q = PT.map (λ { (c , e) → c , Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) e })
    (H.hull-member (fst q) (snd q))
```

码从单个元素提升到有限环境：空环境由空向量编码，递归情形把一个新码与已建好的码并列。

```agda
  codeEnv : {n : ℕ} (δ : Vec A.SM n)
          → ∥ Σ[ ds ∈ Vec H.T.Code n ]
               (map H.T.val ds ≡ map A.inL δ) ∥₁
  codeEnv [] = ∣ [] , refl ∣₁
  codeEnv (q ∷ δ) = PT.map2
```

添入情形把两个截断存在复合成一个：加长后的码向量求值恰为包含后的环境。

```agda
    (λ { (c , ec) (ds , eds) → c ∷ ds , cong₂ _∷_ ec eds })
    (codeOf q) (codeEnv δ)
```

逐分量映射还保持有限环境的拼接。因此，自由变元的取值与替代常元出现的取值可以合并为一个供 Tarski-Vaught 论证使用的编码环境。

```agda
  inL-++ : {n m : ℕ} (δ : Vec A.SM n) (σ : Vec A.SM m)
          → map A.inL (δ ++ σ) ≡ map A.inL δ ++ map A.inL σ
  inL-++ [] σ = refl
  inL-++ (q ∷ δ) σ = cong (A.inL q ∷_) (inL-++ δ σ)
  tv : (n : ℕ) (ψ : Formula A.SM (suc n)) (δ : Vec A.SM n)
```

该陈述即 Tarski-Vaught 条件本身：若层在包含后的环境处满足一个存在式，则仅仅地有壳中某元素在该处满足矩阵。证明先消去环境的编码，再进入搜索闭合。

```agda
     → ⟨ map A.inL δ ASt.AbsL.⊨ᵐ (mapFo A.inL (∃̇ ψ)) ⟩
     → ∥ Σ[ q ∈ A.SM ]
          ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩ ∥₁
  tv n ψ δ h = PT.rec squash₁ takeEnvironment (codeEnv params)
    where
```

参数抽象把每个常元出现替换为一个额外自由变元。所得公式的常元域为空，元数增加 `countFo ψ`，同时保留 `ψ` 的完整逻辑结构。

```agda
    bodyFo : Formula (⊥* {ℓ}) (suc (n + countFo ψ))
    bodyFo = absFo ψ
```

抽象后矩阵的环境是原环境后接诸常数出现：抽象把常数变成额外的自由变元，因此一个向量就携带搜索所需的一切。

```agda
    params : Vec A.SM (n + countFo ψ)
    params = δ ++ constantsFo ψ
```

一旦这个合并环境有了码，最小见证闭合便给出壳中的见证。再利用抽象公式与原带参公式之间的语义同一视，即得所需的 Tarski-Vaught 见证。

```agda
    takeEnvironment : Σ[ ds ∈ Vec H.T.Code (n + countFo ψ) ]
                        (map H.T.val ds ≡ map A.inL params)
                    → ∥ Σ[ q ∈ A.SM ]
                         ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
                             (mapFo A.inL ψ) ⟩ ∥₁
```

搜索闭合在编码环境处运行。其自身的求值记录随后与编码等式、以及包含对拼接的分配复合，得到「码的求值即包含后的参数」。

```agda
    takeEnvironment (ds , eds) = PT.map finish (H.T.closed _ bodyFo ds witness)
      where
      vals-env : H.T.vals ds
               ≡ map A.inL δ ++ map A.inL (constantsFo ψ)
      vals-env = H.T.vals≡map ds ∙ eds ∙ inL-++ δ (constantsFo ψ)
```

关键的同一视陈述：抽象矩阵在「编码环境处的裸搜索语义」下的读法，与它在「包含环境处的层语义」下的读法是同一命题。

```agda
      body-path : (b : ASt.SL)
                → ((b ∷ H.T.vals ds) H.T.⊨₀ bodyFo)
                ≡ ((b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ mapFo A.inL ψ)
      body-path b =
          cong (λ ε → ε H.T.⊨₀ bodyFo) (cong (b ∷_) vals-env)
```

这条路径复合两个语义相容律：`⊨-abs` 把参数抽象联系到扩展环境，`⊨-map` 把重标记联系到映射后的环境。

```agda
        ∙ sym (⊨-abs ASt.AbsL.𝒮M A.inL ψ
                 (b ∷ map A.inL δ))
        ∙ sym (⊨-map ASt.AbsL.𝒮M A.inL id ψ
                 (b ∷ map A.inL δ))
```

层对存在式的满足沿体路径搬运进裸读法，产出恰是搜索闭合所需的可满足性见证。

```agda
      witness : H.T.Sat (n + countFo ψ) bodyFo (H.T.vals ds)
      witness = PT.map (λ { (b , hb) →
        b , subst ⟨_⟩ (sym (body-path b)) hb }) h
```

搜索返回壳内满足抽象矩阵的最小见证，其在编码环境处成立。转换须把它变成原公式的 Tarski-Vaught 对。

```agda
      finish : Σ[ a ∈ ASt.SL ]
                 ( ⟨ fst a ∈ˢ M ⟩
                 × ⟨ (a ∷ H.T.vals ds) H.T.⊨₀ bodyFo ⟩ )
             → Σ[ q ∈ A.SM ]
                 ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
```

见证被读回子结构的载体：底层集合即壳，隶属即刚产出者。

```agda
      finish (a , a∈H , ha) = q , sat
        where
        q : A.SM
        q = fst a , a∈H
```

见证到层的包含就是见证本身：两个载体只差命题值性的隶属证明，而它由自反性等同。

```agda
        q≡a : A.inL q ≡ a
        q≡a = Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) refl
```

见证处本体的满足沿体路径搬入层语义，再沿见证的同一视搬入子结构载体；这恰是原公式与原环境的 Tarski-Vaught 结论。

```agda
        sat : ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
        sat = subst (λ b → ⟨ (b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
                                (mapFo A.inL ψ) ⟩)
                (sym q≡a) (subst ⟨_⟩ (body-path a) ha)
```

因此，Tarski-Vaught 条件给出壳在 `Lset α` 中的初等性。

```agda
  elem : A.Elementary
  elem = A.TV→elem tv
```

## 在外围宇宙中读取无参公式

对于常元域为空的公式，外围满足关系的比较不涉及任何非平凡的常元重标记。

```agda
module AtP = SemV.At (⊥* {ℓ-suc ℓ}) (λ b → Empty.rec* b) using ( _⊨_ )
```

无参公式的外围满足被命名备用；关键观察是：改名无参公式不改变它，因为无可重映射的常数。

```agda
_⊨ₚ_ : {n : ℕ} → S ^ n → Formula (⊥* {ℓ-suc ℓ}) n → hProp (ℓ-suc ℓ)
_⊨ₚ_ = AtP._⊨_
embed-map : {ℓ₁ ℓ₂ : Level} {K : Type ℓ₁} {K' : Type ℓ₂} (f : K → K')
            {n : ℕ} (φ : Formula (⊥* {ℓ-suc ℓ}) n)
          → mapFo f (embed φ) ≡ embed φ
```

证明复合映射法则与「空域嵌入在出现上是恒等」的事实：改名无可移动之物。

```agda
embed-map f φ =
    mapFo-comp Empty.rec* f φ
  ∙ cong (λ h → mapFo h φ) (funExt (λ b → Empty.rec* b))
opaque
  isOrdAt : Formula (⊥* {ℓ-suc ℓ}) 1
```

序数性由一个单空位有界公式表达：参数本身传递，且参数的每个成员也传递。

```agda
  isOrdAt =
    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
    ∧̇ (∀̇∈ (var zero) (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
```

`Δ₀` 证书先穿过外层合取，再分别穿过第一子句的两个与第二子句的三个有界量词，最终落到隶属原子。

```agda
  Δ₀-isOrdAt : Δ₀ isOrdAt
  Δ₀-isOrdAt =
    δ-∧ (δ-∀∈ (δ-∀∈ δ-∈))
        (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
```

两个读取引理在两个方向上把 `isOrdAt` 的满足精确等同于序数谓词。

```agda
module Amb where
  opaque
    unfolding isOrdAt
```

从公式读出序数性，即把两条有界子句拆成序数谓词的两个字段：参数的传递性，以及每个成员的传递性。

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

反过来，`IsOrd` 的两个字段满足这两个有界子句。三空位伴随公式在中间的自由空位表达同一谓词；另外两个自由空位并未出现于公式中。

```agda
    isOrdAt-in : (x : S) → IsOrd x → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩
    isOrdAt-in x o =
        ( λ a a∈x b hb → o .fst {a} {b} hb a∈x )
      , ( λ a a∈x b b∈a c hc → o .snd a a∈x {b} {c} hc b∈a )
isOrd-at-p : Formula (⊥* {ℓ-suc ℓ}) 3
```

三空位公式的第一个合取支说：参数的成员的成员都是参数的成员，即在第二空位处读取的传递性。

```agda
isOrd-at-p =
    (∀̇∈ (var (suc zero))
      (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc (suc zero))))))
  ∧̇ (∀̇∈ (var (suc zero))
      (∀̇∈ (var zero)
```

第二个合取支说明参数的每个成员 `a` 都传递：若 `c ∈ b ∈ a`，则 `c ∈ a`。

```agda
        (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
```

其有界性证书循同样的递归。随后消去引理开始：对无常数出现的公式，消去常数保持 Δ₀ 证书，逐子句成立。

```agda
Δ₀-isOrd-at-p : Δ₀ isOrd-at-p
Δ₀-isOrd-at-p = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
erase-Δ₀ : {m : ℕ} (φ : Formula CS.S m) (p : countFo φ ≡ 0)
         → Δ₀ φ → Δ₀ (Cnt.erase φ p)
erase-Δ₀ (t ∈̇ u) p δ-∈ = δ-∈
```

原子原样通过，命题联结词按结构递归，因为消去是结构性施加的。

```agda
erase-Δ₀ (t ≐ u) p δ-≐ = δ-≐
erase-Δ₀ (φ ∧̇ ψ) p (δ-∧ c d) = δ-∧ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ∨̇ ψ) p (δ-∨ c d) = δ-∨ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ⇒̇ ψ) p (δ-⇒ c d) = δ-⇒ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ ⊥̇ p δ-⊥ = δ-⊥
```

有界量词情形递归处理其矩阵。

```agda
erase-Δ₀ (∀̇∈ t φ) p (δ-∀∈ c) = δ-∀∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇∈ t φ) p (δ-∃∈ c) = δ-∃∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇ φ) p ()
erase-Δ₀ (∀̇ φ) p ()
```

## 凝聚所需的壳数据

非有界量词情形不可能出现，因为 `Δ₀` 证书没有对应构造子。

```agda
module HullStage (lam : S) (ordλ : IsOrd lam)
```

框架收取：一个其指数容纳成员后继的层、包含于该层的起始集合，以及空集属于该指数。

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

在 `Lset lam` 内，起始集合生成 Skolem 壳 `M`。`M` 的每个元素仍属于该层。

```agda
  module ASt = AtStage lam ordλ
    using ( module AbsL; module AtM; module Hull; Ltr; SL; wL )
```

原集合与作为回退值的空集都在壳构造中得到呈现。

```agda
  module H = ASt.Hull X X⊆L ∅∈λ
    using ( module T; module XInM; Hull⊆L; X⊆M; hull-member
          ; val-in-Hull; ∅∈Lsetα; inStg )
```

这个集合 `M` 是凝聚论证所使用的载体，其初等性与 Mostowski 塌缩构成论证的数据。

```agda
  M : S
  M = H.T.Hull
```

对壳 `M`，令 `π` 为其 Mostowski 塌缩，`πX` 为塌缩像。每个塌缩后的壳中点都属于 `πX`，`πX` 的每个成员都来自壳中的一点，并且 `πX` 是传递的。此外，塌缩固定壳中的每个传递点。

```agda
  module C = Collapse M
    using ( module InjExt; π; πX; πX-intro; πX-member; πX-trans; fixes )
```

凝聚论证对塌缩像作两项假设。第一，若序数 `δ` 属于该像，则层 `Lset δ` 也属于该像。第二，每个壳成员的塌缩都属于某个层，而该层的序数指数属于塌缩像。这两项闭合与覆盖性质将把塌缩像认同为 `L` 的一个层。

```agda
  module Condense
    (levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ C.πX ⟩ → ⟨ Lset δ ∈ˢ C.πX ⟩)
    (cover : (y : S) → ⟨ y ∈ˢ M ⟩
           → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ C.π y ∈ˢ Lset γ ⟩) ∥₁)
    where
```

分离构造出恰由 `πX` 中序数组成的集合。因此 `β` 记录塌缩像的序数部分。其分离谓词正是那条陈述序数性的有界公式，凭 Δ₀ 证书在每个环境处都是小的。

```agda
    β-sep : Σ[ s ∈ S ]
              (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt)))
    β-sep = separateFromSmall C.πX (λ y → (y ∷ []) ⊨ₚ isOrdAt)
              (λ y → D0.Δ₀-small Δ₀-isOrdAt (y ∷ []))
```

我们把这个序数部分记为 `β`；下面证明它本身是序数，并且它所索引的层恰为塌缩像。

```agda
    β : S
    β = β-sep .fst
```

属于 `β`，等价于属于 `πX`，并且把该成员赋给自由变元后满足无常元的序数公式。

```agda
    β-spec : (y : S) → (y ∈ˢ β) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt))
    β-spec = β-sep .snd
```

定义等价的第一个投影表明：beta 的每个成员都是塌缩像的成员。

```agda
    β∈πX : (δ : S) → ⟨ δ ∈ˢ β ⟩ → ⟨ δ ∈ˢ C.πX ⟩
    β∈πX δ δ∈β = subst ⟨_⟩ (β-spec δ) δ∈β .fst
```

第二个分量把这条无常元一自由变元公式的满足转换为外围宇宙中的序数性。

```agda
    β-ord : (δ : S) → ⟨ δ ∈ˢ β ⟩ → IsOrd δ
    β-ord δ δ∈β = Amb.isOrdAt-out δ (subst ⟨_⟩ (β-spec δ) δ∈β .snd)
```

反之，塌缩像的序数落入 beta：隶属与序数性两个定义分量一并提供，定义等价再把它们送回 beta 内部。

```agda
    ord∈β : (δ : S) → ⟨ δ ∈ˢ C.πX ⟩ → IsOrd δ → ⟨ δ ∈ˢ β ⟩
    ord∈β δ δ∈πX oδ = subst ⟨_⟩ (sym (β-spec δ)) (δ∈πX , Amb.isOrdAt-in δ oδ)
```

为证明 `β` 是序数，需要验证其两项定义条件。第一项是传递性：每当 `z ∈ x ∈ β`，都须有 `z ∈ β`。

```agda
    β-isOrd : IsOrd β
    β-isOrd = β-trans , β-mem
      where
      β-trans : isTransV β
      β-trans {x = x} {y = z} z∈x x∈β =
```

传递性在中间隶属处使用塌缩像的传递性，并从外围公式读取中间点的序数性；第二字段随之成立，因为 beta 的每个成员都是序数，故传递。

```agda
        subst ⟨_⟩ (sym (β-spec z))
          ( C.πX-trans {x = x} {y = z} z∈x (β∈πX x x∈β)
          , Amb.isOrdAt-in z (mem-ord {A = x} (β-ord x x∈β) z z∈x) )
      β-mem : (x : S) → ⟨ x ∈ˢ β ⟩ → isTransV x
      β-mem x x∈β = β-ord x x∈β .fst
```

覆盖假设从壳成员提升到塌缩成员。由于塌缩成员仅仅是某个壳成员的塌缩，该壳成员的覆盖沿此同一视搬运。

```agda
    covered : (x : S) → ⟨ x ∈ˢ C.πX ⟩
            → ∥ Σ[ γ ∈ S ]
                 (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
    covered x x∈πX = PT.rec squash₁ go (C.πX-member x x∈πX)
      where
```

该求逆正是塌缩自身的成员描述：像的成员仅仅是某个壳成员的塌缩。

```agda
      go : Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (C.π y ≡ x))
         → ∥ Σ[ γ ∈ S ]
              (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
      go (y , y∈M , e) = PT.map
        (λ { (γ , oγ , γ∈πX , h) →
```

覆盖沿塌缩值的相等搬运。提升后的命题随即被直接使用：beta 的每个序数都位于 beta 中更大的序数之内，这就是凝聚论证的经典极限层步骤。

```agda
          γ , oγ , γ∈πX , subst (λ w → ⟨ w ∈ˢ Lset γ ⟩) e h })
        (cover y y∈M)
    β-succ : (δ : S) → ⟨ δ ∈ˢ β ⟩
           → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩) ∥₁
    β-succ δ δ∈β = PT.map go (covered δ (β∈πX δ δ∈β))
```

delta 的序数性从 beta 读出；转换把覆盖结论改写为隶属形式：包含 delta 的层可取其指数落在 beta 内。

```agda
      where
      oδ : IsOrd δ
      oδ = β-ord δ δ∈β
      go : Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ δ ∈ˢ Lset γ ⟩)
         → Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
```

由于 `δ` 与 `γ` 都是序数，`δ ∈ Lset γ` 推出 `δ ∈ γ`；又因 `γ` 是 `πX` 中的序数，所以 `γ ∈ β`。随后陈述反向包含：塌缩的每个成员都属于 beta 处的层。

```agda
      go (γ , oγ , γ∈πX , δ∈Lγ) =
        γ , oγ , ord∈Lset→∈ γ oγ δ oδ δ∈Lγ , ord∈β γ γ∈πX oγ
    πX⊆Lβ : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ x ∈ˢ Lset β ⟩
    πX⊆Lβ x x∈πX = PT.rec (snd (x ∈ˢ Lset β)) go (covered x x∈πX)
      where
```

反向包含成立，因为 beta 处的层包含所有更小的层：层构造的单调性把覆盖层搬入 beta 之内。

```agda
      go : Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩)
         → ⟨ x ∈ˢ Lset β ⟩
      go (γ , oγ , γ∈πX , x∈Lγ) =
        Lset-mono {α = β} {β = γ} (ord∈β γ γ∈πX oγ) x∈Lγ
    Lβ⊆πX : (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ C.πX ⟩
```

正向包含按层构造分解 beta 层的成员，而极限步供给 beta 内更大的序数。

```agda
    Lβ⊆πX x x∈Lβ = PT.rec (snd (x ∈ˢ C.πX)) go (Lset-out β x x∈Lβ)
      where
      go : Σ[ δ ∈ S ] (⟨ δ ∈ˢ β ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
         → ⟨ x ∈ˢ C.πX ⟩
      go (δ , δ∈β , x∈𝒟ₒδ) = PT.rec (snd (x ∈ˢ C.πX)) liftStage (β-succ δ δ∈β)
```

陈述提升层：从 beta 内包含 delta 的序数，产出 `x` 在塌缩中的隶属。

```agda
        where
        liftStage : Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
             → ⟨ x ∈ˢ C.πX ⟩
        liftStage (γ , oγ , δ∈γ , γ∈β) =
          C.πX-trans {x = Lset γ} {y = x}
```

提升复合两条闭合：由于 `x` 定义在 gamma 之下的 delta 处，gamma 的层包含 `x`；又由第一条假设，塌缩像包含 gamma 处的层。两条包含随即在宇宙的外延性处会合。

```agda
            (Lset-in γ δ x δ∈γ x∈𝒟ₒδ)
            (levelIn γ oγ (β∈πX γ γ∈β))
    ext : C.πX ≡ Lset β
    ext = extensionality C.πX (Lset β) (sub , sup)
      where
```

外延性论证的前一半让每个成员经桥进入层读法，应用反向包含，再经桥返回。

```agda
      sub : (x : S) → ⟨ x ∈ₛ C.πX ⟩ → ⟨ x ∈ₛ Lset β ⟩
      sub x x∈ₛπX = ∈∈ₛ {a = x} {b = Lset β} .fst
        (πX⊆Lβ x (∈∈ₛ {a = x} {b = C.πX} .snd x∈ₛπX))
      sup : (x : S) → ⟨ x ∈ₛ Lset β ⟩ → ⟨ x ∈ₛ C.πX ⟩
      sup x x∈ₛLβ = ∈∈ₛ {a = x} {b = C.πX} .fst
```

后半对正向包含做同样的事，两半合起来把塌缩像等同于 beta 处的层。

```agda
        (Lβ⊆πX x (∈∈ₛ {a = x} {b = Lset β} .snd x∈ₛLβ))
```

凝聚陈述就此成立：塌缩像等于序数 `β` 所索引的层。为作应用，取层 `Lset α` 与额外一点 `x` 的并集为起始集，并假设 `α ∈ lam`、`x ⊆ Lset α` 以及 `x ∈ Lset lam`。

```agda
    condenses : Σ[ γ ∈ S ] (IsOrd γ × (C.πX ≡ Lset γ))
    condenses = β , β-isOrd , ext
module UnionKit (α lam x : S) (ordα : IsOrd α) (ordλ : IsOrd lam)
  (α∈λ : ⟨ α ∈ˢ lam ⟩) (x⊆Lα : (z : S) → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ Lset α ⟩)
  (x∈Lλ : ⟨ x ∈ˢ Lset lam ⟩) (α∉ω : ⟨ α ∈ˢ ω ⟩ → Empty.⊥) where
```

起始集合是 `Lset α` 与单点集 `{x}` 的并集；单点集的分类给出 `x ∈ {x}`。

```agda
  X : S
  X = Lset α ∪ ⁅ x ⁆s
  x∈sgl : ⟨ x ∈ₛ ⁅ x ⁆s ⟩
  x∈sgl = SetPackage.classification (SingletonPackage x) x .snd refl
```

额外点经并集的右侧属于起始集合。

```agda
  x∈X : ⟨ x ∈ˢ X ⟩
  x∈X = cup-inr (Lset α) ⁅ x ⁆s x (∈∈ₛ {a = x} {b = ⁅ x ⁆s} .snd x∈sgl)
```

层的每个成员经左侧属于起始集合。

```agda
  Lα∈X : (z : S) → ⟨ z ∈ˢ Lset α ⟩ → ⟨ z ∈ˢ X ⟩
  Lα∈X = cup-inl (Lset α) ⁅ x ⁆s
```

单点集的特征刻画说明，`{x}` 的每个成员都等于 `x`。

```agda
  sgl≡ : (z : S) → ⟨ z ∈ˢ ⁅ x ⁆s ⟩ → z ≡ x
  sgl≡ = sgl-out x
```

因此，属于起始集分成两种情形：该点或者属于 `Lset α`，或者属于单点集 `{x}`。

```agda
  X-mem : (z : S) → ⟨ z ∈ˢ X ⟩
        → ⟨ (z ∈ˢ Lset α) ⊔ (z ∈ˢ ⁅ x ⁆s) ⟩
  X-mem = cup-out (Lset α) ⁅ x ⁆s
```

生成集包含于外围层：层一侧的成员沿指数包含、由层构造的单调性搬运。

```agda
  X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z z∈X = PT.rec (snd (z ∈ˢ Lset lam)) go (X-mem z z∈X)
    where
    go : (⟨ z ∈ˢ Lset α ⟩ ⊎ ⟨ z ∈ˢ ⁅ x ⁆s ⟩) → ⟨ z ∈ˢ Lset lam ⟩
    go (inl z∈Lα) = Lset-mono {α = lam} {β = α} α∈λ z∈Lα
```

单点一侧的成员化归为额外点，而额外点的层隶属本是假设。

```agda
    go (inr z∈sgl) = subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym (sgl≡ z z∈sgl)) x∈Lλ
```

生成集是传递的。若成员的成员位于层一侧，则由层的传递性它属于层，再由左包含把它放入生成集。

```agda
  Xtr : isTransV X
  Xtr {x = a} {y = b} b∈a a∈X = PT.rec (snd (b ∈ˢ X)) go (X-mem a a∈X)
    where
    go : (⟨ a ∈ˢ Lset α ⟩ ⊎ ⟨ a ∈ˢ ⁅ x ⁆s ⟩) → ⟨ b ∈ˢ X ⟩
    go (inl a∈Lα) = Lα∈X b (layer-trans (Lset-layer α) b∈a a∈Lα)
```

在单点集一侧，中间集合就是 `x`；假设 `x ⊆ Lset α` 随即把它的每个成员放入并集的左侧。

```agda
    go (inr a∈sgl) = Lα∈X b (x⊆Lα b
      (subst (λ u → ⟨ b ∈ˢ u ⟩) (sgl≡ a a∈sgl) b∈a))
  one∈α : ⟨ sucV ∅ ∈ˢ α ⟩
  one∈α = Sum.rec
      (λ α∈ω → Empty.rec (α∉ω α∈ω))
```

无穷即不属于 `ω`，序数三分法分拆各情形：属于 `ω` 与假设矛盾；等于 `ω` 则由数码一见证隶属；`ω` 低于 `α` 则由传递性把数码一放入 `α` 之内。

```agda
      (Sum.rec (λ α≡ω → subst (λ w → ⟨ sucV ∅ ∈ˢ w ⟩) (sym α≡ω) (#∈ω 1))
               (λ ω∈α → ordα .fst (#∈ω 1) ω∈α))
      (ord-tri α ordα ω ω-ord)
```

空集出现在第一个后继层，由基层编码沿后继层的描述搬运而来。

```agda
  ∅∈Lset1 : ⟨ ∅ ∈ˢ Lset (sucV ∅) ⟩
  ∅∈Lset1 = subst (λ w → ⟨ ∅ ∈ˢ w ⟩) (sym (Lset-suc ∅)) (∅∈𝒟ₒ ∅)
```

单调性先把空集提升到 `Lset α`，再到 `Lset lam`。

```agda
  ∅∈Lλ : ⟨ ∅ ∈ˢ Lset lam ⟩
  ∅∈Lλ = Lset-mono {α = lam} {β = α} α∈λ
    (Lset-mono {α = α} {β = sucV ∅} one∈α ∅∈Lset1)
```

秩刻画随之把它提升为空集属于指数 `lam` 本身。余下需要证明壳的外延性，这是使其塌缩成为单射所需的最后条件。

```agda
  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = subst (λ w → ⟨ w ∈ˢ lam ⟩) (rank-fix ∅ ∅-ord)
    (rank-Lset lam ordλ ∅ ∅∈Lλ)
module HullExt (α : S) (ordα : IsOrd α)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
```

空集属于指数这一假设，保证 `Lset α` 处的 Skolem 壳具有其项代数所需的默认值。

```agda
  (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
```

令 `M` 为 `Lset α` 内由 `X` 生成的 Skolem 壳。它到该层的包含是初等的。为证明限制在 `M` 上的隶属关系具有外延性，我们比较壳中公式与其在该层中的解释。

```agda
  module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
  module H = ASt.Hull X X⊆L ∅∈α using ( module T; Hull⊆L )
  module A = ASt.AtM H.T.Hull H.Hull⊆L using ( SM; inL; module SemM )
  module E = HullElemDown α ordα X X⊆L ∅∈α using ( elem )
  module Mse = A.SemM.At A.SM id using ( _⊨_ )
```

壳被命名；两集合的对称差在隶属真值层面陈述：一个点在一侧之中，且可证不在另一侧之中。

```agda
  M : S
  M = H.T.Hull
  Different : S → S → S → Type (ℓ-suc ℓ)
  Different x y z = (z ∈ᵗ x × (z ∈ᵗ y → Empty.⊥))
                  ⊎ (z ∈ᵗ y × (z ∈ᵗ x → Empty.⊥))
```

经典地，不等的集合必有一点位于其对称差中：这一截断存在由排中律判定。

```agda
  different : (x y : S) → (x ≡ y → Empty.⊥) → ∥ Σ[ z ∈ S ] Different x y z ∥₁
  different x y nxy = go (lem P)
    where
    P : hProp (ℓ-suc ℓ)
    P = ∥ Σ[ z ∈ S ] Different x y z ∥₁ , squash₁
```

若没有点区分这两个集合，则每个隶属真值都双向一致，宇宙的外延性将迫使二者相等，与假设矛盾。

```agda
    go : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → ⟨ P ⟩
    go (inl p) = p
    go (inr np) = Empty.rec (nxy (extensionalV (λ z → ⇔toPath (fwd z) (bwd z))))
      where
      fwd : (z : S) → z ∈ᵗ x → z ∈ᵗ y
```

一致的两个方向各由排中律判定，每个失败的方向都把它的点贡献给对称差。

```agda
      fwd z zx = Sum.rec (λ zy → zy)
        (λ nzy → Empty.rec (np ∣ z , inl (zx , nzy) ∣₁)) (lem (z ∈ˢ y))
      bwd : (z : S) → z ∈ᵗ y → z ∈ᵗ x
      bwd z zy = Sum.rec (λ zx → zx)
        (λ nzx → Empty.rec (np ∣ z , inr (zy , nzx) ∣₁)) (lem (z ∈ˢ x))
```

差公式是析取式 `(z ∈ x ∧ z ∉ y) ∨ (z ∈ y ∧ z ∉ x)`，两个常元槽分别放入这两个壳成员。

```agda
  φ : A.SM → A.SM → Formula A.SM 1
  φ x y = ((var zero ∈̇ con x) ∧̇ (¬̇ (var zero ∈̇ con y)))
        ∨̇ ((var zero ∈̇ con y) ∧̇ (¬̇ (var zero ∈̇ con x)))
  outer : (u v : S) (u∈M : u ∈ᵗ M) (v∈M : v ∈ᵗ M)
        → (z : S) → Different u v z
```

存在公式的满足是截断的，因此区分点也在截断之下返回。在对称差的任一分支中，同一点都见证该公式在层中相应的析取支。

```agda
        → ∥ Σ[ a ∈ ASt.SL ]
            ⟨ (a ∷ []) ASt.AbsL.⊨ᵐ (mapFo A.inL (φ (u , u∈M) (v , v∈M))) ⟩ ∥₁
  outer u v u∈M v∈M z d = ∣ a , ∣ objectDifferent d ∣₁ ∣₁
    where
    objectDifferent = Sum.map
```

在任一分支中，外围隶属给出肯定合取项，而不隶属证明被提升为公式语义所需的否定。层的传递性则把区分点放入该层载体。

```agda
      (λ (zu , nzv) → zu , λ zv → lift (nzv zv))
      (λ (zv , nzu) → zv , λ zu → lift (nzu zu))
    z∈L : ⟨ z ∈ˢ Lset α ⟩
    z∈L = Sum.rec
      (λ (zx , _) → layer-trans (Lset-layer α) zx (H.Hull⊆L u u∈M))
```

把区分点与其层隶属配对，便得到层载体中的见证。为证明壳的外延性，先假设壳中每个属于 `x` 的元素也属于 `y`。

```agda
      (λ (zv , _) → layer-trans (Lset-layer α) zv (H.Hull⊆L v v∈M)) d
    a : ASt.SL
    a = z , z∈L
  refute : (x y : S) (x∈M : x ∈ᵗ M) (y∈M : y ∈ᵗ M)
         → (ag1 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩)
```

反向再假设壳中每个属于 `y` 的元素也属于 `x`。若 `x` 与 `y` 仍不相等，则其对称差中的一点将导出矛盾。

```agda
         → (ag2 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩)
         → (x ≡ y → Empty.⊥) → Empty.⊥
  refute x y x∈M y∈M ag1 ag2 nxy = PT.rec Empty.isProp⊥ diff (different x y nxy)
    where
    xS : A.SM
```

两个壳成员被读作子结构载体的元素，准备代入差公式。

```agda
    xS = x , x∈M
    yS : A.SM
    yS = y , y∈M
```

反驳消去差点。初等性把层对该存在公式的满足，以差点为见证，转换为壳内对同一存在公式的满足。

```agda
    diff : Σ[ z ∈ S ] Different x y z → Empty.⊥
    diff (z , d) = PT.rec Empty.isProp⊥ inside h
      where
      h : ⟨ [] Mse.⊨ (∃̇ (φ xS yS)) ⟩
      h = subst ⟨_⟩ (sym (E.elem 0 (∃̇ (φ xS yS)) []))
```

初等性给出一个满足差公式的壳中见证。消去其截断的析取后，便得到两个非对称隶属陈述中成立的那个。

```agda
        (outer x y x∈M y∈M z d)
      inside : Σ[ b ∈ A.SM ] ⟨ (b ∷ []) Mse.⊨ φ xS yS ⟩ → Empty.⊥
      inside (b , q) = PT.rec Empty.isProp⊥ cases q
        where
        cases : (⟨ fst b ∈ˢ x ⟩ × (⟨ fst b ∈ˢ y ⟩ → Lift Empty.⊥))
```

无论哪个析取支，都会把见证认作一个壳成员的成员而非另一个的，相应的一致性假设与该否定矛盾。这一矛盾正是壳的外延性所需要的。

```agda
              ⊎ (⟨ fst b ∈ˢ y ⟩ × (⟨ fst b ∈ˢ x ⟩ → Lift Empty.⊥))
              → Empty.⊥
        cases (inl (bx , nby)) = lower (nby (ag1 (fst b) (snd b) bx))
        cases (inr (by , nbx)) = lower (nbx (ag2 (fst b) (snd b) by))
```

壳的外延性由经典反证法证明。由于集合的宇宙是 h-集合，`x ≡ y` 是命题，排中律因此给出相等或不相等。若 `x ≢ y`，`refute` 会在壳中找到一个只属于 `x`、`y` 之一的成员，这与两个隶属一致性前提矛盾；故 `x ≡ y`。

```agda
  hullExt : isExt M
  hullExt x y x∈M y∈M ag1 ag2 =
    Sum.rec (λ p → p) (λ np → Empty.rec (bad np))
      (lem ((x ≡ y) , isSetS x y))
    where
```

`bad` 消去矛盾分支，完成壳的外延性。

```agda
    bad : (x ≡ y → Empty.⊥) → Empty.⊥
    bad = refute x y x∈M y∈M ag1 ag2
```

## 沿塌缩搬运有界公式

为比较塌缩与外围宇宙，现固定一个传递集 `U`。无常元的 Δ₀ 公式在 `U` 的成员处求值时，在 `U` 上的受限结构与外围结构中具有相同真值。

```agda
module Unpack (U : S) (Utr : isTrans U) where
```

受限载体 `SM` 的元素由一个集合及其属于 `U` 的证据组成。把这些二元组逐项投影到第一分量，便得到对应的外围环境；有界绝对性 `abs₀` 比较投影前后的满足关系。

```agda
  module Ab = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ U) Utr using (SM; abs₀; _⊨ᵐ_)
```

对无常元的 Δ₀ 公式 `φ`，`read` 先把 `embed φ` 看作受限载体上的公式。有界绝对性比较其受限读法与外围读法；`embed-⊨` 消去由嵌入引入的改名，空常元域到任意类型的函数唯一性再同一视余下的常元解释。

```agda
  read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Ab.SM ^ n)
       → (δ Ab.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
  read {n} {φ} dφ δ =
      Ab.abs₀ (mapΔ₀ Empty.rec* dφ) δ
    ∙ embed-⊨ 𝒮ᵥ {K = Ab.SM} fst φ (map fst δ)
```

最后一条路径使用函数外延性：常元域为空，所以两种常元解释逐点相同，因而相等。随后固定 `Lset lam` 内构造壳所需的数据：对后继封闭的序数 `lam`，以及起始集合 `X ⊆ Lset lam`。

```agda
    ∙ cong (λ ι → SemV.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ)
           (funExt (λ b → Empty.rec* b))
module Frame (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
```

还假设 `∅ ∈ lam`；这是壳构造所需的基础层前提。

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
```

令 `M` 为 `Lset lam` 内由 `X` 生成的壳。下文使用它到该层的包含、相应的初等性概念，以及上文证明的外延性。

```agda
  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using (module ASt; module C; module Condense; module H; M)
  module ASt = HS.ASt using (module AbsL; module AtM; Ltr; SL)
  module A = ASt.AtM HS.M HS.H.Hull⊆L using (Elementary; SM; module SemM; inL)
  module HE = HullExt lam ordλ X X⊆Lλ ∅∈λ using (hullExt)
```

因此 `M` 是外延的；这正是把 `M` 与其传递的 Mostowski 塌缩同一视所需的前提。

```agda
  Mext : isExt HS.M
  Mext = HE.hullExt
```

搬运论证显式取得包含 `M → Lset lam` 的初等性。它与 `M` 的外延性一起给出下文的两种比较：从壳到层，以及从壳到其塌缩。

```agda
  module Carry (elem : A.Elementary) where
```

现在要比较三个结构：壳 `M`、层 `Lset lam` 与传递塌缩像 `πX`。塌缩同构联系第一个与第三个结构，有界绝对性则把两个传递集各自联系到外围宇宙。

```agda
    module CIso = CollapseIso HS.M Mext using (module I; iso-fwd; iso-bwd)
    module TL = Unpack (Lset lam) ASt.Ltr using (read)
    module Tπ = Unpack HS.C.πX HS.C.πX-trans using (module Ab; read)
```

隶属由塌缩直接保持：隶属同构的正向恰是原子隶属所需的推送。

```agda
    member-push : (x y : S) → ⟨ x ∈ˢ HS.M ⟩ → ⟨ y ∈ˢ HS.M ⟩
                → ⟨ y ∈ˢ x ⟩ → ⟨ HS.C.π y ∈ˢ HS.C.π x ⟩
    member-push = CIso.iso-fwd
```

由于 `Lset lam` 是传递的，每条无常元 Δ₀ 公式在该层的受限读法与外围读法相同；`atL` 就是 `read` 在此层的实例。

```agda
    atL : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : ASt.SL ^ n)
        → (δ ASt.AbsL.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atL dφ δ = TL.read dφ δ
```

塌缩像 `πX` 也具有传递性，因此无常元 Δ₀ 公式在那里同样具有内外一致的读法。

```agda
    atπ : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Tπ.Ab.SM ^ n)
        → (δ Tπ.Ab.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atπ dφ δ = Tπ.read dφ δ
```

壳自身载体处的读法经由初等性分解：嵌入公式先在内部读取；由于该公式无常元，改名固定不动；结果再搬运到层读法。

```agda
    atM : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
        → (δ CIso.I.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atM {n} {φ} dφ δ =
        elem n (embed φ) δ
      ∙ cong (λ ψ → map A.inL δ ASt.AbsL.⊨ᵐ ψ) (embed-map A.inL φ)
```

经过层上的绝对性后，只需比较两个环境。把壳成员包含进 `Lset lam` 不改变其底层集合，因此先包含再投影所得的外围集合向量，等于直接投影原环境所得的向量。

```agda
      ∙ atL dφ (map A.inL δ)
      ∙ cong (λ γ → γ ⊨ₚ φ) (map-inL-fst δ)
      where
      map-inL-fst : {m : ℕ} (γ : A.SM ^ m)
                  → map fst (map A.inL γ) ≡ map fst γ
```

该等式对空环境立即成立，并在环境前添加一个分量时保持。因此，对无常元 Δ₀ 公式，壳成员环境处的外围真值蕴含其塌缩值环境处的外围真值。

```agda
      map-inL-fst [] = refl
      map-inL-fst (q ∷ γ) = cong (fst q ∷_) (map-inL-fst γ)
    push : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
         → ⟨ map fst δ ⊨ₚ φ ⟩
         → ⟨ map fst (map CIso.I.g δ) ⊨ₚ φ ⟩
```

从壳环境处的外围真值出发，先反向使用 `atM` 得到壳中的内部真值；`iso-inv` 把它搬到塌缩像，`embed-map` 消去无内容的常元改名，最后正向使用 `atπ` 得到塌缩值处的外围真值。

```agda
    push {n} {φ} dφ δ h =
      subst ⟨_⟩ (atπ dφ (map CIso.I.g δ))
        (subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
               (embed-map CIso.I.g φ)
               (CIso.I.iso-inv n (embed φ) δ (subst ⟨_⟩ (sym (atM dφ δ)) h)))
```

在 `pull` 中，塌缩值处的外围真值先沿 `atπ` 反向进入塌缩像；`embed-map` 恢复改名后的形式，`iso-inv-bwd` 再返回壳中的内部真值，最后正向使用 `atM`，恢复原壳环境处的外围真值。

```agda
    pull : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
         → ⟨ map fst (map CIso.I.g δ) ⊨ₚ φ ⟩
         → ⟨ map fst δ ⊨ₚ φ ⟩
    pull {n} {φ} dφ δ h =
      subst ⟨_⟩ (atM dφ δ)
```

`push` 与 `pull` 合起来表明：对每条无常元 Δ₀ 公式及每个由壳成员组成的有限环境，把各分量换成其塌缩值不会改变外围满足。另一个引理 `member-push` 则直接给出隶属关系的相应保持性。

```agda
        (CIso.I.iso-inv-bwd n (embed φ) δ
          (subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
                 (sym (embed-map CIso.I.g φ))
                 (subst ⟨_⟩ (sym (atπ dφ (map CIso.I.g δ))) h)))
```