Bedrock可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。
交互式目录 · 依赖图模块把宇宙层级固定为 ℓ，并按本书的固定形式陈述经典假设：排中律以显式参数在 ℓ-suc ℓ 处领取，从不全局假设，因此本章每条定理都准确记录所用的是哪个层级的实例。
module L.GCH.SkolemHull {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
本章在可构造层内对起始集合作 Skolem 壳，证明壳在层中初等，再经保持成员关系的双射把它塌缩到传递集上，并整理满足关系与有界公式如何跨过这次塌缩。关键区别是：壳本身只是编码所得的像；传递性只在 Mostowski 塌缩之后出现。
本章依赖经典逻辑，假设在此引入。壳的构造要判定查询的可满足性，外延性证明要双向判定成员关系，初等性移送要消去双重否定；这些步骤都在消耗排中律。
open import Cubical.Relation.Nullary using ( decRec )
open import Cubical.HITs.PropositionalTruncation using ( map2 )
open import Cubical.Data.Sum using () renaming ( map to sumMap )
open import Cubical.Data.Vec using ( _++_ )
对象语言即本书的一阶语言：公式由项经等词与成员关系构成，对命题联结词、非有界量词与有界量词封闭。谓词 Δ₀ 挑出全部量词都有界的公式。
谓词 Δ₀ 是沿公式结构定义的归纳证书：其构造子覆盖原子式、联结词与有界量词，而无界量词没有对应构造子。这种证书支撑后文的绝对性论证；countFo 与 constantsFo 记录常元的每次出现。
参数抽象用额外的环境变元替换常元出现；常元映射与常元改名在保持语义的同时改变常元字母表；renameTm 则沿语境映射改名变元槽，由此得到下文以 suc 实现的弱化。外围层级连同其外延性一同打开，外延性即元素相同的集合相等。
呈现用一个带嵌入的小类型索引集合的元素，其纤维为被呈现元素命名。塌缩对任意载体 X 构造一个传递像；要使塌缩映射在 X 上单射，还需受限成员关系满足外延性。Δ₀ 小性把有界可定义的类分离成集合。空集属于每个可定义性后继，而 Lset-suc 把后继指标处的层认同为前一层的可定义幂集。
可构造层 Lset α 是传递的，且其构造对指数单调，故更大的指数给出更大的层。壳论证中反复用到的序数事实有：序数的元素是序数、ω 是序数、数码属于 ω、空集是序数。
良序自带最小元选择器：从「存在某元素满足谓词」的截断陈述出发，它返回一个满足谓词且在良序下最小的元素。层成员关系的秩刻画与限制到层载体的层序为该选择器供给输入，而并与单点的编码则构造后文使用的有限起始集合。
本章的环境是载体元素构成的向量，其运算逐分量进行：把函数映射到环境上、按索引查找、添入一个元素、以及拼接。第二分量为命题的对把元素与永不区分的证书一并记录。
空类型表示矛盾：⊥*-rec 可把其元素消去到任意目标，而 isProp⊥ 使目标为矛盾时可以消去命题截断。存在公式的满足以及呈现集合中的成员关系用命题截断表达，因而保留存在性而不选定见证。
累积层级用索引类型与赋值呈现集合。壳以有限树类型 Code 为索引类型；公式是见证码中的字段，并不自身充当码。构造部分供给空集、并、无序对与单点集构造，以及无穷序数及其后继。
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 )
小成员关系 _∈ₛ_ 及其与外围成员关系 _∈ˢ_ 之间的桥 ∈∈ₛ，把一个集合的呈现读法与它在层级中的读法连接起来：呈现内部所记录的，恰是宇宙中成立的。
open import Cubical.HITs.CumulativeHierarchy.Properties
using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; extensionality )
打开外围结构后，无修饰的等号与成员关系符号固定表示外围关系；下文的受限结构仍各有自己的语义解释。
open hPropView 𝒮ᵥ
SemV 给出下文实例化满足关系时使用的定长外围环境。对常元取自 𝒮ʟ 的公式，出现次数计数识别无常元情形；erase 随后把不可能出现的常元域换为空类型，而不改变满足关系。
module SemV = FOL.Semantics 𝒮ᵥ using ( module At )
module CS = hPropView 𝒮ʟ using ( S )
module Cnt = FOL.Manipulation.ConstantOccurrences.ZeroOccurrences CS.S using ( erase; erase-inv )
在空常元域上，Δ₀-small 证明每个有界公式在每个环境中的真值都等价于低一层宇宙中的命题；要得到分离还需另行应用 separateFromSmall。项代数随之开始：它以一个结构、把其载体映入外围宇宙的映射，以及该载体上的良序为参数。
module D0 = Δ₀Small {ℓc = ℓ-suc ℓ} {K = ⊥* {ℓ-suc ℓ}} (λ b → ⊥*-rec b)
using ( Δ₀-small )
module TermAlgebra (𝒮 : ZFStructureₕ (ℓ-suc ℓ))
(toSet : ZFStructure.S 𝒮 → V ℓ)
(wo : SWO (ZFStructure.S 𝒮))
(junk : ZFStructure.S 𝒮)
{K : Type ℓ} (emb : K → ZFStructure.S 𝒮) where
其余参数是默认元素 junk 与以 K 为索引的基生成元族；只有后文的壳实例把 K 认同为起始集合的一个呈现。垃圾值只是簿记装置，下文的构造从不检视它。
这里只隐藏参数结构中未加限定的 Agda 名 _∈ˢ_；满足关系 _⊨₀_ 仍用 𝒮 解释原子成员关系。为载体改名，则使本章对外围载体的指称保持无歧义。
open ZFStructure 𝒮 hiding ( _∈ˢ_ ) renaming ( S to S𝒮 )
项代数的满足在平凡为空的常元域上陈述：被求值的公式恰是无常元符号构成的那些，即纯粹的成员关系与相等语言，且满足取值于命题。本节的每条查询与闭合陈述都采用这一读法。
private module Sem = FOL.Semantics 𝒮
module At0 = Sem.At (⊥* {ℓ}) ⊥*-rec using ( _⊨_ )
_⊨₀_ : {n : ℕ} → Vec S𝒮 n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
_⊨₀_ = At0._⊨_
码构成基生成元上的有限树代数：基码指名一个生成元；见证码记录一个元数为 suc k 的查询连同 k 个参数码。由于 Code 是归纳类型，每个码都是有限树；cs 的分量是当前码的直接参数子码，每个子码都可再是基码或见证码。
data Code : Type ℓ where
base : K → Code
wit : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec Code k → Code
Sat k ψ vs 是「存在元素在任意参数向量 vs 处满足 ψ」的仅仅存在；闭合定理随后把 vs 特化为码的取值。可满足性被陈述为截断的存在：它断言见证存在，而不产出见证。
Sat : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec S𝒮 k → Type (ℓ-suc ℓ)
Sat k ψ vs = ∥ Σ[ a ∶ S𝒮 ] ⟨ (a ∷ vs) ⊨₀ ψ ⟩ ∥₁
satDecision : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
→ Dec (Sat k ψ vs)
satDecision k ψ vs = Sem.decideSatisfaction ⊥*-rec lem vs (∃̇ ψ)
搜索谓词由查询中已经存放的公式呈现。其环境把候选放在最前的新槽位，再接上固定的参数向量。读取证明就是自反性，因为宿主谓词按定义恰是这条满足判断。
searchPredicate : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
→ Sem.FormulaPredicate S𝒮 (⊥* {ℓ}) ⊥*-rec
(λ a → (a ∷ vs) ⊨₀ ψ)
searchPredicate k ψ vs = Sem.presented (suc k) ψ (λ a → a ∷ vs) (λ a → refl)
有了这条截断存在，search 就参数 wo 所供给的特定严格良序返回一个最小的满足元素。「最小」指该良序下的最小；它既不是关于成员关系的极小，也不是秩的比较。
search : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
→ Sat k ψ vs → S𝒮
search k ψ vs w = leastOfFormula wo (searchPredicate k ψ vs) lem w .fst
码向量逐分量求值，与单个码的求值相互定义：见证码的参数取值即其分量码的取值。
mutual
vals : {m : ℕ} → Vec Code m → Vec S𝒮 m
vals [] = []
vals (c ∷ cs') = val c ∷ vals cs'
可满足的见证码求值为最小的满足元素；不可满足的见证码求值为 junk。由于每个码都向像贡献一个值，junk 可能出现在壳中；而 val-wit 表明，一旦给出可满足性，junk 便无关紧要。
val : Code → S𝒮
val (base m) = emb m
val (wit k ψ cs) = decRec (search k ψ (vals cs)) (λ _ → junk)
(satDecision k ψ (vals cs))
这条小引理记录：一旦命题目标已知有元素，经典判定如何被使用。若判定落在左支，命题性把其中的元素与 x 认同，故消去式等于 f x；若落在右支，其中的否定与 x 矛盾，因此该情形不可能。
sum-stuck : {X : Type (ℓ-suc ℓ)} (x : X) (px : isProp X)
→ (f : X → S𝒮) (g : (X → ⊥₀) → S𝒮) (s : Dec X)
→ decRec f g s ≡ f x
sum-stuck x px f g (yes x') = sym (cong f (px x x'))
sum-stuck x px f g (no h) = ⊥₀-rec (h x)
给定见证码所存查询的可满足性见证，这条引理即可确认：该码的取值就是搜索的最小满足元素；垃圾分支被反驳，有见证的分支运行搜索。
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)
(satDecision k ψ (vals cs))
码向量的求值等同于对其映射求值，由简单递归证明。这使得后文的陈述可以在环境的递归形式与映射形式之间自由通行。
vals≡map : {m : ℕ} (cs : Vec Code m) → vals cs ≡ map val cs
vals≡map [] = refl
vals≡map (c ∷ cs') = cong₂ _∷_ refl (vals≡map cs')
壳的呈现与层级呈现集合的方式相同：一个码族加一个赋值。它是全部码取值的像；由于不同码可能求值相同，呈现可以重复元素。因此壳中的成员关系只是「存在某个码」的截断陈述，本章不主张壳传递，也不主张它是最小的闭合集合。
Hull : V ℓ
Hull = sett Code (λ c → toSet (val c))
呈现中的成员关系是直接的：任何码的取值都是壳的元素，其见证正是该码本身。
inHull : (c : Code) → ⟨ toSet (val c) ∈ˢ Hull ⟩
inHull c = ∣ c , refl ∣₁
于是每条可满足的编码查询都在壳中有满足的见证。该定理断言的正是这条闭合性质；它并不把壳的全部元素都刻画为成功的最小见证。
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 ∣₁
见证无需另寻：它就是项代数已赋予的取值，即搜索返回的最小满足元素。
where
a : S𝒮
a = search k ψ (vals cs) w
选择器返回 a 以及 IsLeast 的两个分量：a 满足查询的证明，和不存在严格更小的满足元素的证明；本行投影前一分量。
pa : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
pa = leastOfFormula wo (searchPredicate k ψ (vals cs)) lem w .snd .fst
见证属于壳，来自专为该查询构造的见证码：其取值经 val-wit 被认同为搜索结果，而每个码的取值都在壳中。
a∈H : ⟨ toSet a ∈ˢ Hull ⟩
a∈H = subst (λ z → ⟨ toSet z ∈ˢ Hull ⟩) (val-wit k ψ cs w)
(inHull (wit k ψ cs))
满足即被记录的分量，闭合子句就此完成。
sat : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
sat = pa
沿载体映射搬运满足关系
壳已建成并闭合，本章转向第二个任务，即在结构之间搬运满足关系；移送模块就外围载体上的两个谓词陈述。
module SatTransfer (MA MB : S → hProp (ℓ-suc ℓ)) where
源载体把外围载体的每个元素与「它满足第一个谓词」的证明配对；其公式只在这种对上读取。
SA : Type (ℓ-suc ℓ)
SA = Σ[ x ∶ S ] ⟨ MA x ⟩
目标载体是第二个谓词上的同一构造；那里的满足是对同一公式的目标读法。
SB : Type (ℓ-suc ℓ)
SB = Σ[ x ∶ S ] ⟨ MB x ⟩
源结构在配对载体上读取公式：项词典把变元解释为配对中的元素，满足取值于命题。
module SemA = FOL.Semantics (𝒮ᵥ ↾ MA)
using ( module At )
module SemB = FOL.Semantics (𝒮ᵥ ↾ MB)
using ( module At )
open SemA.At SA id renaming ( _⊨_ to _⊨ᴬ_ ; ⟦_⟧ to ⟦_⟧ᴬ )
目标结构在另一侧做同样的事，拥有自己的满足与自己的项词典。
open SemB.At SB id renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
移送由两条原理组织。一致性对每条公式与每个环境陈述命题的相等：左侧的满足等于映射环境上映射公式的满足。接下来陈述的见证原理支撑存在量词的反向：目标侧存在式为真时，只须仅仅给出某个 q : SA，使其像满足矩阵。
Agree : (SA → SB) → Type (ℓ-suc (ℓ-suc ℓ))
Agree g = (n : ℕ) (φ : Formula SA n) (δ : Vec SA n)
→ (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
Witness : (SA → SB) → Type (ℓ-suc ℓ)
Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : Vec SA n)
它不要求该 q 是某个既定目标见证的原像；该原理只主张存在某个内部点的像满足矩阵的截断陈述，而这恰是存在量词反向所消耗的形式。
→ ⟨ map g δ ⊨ᴮ mapFo g (∃̇ φ) ⟩
→ ∥ Σ[ q ∶ SA ] ⟨ (g q ∷ map g δ) ⊨ᴮ mapFo g φ ⟩ ∥₁
移送模块收取映射连同原子假设：原子成员关系与相等必须沿 g 双向一致，如此归纳中的原子成员关系与相等才能成为命题的路径。
module Along (g : SA → SB)
(at∈ : (n : ℕ) (t u : Term SA n) (δ : Vec SA n)
→ (δ ⊨ᴬ (t ∈̇ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ∈̇ u)))
(at≐ : (n : ℕ) (t u : Term SA n) (δ : Vec SA n)
→ (δ ⊨ᴬ (t ≐ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ≐ u)))
(wit : Witness g) where
见证原理是第三条假设，移送的数据就此齐备。
第一条弱化事实在源结构中陈述。沿 suc 改名把每个旧变元移过环境中新添的首槽，故在 x ∷ δ 处求值还原为在 δ 处求值；常元不受影响。
private
renA : {n : ℕ} (t : Term SA n) (x : SA) (δ : Vec SA n)
→ ⟦ renameTm suc t ⟧ᴬ (x ∷ δ) ≡ ⟦ t ⟧ᴬ δ
renA (con c) x δ = refl
renA (var i) x δ = refl
同样的弱化在目标结构中也成立；下一条陈述开始比较映射与弱化。
renB : {n : ℕ} (t : Term SB n) (x : SB) (δ : Vec SB n)
→ ⟦ renameTm suc t ⟧ᴮ (x ∷ δ) ≡ ⟦ t ⟧ᴮ δ
renB (con c) x δ = refl
renB (var i) x δ = refl
mapTm-ren : {n : ℕ} (t : Term SA n)
映射与弱化在项上交换，这是定义性的：弱化项的映射逐个弱化被改名的分量。
→ mapTm g (renameTm suc t) ≡ renameTm suc (mapTm g t)
mapTm-ren (con c) = refl
mapTm-ren (var i) = refl
被映射的弱化项在任意目标点 x 接映射环境处求值，与被映射项在映射环境处的值相同。
renG : {n : ℕ} (t : Term SA n) (x : SB) (δ : Vec 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 δ)
对项的成员关系不受弱化影响，其形式恰为有界子句所消耗者；下一条引理陈述边条件的转移本身。
memRen : {n : ℕ} (t : Term SA n) (x : SB) (δ : Vec SA n)
→ (x .fst ∈ˢ (⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ)) .fst)
≡ (x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst)
memRen t x δ = cong (λ s → x .fst ∈ˢ s .fst) (renG t x δ)
memPath : {n : ℕ} (t : Term SA n) (q : SA) (δ : Vec SA n)
有界量词的边条件跨越映射转移。链条先在源结构中弱化，再在移位环境处应用原子的成员关系假设。
→ (q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst)
≡ ((g q) .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst)
memPath {n} t q δ =
cong (λ s → q .fst ∈ˢ s .fst) (sym (renA t q δ))
∙ at∈ (suc n) (var zero) (renameTm suc t) (q ∷ δ)
链条以目标结构中的弱化结束。有了它，任何有界子句的边条件都可在映射两侧读取。
∙ memRen t (g q) δ
经典步骤被打包一次：对命题而言，双否消去由排中律而来。全称子句的正向先假设目标侧存在反例，把它包装成否定矩阵的存在见证，再用 Witness 拉回内部反例并推出矛盾；最后由 dne 得到所需的目标侧真值。
dne : (P : hProp (ℓ-suc ℓ)) → (((⟨ P ⟩) → ⊥₀) → ⊥₀) → ⟨ P ⟩
dne P h = decRec (λ p → p)
(λ (np : ⟨ P ⟩ → ⊥₀) → ⊥₀-rec (h np)) (lem P)
归纳现在沿十条子句运行，而它恰从假设所在处开始：两条原子子句正是 at∈ 与 at≐。命题联结词逐分量搬运，因为命题上的合取、析取与蕴含都由其分量决定。
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 ψ δ)
蕴含同样逐分量搬运，假值恒定，而存在子句以一个双条件开场。其正向陈述：内部对存在式的满足映射为「映射环境上映射存在式」的满足。
agree n (φ ⇒̇ ψ) δ = cong₂ _⇒_ (agree n φ δ) (agree n ψ δ)
agree n ⊥̇ δ = refl
agree n (∃̇ ψ) δ = ⇔toPath fwd bwd
where
fwd : ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩ → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩
正向消去内部见证的截断并把见证映射过去；反向正是见证原理发挥作用之处：把外部满足交给见证原理，它返回一个内部点，其像满足矩阵，再由一致把该满足搬回。
fwd = rec₁ ((map g δ ⊨ᴮ mapFo g (∃̇ ψ)) .snd)
(λ { (q , hq) → ∣ g q , subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hq ∣₁ })
bwd : ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩ → ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩
bwd h = map₁ (λ { (q , hq) →
q , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) hq }) (wit n ψ δ h)
全称子句是经典的一支：其正向假设每个内部点都满足矩阵，固定外部点 x，并须证明 x 在像中满足矩阵。证明从双否消去开始，这正是排中律进入移送之处。
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 处满足否定矩阵；对该否定施加见证原理，返回一个内部点，其像满足否定，而该内部点处的一致便反驳「每个内部点都满足矩阵」的假设。
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 ∷ δ) ⊨ᴬ ψ ⟩
反向是直接的，因为每个内部点都映入外部载体。有界全称随之以一条辅助公式开场：它把边条件，即属于改名后的界，与矩阵的否定合取；辅助公式的满足正是「在界内但矩阵不成立」的经典读法。
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) ∧̇ ¬̇ ψ
正向陈述：若界内的每个内部点都满足矩阵，则每个属于映射后界的外部点都满足映射后的矩阵。证明再次从双否消去开始：假设该外部点失败。
fwd : ((q : SA) → ⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
→ (x : SB) → ⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
→ ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
fwd h x hx =
dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
见证原理被施加于辅助公式，返回内部点 q：其像落在界内却反驳矩阵。像在界内的成员关系经弱化与 memPath 搬回，一致再把内部对矩阵的满足提升到其像处，与失败相矛盾。
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
辅助应用以见证记录收尾，其第二分量是矩阵在像处的失败，即否定矩阵。反向陈述：像处的外部满足加上内部边条件，即得内部对矩阵的满足。
, (λ yes → lift (nx yes))) ∣₁)
bwd : ((x : SB) → ⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
→ ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
→ (q : SA) → ⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
bwd h q hq =
反向在内点的像处施加外部满足，边条件经 memPath、矩阵经一致搬运。有界存在随之以其辅助矩阵开场：它合取边条件与矩阵本身。
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)
辅助矩阵即边条件与矩阵的合取；正向陈述：内部见证对映射为外部见证对。证明只是对截断的一次映射。
mat = (var zero ∈̇ renameTm suc t) ∧̇ ψ
fwd : ∥ Σ[ q ∶ SA ] (⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
→ ∥ Σ[ x ∶ SB ] (⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
× ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
fwd = map₁ (λ { (q , hq , hψ) →
两个分量分别搬运：边条件经 memPath，矩阵经一致。反向陈述其逆：外部见证对给出内部见证对。
g q , (subst ⟨_⟩ (memPath t q δ) hq ,
subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hψ) })
bwd : ∥ Σ[ x ∶ SB ] (⟨ x .fst ∈ˢ (⟦ mapTm g t ⟧ᴮ (map g δ)) .fst ⟩
× ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
→ ∥ Σ[ q ∶ SA ] (⟨ q .fst ∈ˢ (⟦ t ⟧ᴬ δ) .fst ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
反向对以辅助形式读取的外部对运行见证原理，得到内点及其像处的对；两个分量再分别经弱化与 memPath、经一致搬回。
bwd h = 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 δ (map₁ (λ { (x , hx , hψ) →
两个分量闭合有界存在的移送，十条子句的归纳随之完成。
x , (subst ⟨_⟩ (sym (memRen t x δ)) hx , hψ) }) h))
层内部的 Tarski-Vaught 判据
对序数指数 α，层 Lset α 给出外围结构，上述移送将在其中证明初等性。
module AtStage (α : S) (ordα : IsOrd α) where
层是传递的，理由很精确：Lset-layer α 证明 α 处的层传递，layer-trans 由此给出 Lset α 的传递性。序数性假设在此并未使用，而是留给下文的良序。
Ltr : isTransV (Lset α)
Ltr = layer-trans (Lset-layer α)
传递性保证有界公式在 Lset α 内部与全集中绝对一致。因此，层上的受限结构可作为 Tarski-Vaught 论证的外部语义。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ Lset α) Ltr
using ( SM; 𝒮M; _⊨ᵐ_; ⟦_⟧ᵐ; abs₀ )
层载体是属于 Lset α 的元素的类型；下文的每个壳元素与每次层读取都居于该类型。
SL : Type (ℓ-suc ℓ)
SL = AbsL.SM
前一章的层序限制为该载体上的良序。固定一个包含于该层的载体 M；它到该层的包含是所取假设的一部分。
wL : SWO SL
wL = orderAt α ordα
module AtM (M : S) (M⊆L : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ x ∈ˢ Lset α ⟩) where
子结构的载体是外围载体中的元素连同其属于 M 的证明；公式只在这种对上读取。
SM : Type (ℓ-suc ℓ)
SM = Σ[ x ∶ S ] ⟨ x ∈ˢ M ⟩
子结构的语义是外围语义在 M 上的限制：项在限制内部求值，满足取值于命题。
module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
using ( module At )
open SemM.At SM id renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
到层的包含把载体的每个元素与其层成员关系配对，后者由包含假设供给。
inL : SM → SL
inL c = c .fst , M⊆L (c .fst) (c .snd)
初等性陈述：对该载体的每条公式与每个环境，满足在包含下不变。它是命题间的路径，两条原子同余与见证原理正是以这种形式与它复合。
Elementary : Type (ℓ-suc (ℓ-suc ℓ))
Elementary = (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ (δ ⊨ᵐ φ) ≡ (map inL δ AbsL.⊨ᵐ (mapFo inL φ))
Tarski-Vaught 判据是初等性的见证形式：每当层在某个环境的像处满足一个存在式，就有载体的某个元素，其像在该处满足矩阵。由满足的命题值性，仅仅存在即可。
TarskiVaught : Type (ℓ-suc ℓ)
TarskiVaught = (n : ℕ) (φ : Formula SM (suc n)) (δ : Vec SM n)
→ ⟨ map inL δ AbsL.⊨ᵐ (mapFo inL (∃̇ φ)) ⟩
→ ∥ Σ[ q ∶ SM ] ⟨ (inL q ∷ map inL δ) AbsL.⊨ᵐ (mapFo inL φ) ⟩ ∥₁
逐点包含与环境查找可交换；这正是项的一致性所需的变元情形。
private
lookup-inL : {n : ℕ} (i : Fin n) (δ : Vec SM n)
→ lookup i (map inL δ) ≡ inL (lookup i δ)
lookup-inL zero (c ∷ δ) = refl
lookup-inL (suc i) (c ∷ δ) = lookup-inL i δ
项在包含两侧一致：载体的项无论在子结构中读取，还是映射后在层中读取，都求得同一底层元素。常元固定，变元随查找而定。移送机制随即在两个成员关系谓词处实例化。
tm-agree : (n : ℕ) (t : Term SM n) (δ : Vec SM n)
→ (⟦ t ⟧ᵐ δ) .fst ≡ (AbsL.⟦ mapTm inL t ⟧ᵐ (map inL δ)) .fst
tm-agree n (con c) δ = refl
tm-agree n (var i) δ = sym (cong (λ p → p .fst) (lookup-inL i δ))
module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ Lset α)
初等性由共享归纳实例化而来：两个原子情形由刚证得的满足关系合同性给出，见证原理恰是 Tarski-Vaught 实例，而布尔与量词子句由共享主体搬运。除这两条同余与该判据外，不使用任何关于层的特殊性质。
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 α，因为 ∅ 位于序数 α 中，且在基层有编码。
module Hull (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
(∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
∅∈Lsetα : ⟨ ∅ ∈ˢ Lset α ⟩
∅∈Lsetα = Lset-in α ∅ ∅ ∅∈α (∅∈𝒟ₒ ∅)
起始集合呈现的嵌入落入层载体：每个索引指名 X 的一个元素，包含假设证明该元素属于层 Lset α。
inStg : ⟪ X ⟫ → SL
inStg m = ⟪ X ⟫↪ m , X⊆L (⟪ X ⟫↪ m) (member X m)
项代数在层的受限结构处实例化：其载体经第一投影映入宇宙，见证搜索使用层的良序，垃圾值取空集，基码以 X 的呈现为索引。壳就此在层内生长。
module T = TermAlgebra AbsL.𝒮M (λ p → p .fst) wL (∅ , ∅∈Lsetα) {K = ⟪ X ⟫} inStg
open T using ( Code; base; val; Hull; inHull )
壳位于层内：每个元素都是某个码的取值，而码的取值依项代数自身的类型都属于层 Lset α。证明消去截断的呈现，并沿该同一视搬运。
Hull⊆L : (x : S) → ⟨ x ∈ˢ Hull ⟩ → ⟨ x ∈ˢ Lset α ⟩
Hull⊆L x x∈H = rec₁ ((x ∈ˢ Lset α) .snd) go x∈H
where
go : Σ[ c ∶ Code ] ((val c) .fst ≡ x) → ⟨ x ∈ˢ Lset α ⟩
go (c , q) = subst (λ z → ⟨ z ∈ˢ Lset α ⟩) q ((val c) .snd)
成员关系只能读回为截断的存在：壳的元素是某个码的取值，但没有选定哪个码。这是呈现的诚实形式，因为不同码可能求值相同。
hull-member : (x : S) → ⟨ x ∈ˢ Hull ⟩
→ ∥ Σ[ c ∶ Code ] ((val c) .fst ≡ x) ∥₁
hull-member x x∈H = x∈H
另一方向无需截断：由呈现自身的引入规则，每个码的取值都是元素。
val-in-Hull : (c : Code) → ⟨ (val c) .fst ∈ˢ Hull ⟩
val-in-Hull c = inHull c
起始集合逐元素进入壳。X 的元素 x 由一个索引呈现，呈现它在 x 处的纤维返回该索引。
module XInM (x : S) (x∈X : ⟨ x ∈ˢ X ⟩) where
mx : ⟪ X ⟫
mx = fiber X x∈X .fst
纤维携带被呈现元素与 x 的同一视，这正是沿之搬运成员关系的通道。
x≡val : ⟪ X ⟫↪ mx ≡ x
x≡val = fiber X x∈X .snd
该索引处的基码求值为被呈现元素，即 x；搬运把 x 在壳中的成员关系落定。
inM : ⟨ x ∈ˢ Hull ⟩
inM = subst (λ z → ⟨ z ∈ˢ Hull ⟩) x≡val (inHull (base mx))
组装一次后，起始集合含于壳即成单条引理。
X⊆M : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Hull ⟩
X⊆M x x∈X = XInM.inM x x∈X
满足关系在塌缩同构下不变
为比较同构前后的满足关系，固定集合 M、PM，以及把 M 的元素映到 PM 的元素的载体映射 p。
module IsoInv (M : S) (PM : S)
(p : S → S)
(p∈ : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ p x ∈ˢ PM ⟩)
(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 x ≡ p y → x ≡ y)
(surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
→ ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ M ⟩ × (p y ≡ z)) ∥₁)
where
除封闭条件 p∈ 外，映射 p 还满足四条假设。iso-fwd 保持成员关系，iso-bwd 反映成员关系，最后两个参数陈述 M 上的单射性与到目标 PM 上的满射性。
映射 p 在 M 上单射，且仅仅地满射到 PM。与保持、反映合在一起，这恰是两个结构之间成员关系同构的全部数据。
源载体把 M 的每个元素与其成员关系证明配对，与本章各受限结构相同。
SM : Type (ℓ-suc ℓ)
SM = Σ[ x ∶ S ] ⟨ x ∈ˢ M ⟩
目标载体把 PM 的每个元素与其成员关系证明配对。
SPM : Type (ℓ-suc ℓ)
SPM = Σ[ x ∶ S ] ⟨ x ∈ˢ PM ⟩
同构提升到配对载体：对底层元素施加 p，并证明其在像中的成员关系。
g : SM → SPM
g m = p (m .fst) , p∈ (m .fst) (m .snd)
源语义在限制于 M 的结构中解释项与公式。
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 的结构中解释映射后的项与公式。
open module Pse = SemPM.At SPM id public renaming ( _⊨_ to _⊨ᵖᵐ_ ; ⟦_⟧ to ⟦_⟧ᵖᵐ )
满射提升到配对载体：目标 PM 的每个元素都是 M 中某点的像，而底层元素的相等因属于 PM 是命题而提升为对的相等。
surj' : (p' : SPM) → ∥ Σ[ q ∶ SM ] (g q ≡ p') ∥₁
surj' (z , z∈) = map₁ (λ { (y , y∈ , e) →
(y , y∈) , Σ≡Prop (λ w → ⟨ w ∈ˢ PM ⟩isProp) e }) (surj z z∈)
一般的满足关系移送定理现可施用于属于 M 与属于 PM 的谓词；成员关系的保持与反映给出其成员关系原子情形。
module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ PM)
映射 p 逐索引地作用于环境，因此查找一次一格化归。
private
lookup-g : {n : ℕ} (i : Fin n) (δ : Vec SM n)
→ p ((lookup i δ) .fst) ≡ (lookup i (map g δ)) .fst
lookup-g zero (m ∷ δ) = refl
lookup-g (suc i) (m ∷ δ) = lookup-g i δ
项在映射 p 下相一致：对 M 的项的值施加 p，等于在映射环境处求值映射后的项。常元固定，变元随查找而定。成员关系原子由此可陈述。
tm-agree : {n : ℕ} (t : Term SM n) (δ : Vec SM n)
→ p ((⟦ t ⟧ᵐ δ) .fst) ≡ (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) .fst
tm-agree (con m) δ = refl
tm-agree (var i) δ = lookup-g i δ
at∈ : (n : ℕ) (t u : Term SM n) (δ : Vec SM n)
原子项的成员关系双向转移：正向把内部成员关系沿项等式搬运，再施加保持成员关系的 iso-fwd。
→ (δ ⊨ᵐ (t ∈̇ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ∈̇ u))
at∈ n t u δ = ⇔toPath
(λ h → subst (λ z → ⟨ (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) .fst ∈ˢ z ⟩) (tm-agree u δ)
(subst (λ z → ⟨ z ∈ˢ p ((⟦ u ⟧ᵐ δ) .fst) ⟩) (tm-agree t δ)
(iso-fwd ((⟦ u ⟧ᵐ δ) .fst) ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .snd)
正向搬运落在施加 p 后的成员关系上；反向经由同构反映该成员关系，沿项等式恢复内部的成员关系。
((⟦ t ⟧ᵐ δ) .snd) h)))
(λ h → iso-bwd ((⟦ u ⟧ᵐ δ) .fst) ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .snd)
((⟦ t ⟧ᵐ δ) .snd)
(subst (λ z → ⟨ p ((⟦ t ⟧ᵐ δ) .fst) ∈ˢ z ⟩) (sym (tm-agree u δ))
(subst (λ z → ⟨ z ∈ˢ (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) .fst ⟩)
反向闭合成员关系子句：经同构、循项同余的反映，恰好返回内部的成员关系。相等原子与见证原理由其余假设处理。
(sym (tm-agree t δ)) h)))
原子项的等式通过把塌缩施加于等式两侧而转移。正向取 M 中值的等式，经 cong 施加 p，再由项同约把两侧分别搬运到映射后的项。
at≐ : (n : ℕ) (t u : Term SM n) (δ : Vec SM n)
→ (δ ⊨ᵐ (t ≐ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ≐ u))
at≐ n t u δ = ⇔toPath
(λ h → subst (λ z → z ≡ (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) .fst) (tm-agree t δ)
(subst (λ z → p ((⟦ t ⟧ᵐ δ) .fst) ≡ z) (tm-agree u δ) (cong p h)))
反向正是单射性发挥作用之处：塌缩后的两侧相等，p-inj 由此恢复原值的相等。两个方向合起来，把相等原子变成命题之间的路径。
(λ h → p-inj ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .fst) ((⟦ t ⟧ᵐ δ) .snd)
((⟦ u ⟧ᵐ δ) .snd)
(subst (λ z → z ≡ p ((⟦ u ⟧ᵐ δ) .fst)) (sym (tm-agree t δ))
(subst (λ z → (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) .fst ≡ z)
(sym (tm-agree u δ)) h)))
见证原理由满射产出。像中的外部见证 p' 仅仅是 M 中某个 q 的塌缩；沿该同一视搬运满足，即得内部见证及其在像中的满足。
wit : Tr.Witness g
wit n ψ δ h = rec₁ squash₁
(λ { (p' , hp) → map₁
(λ { (q , gq≡p) →
q , subst (λ z → ⟨ (z ∷ map g δ) ⊨ᵖᵐ mapFo g ψ ⟩) (sym gq≡p) hp })
满射引理供给原像，两次搬运复合成移送的见证原理。
(surj' p') }) h
原子情形与见证原理就位后，共享归纳证明：环境沿塌缩映射、常元沿 g 重标记时，满足关系保持不变。
agree : (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ (δ ⊨ᵐ φ) ≡ (map g δ ⊨ᵖᵐ mapFo g φ)
agree = Tr.Along.agree g at∈ at≐ wit
一致性以两个单向形式记录备用。正向：内部的满足给出映射环境上映射公式的满足。
iso-inv : (n : ℕ) (φ : Formula SM n) (δ : Vec SM n)
→ ⟨ δ ⊨ᵐ φ ⟩ → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩
iso-inv n φ δ = subst ⟨_⟩ (agree n φ δ)
反向把外部的满足送回内部的满足。随后本章在有外延性的集合 X 的塌缩处实例化这一不变性，打开塌缩及其成员关系同构与单射性。
iso-inv-bwd : (n : ℕ) (φ : Formula SM n) (δ : Vec 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 上成员关系与塌缩像上成员关系之间的同构随即可用。
module CI = C.InjExt Xext using ( iso; π-inj )
PM : S
PM = C.πX
映射 p 把每个集合送到其 Mostowski 塌缩值。
p : S → S
p = C.π
X 的元素落入像中，这由塌缩对像自身的引入规则给出。
p∈ : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ p x ∈ˢ PM ⟩
p∈ = C.πX-intro
成员关系沿塌缩正向保持：若在 X 中 y 属于 x，则 y 的塌缩属于 x 的塌缩。这是成员关系同构的第一个分量。
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 中真实的成员关系。两个方向合起来说明塌缩对成员关系是忠实的。
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 上单射：塌缩相等的两个元素相等。对成员关系的忠实加上单射性，构成元素层面同构的两半。
p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
→ p x ≡ p y → x ≡ y
p-inj = CI.π-inj
像的每点都来自 X 的元素：满射是截断的，只主张原像存在而不选定它，这正是见证原理所消耗的形式。
surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
→ ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (p y ≡ z)) ∥₁
surj = C.πX-member
对外延集合 X，塌缩保持并反映成员关系，在 X 上单射，且覆盖 πX 的每个点。
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 上的结构之间双向搬运。
module HullElemDown (α : S) (ordα : IsOrd α)
(X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩) (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
把这一点用于 Lset α 内的 Skolem 壳，初等性便归结为 Tarski-Vaught 见证条件。
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
子结构机制在壳处实例化，其公式获得一个外围读法。壳载体的每个元素都有码：码由截断的呈现给出存在，而「取值等于包含」的同一视借层成员关系的命题值性提升。
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 = map₁ (λ { (c , e) → c , Σ≡Prop (λ z → ⟨ z ∈ˢ Lset α ⟩isProp) e })
(H.hull-member (q .fst) (q .snd))
码从单个元素提升到有限环境：空环境由空向量编码，递归情形把一个新码与已建好的码并列。
codeEnv : {n : ℕ} (δ : Vec A.SM n)
→ ∥ Σ[ ds ∶ Vec H.T.Code n ]
(map H.T.val ds ≡ map A.inL δ) ∥₁
codeEnv [] = ∣ [] , refl ∣₁
codeEnv (q ∷ δ) = map2
添入情形把两个截断存在复合成一个：加长后的码向量求值恰为包含后的环境。
(λ { (c , ec) (ds , eds) → c ∷ ds , cong₂ _∷_ ec eds })
(codeOf q) (codeEnv δ)
逐分量映射还保持有限环境的拼接。因此，自由变元的取值与替代常元出现的取值可以合并为一个供 Tarski-Vaught 论证使用的编码环境。
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 条件本身：若层在包含后的环境处满足一个存在式，则仅仅地有壳中某元素在该处满足矩阵。证明先消去环境的编码，再进入搜索闭合。
→ ⟨ 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 = rec₁ squash₁ takeEnvironment (codeEnv params)
where
参数抽象把每个常元出现替换为一个额外自由变元。所得公式的常元域为空，元数增加 countFo ψ，同时保留 ψ 的完整逻辑结构。
bodyFo : Formula (⊥* {ℓ}) (suc (n + countFo ψ))
bodyFo = absFo ψ
抽象后矩阵的环境是原环境后接诸常数出现：抽象把常数变成额外的自由变元，因此一个向量就携带搜索所需的一切。
params : Vec A.SM (n + countFo ψ)
params = δ ++ constantsFo ψ
一旦这个合并环境有了码，最小见证闭合便给出壳中的见证。再利用抽象公式与原带参公式之间的语义同一视，即得所需的 Tarski-Vaught 见证。
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 ψ) ⟩ ∥₁
搜索闭合在编码环境处运行。其自身的求值记录随后与编码等式、以及包含对拼接的分配复合，得到「码的求值即包含后的参数」。
takeEnvironment (ds , eds) = 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 ψ)
关键的同一视陈述：抽象矩阵在「编码环境处的裸搜索语义」下的读法，与它在「包含环境处的层语义」下的读法是同一命题。
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 把重标记联系到映射后的环境。
∙ sym (⊨-abs ASt.AbsL.𝒮M A.inL ψ
(b ∷ map A.inL δ))
∙ sym (⊨-map ASt.AbsL.𝒮M A.inL id ψ
(b ∷ map A.inL δ))
层对存在式的满足沿体路径搬运进裸读法，产出恰是搜索闭合所需的可满足性见证。
witness : H.T.Sat (n + countFo ψ) bodyFo (H.T.vals ds)
witness = map₁ (λ { (b , hb) →
b , subst ⟨_⟩ (sym (body-path b)) hb }) h
搜索返回壳内满足抽象矩阵的最小见证，其在编码环境处成立。转换须把它变成原公式的 Tarski-Vaught 对。
finish : Σ[ a ∶ ASt.SL ]
( ⟨ a .fst ∈ˢ M ⟩
× ⟨ (a ∷ H.T.vals ds) H.T.⊨₀ bodyFo ⟩ )
→ Σ[ q ∶ A.SM ]
⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
见证被读回子结构的载体：底层集合即壳，成员关系即刚产出者。
finish (a , a∈H , ha) = q , sat
where
q : A.SM
q = a .fst , a∈H
见证到层的包含就是见证本身：两个载体只差命题值性的成员关系证明，而它由自反性等同。
q≡a : A.inL q ≡ a
q≡a = Σ≡Prop (λ z → ⟨ z ∈ˢ Lset α ⟩isProp) refl
见证处本体的满足沿体路径搬入层语义，再沿见证的同一视搬入子结构载体；这恰是原公式与原环境的 Tarski-Vaught 结论。
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 α 中的初等性。
elem : A.Elementary
elem = A.TV→elem tv
在外围宇宙中读取无参公式
对于常元域为空的公式，外围满足关系的比较不涉及任何非平凡的常元重标记。
module AtP = SemV.At (⊥* {ℓ-suc ℓ}) (λ b → ⊥*-rec b) using ( _⊨_ )
无参公式的外围满足被命名备用；关键观察是：改名无参公式不改变它，因为无可重映射的常数。
_⊨ₚ_ : {n : ℕ} → Vec 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 φ
证明复合映射法则与「空域嵌入在出现上是恒等」的事实：改名无可移动之物。
embed-map f φ =
mapFo-comp ⊥*-rec f φ
∙ cong (λ h → mapFo h φ) (funExt (λ b → ⊥*-rec b))
opaque
isOrdAt : Formula (⊥* {ℓ-suc ℓ}) 1
序数性由一个单空位有界公式表达：参数本身传递，且参数的每个元素也传递。
isOrdAt =
(∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
∧̇ (∀̇∈ (var zero) (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
Δ₀ 证书先穿过外层合取，再分别穿过第一子句的两个与第二子句的三个有界量词，最终落到成员关系原子。
Δ₀-isOrdAt : Δ₀ isOrdAt
Δ₀-isOrdAt =
δ-∧ (δ-∀∈ (δ-∀∈ δ-∈))
(δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
两个读取引理在两个方向上把 isOrdAt 的满足精确等同于序数谓词。
module Amb where
opaque
unfolding isOrdAt
从公式读出序数性，即把两条有界子句拆成序数谓词的两个字段：参数的传递性，以及每个元素的传递性。
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 的两个字段满足这两个有界子句。三空位伴随公式在中间的自由空位表达同一谓词；另外两个自由空位并未出现于公式中。
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
三空位公式的第一个合取支说：参数的元素的元素都是参数的元素，即在第二空位处读取的传递性。
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。
(∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
其有界性证书循同样的递归。随后消去引理开始：对无常数出现的公式，消去常数保持 Δ₀ 证书，逐子句成立。
Δ₀-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 δ-∈ = δ-∈
原子原样通过，命题联结词按结构递归，因为消去是结构性施加的。
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 δ-⊥ = δ-⊥
有界量词情形递归处理其矩阵。
erase-Δ₀ (∀̇∈ t φ) p (δ-∀∈ c) = δ-∀∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇∈ t φ) p (δ-∃∈ c) = δ-∃∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇ φ) p ()
erase-Δ₀ (∀̇ φ) p ()
凝聚所需的壳数据
module HullStage (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 ⟩) where
框架收取：一个其指数容纳元素后继的层、包含于该层的起始集合，以及空集属于该指数。
在 Lset lam 内，起始集合生成 Skolem 壳 M。M 的每个元素仍属于该层。
module ASt = AtStage lam ordλ
using ( module AbsL; module AtM; module Hull; Ltr; SL; wL )
原集合与作为回退值的空集都在壳构造中得到呈现。
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 塌缩构成论证的数据。
M : S
M = H.T.Hull
对壳 M，令 π 为其 Mostowski 塌缩，πX 为塌缩像。每个塌缩后的壳中点都属于 πX，πX 的每个元素都来自壳中的一点，并且 πX 是传递的。此外，塌缩固定壳中的每个传递点。
module C = Collapse M
using ( module InjExt; π; πX; πX-intro; πX-member; πX-trans; fixes )
凝聚论证对塌缩像作两项假设。第一，若序数 δ 属于该像，则层 Lset δ 也属于该像。第二，每个壳元素的塌缩都属于某个层，而该层的序数指数属于塌缩像。这两项闭合与覆盖性质将把塌缩像认同为 L 的一个层。
module Condense
(levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ C.πX ⟩ → ⟨ Lset δ ∈ˢ C.πX ⟩)
(cover : (y : S) → ⟨ y ∈ˢ M ⟩
→ ∥ Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ C.π y ∈ˢ Lset γ ⟩) ∥₁)
where
分离构造出恰由 πX 中序数组成的集合。因此 β 记录塌缩像的序数部分。其分离谓词正是那条陈述序数性的有界公式，凭 Δ₀ 证书在每个环境处都是小的。
β-sep : Σ[ s ∶ S ]
(∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt)))
β-sep = separateFromSmall C.πX (λ y → (y ∷ []) ⊨ₚ isOrdAt)
(λ y → D0.Δ₀-small Δ₀-isOrdAt (y ∷ []))
我们把这个序数部分记为 β；下面证明它本身是序数，并且它所索引的层恰为塌缩像。
β : S
β = β-sep .fst
属于 β，等价于属于 πX，并且把该元素赋给自由变元后满足无常元的序数公式。
β-spec : (y : S) → (y ∈ˢ β) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt))
β-spec = β-sep .snd
定义等价的第一个投影表明：beta 的每个元素都是塌缩像的元素。
β∈πX : (δ : S) → ⟨ δ ∈ˢ β ⟩ → ⟨ δ ∈ˢ C.πX ⟩
β∈πX δ δ∈β = subst ⟨_⟩ (β-spec δ) δ∈β .fst
第二个分量把这条无常元一自由变元公式的满足转换为外围宇宙中的序数性。
β-ord : (δ : S) → ⟨ δ ∈ˢ β ⟩ → IsOrd δ
β-ord δ δ∈β = Amb.isOrdAt-out δ (subst ⟨_⟩ (β-spec δ) δ∈β .snd)
反之，塌缩像的序数落入 beta：成员关系与序数性两个定义分量一并提供，定义等价再把它们送回 beta 内部。
ord∈β : (δ : S) → ⟨ δ ∈ˢ C.πX ⟩ → IsOrd δ → ⟨ δ ∈ˢ β ⟩
ord∈β δ δ∈πX oδ = subst ⟨_⟩ (sym (β-spec δ)) (δ∈πX , Amb.isOrdAt-in δ oδ)
为证明 β 是序数，需要验证其两项定义条件。第一项是传递性：每当 z ∈ x ∈ β，都须有 z ∈ β。
β-isOrd : IsOrd β
β-isOrd = β-trans , β-mem
where
β-trans : isTransV β
β-trans {x = x} {y = z} z∈x x∈β =
传递性在中间成员关系处使用塌缩像的传递性，并从外围公式读取中间点的序数性；第二字段随之成立，因为 beta 的每个元素都是序数，故传递。
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
覆盖假设从壳元素提升到塌缩元素。由于塌缩元素仅仅是某个壳元素的塌缩，该壳元素的覆盖沿此同一视搬运。
covered : (x : S) → ⟨ x ∈ˢ C.πX ⟩
→ ∥ Σ[ γ ∶ S ]
(IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
covered x x∈πX = rec₁ squash₁ go (C.πX-member x x∈πX)
where
该求逆正是塌缩自身的元素描述：像的元素仅仅是某个壳元素的塌缩。
go : Σ[ y ∶ S ] (⟨ y ∈ˢ M ⟩ × (C.π y ≡ x))
→ ∥ Σ[ γ ∶ S ]
(IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
go (y , y∈M , e) = map₁
(λ { (γ , oγ , γ∈πX , h) →
覆盖沿塌缩值的相等搬运。提升后的命题随即被直接使用：beta 的每个序数都位于 beta 中更大的序数之内，这就是凝聚论证的经典极限层步骤。
γ , oγ , γ∈πX , subst (λ w → ⟨ w ∈ˢ Lset γ ⟩) e h })
(cover y y∈M)
β-succ : (δ : S) → ⟨ δ ∈ˢ β ⟩
→ ∥ Σ[ γ ∶ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩) ∥₁
β-succ δ δ∈β = map₁ go (covered δ (β∈πX δ δ∈β))
delta 的序数性从 beta 读出；转换把覆盖结论改写为成员关系形式：包含 delta 的层可取其指数落在 beta 内。
where
oδ : IsOrd δ
oδ = β-ord δ δ∈β
go : Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ δ ∈ˢ Lset γ ⟩)
→ Σ[ γ ∶ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
由于 δ 与 γ 都是序数，δ ∈ Lset γ 推出 δ ∈ γ；又因 γ 是 πX 中的序数，所以 γ ∈ β。随后陈述反向包含：塌缩的每个元素都属于 beta 处的层。
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 = rec₁ ((x ∈ˢ Lset β) .snd) go (covered x x∈πX)
where
反向包含成立，因为 beta 处的层包含所有更小的层：层构造的单调性把覆盖层搬入 beta 之内。
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 内更大的序数。
Lβ⊆πX x x∈Lβ = rec₁ ((x ∈ˢ C.πX) .snd) go (Lset-out β x x∈Lβ)
where
go : Σ[ δ ∶ S ] (⟨ δ ∈ˢ β ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
→ ⟨ x ∈ˢ C.πX ⟩
go (δ , δ∈β , x∈𝒟ₒδ) = rec₁ ((x ∈ˢ C.πX) .snd) liftStage (β-succ δ δ∈β)
陈述提升层：从 beta 内包含 delta 的序数，产出 x 在塌缩中的成员关系。
where
liftStage : Σ[ γ ∶ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
→ ⟨ x ∈ˢ C.πX ⟩
liftStage (γ , oγ , δ∈γ , γ∈β) =
C.πX-trans {x = Lset γ} {y = x}
提升复合两条闭合：由于 x 定义在 gamma 之下的 delta 处，gamma 的层包含 x；又由第一条假设，塌缩像包含 gamma 处的层。两条包含随即在宇宙的外延性处会合。
(Lset-in γ δ x δ∈γ x∈𝒟ₒδ)
(levelIn γ oγ (β∈πX γ γ∈β))
ext : C.πX ≡ Lset β
ext = extensionality C.πX (Lset β) (sub , sup)
where
外延性论证的前一半让每个元素经桥进入层读法，应用反向包含，再经桥返回。
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 处的层。
(Lβ⊆πX x (∈∈ₛ {a = x} {b = Lset β} .snd x∈ₛLβ))
凝聚陈述就此成立：塌缩像等于序数 β 所索引的层。为作应用，取层 Lset α 与额外一点 x 的并集为起始集，并假设 α ∈ lam、x ⊆ Lset α 以及 x ∈ Lset lam。
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 ⟩) (α∉ω : ⟨ α ∈ˢ ω ⟩ → ⊥₀) where
起始集合是 Lset α 与单点集 {x} 的并集；单点集的分类给出 x ∈ {x}。
X : S
X = Lset α ∪ ⁅ x ⁆s
x∈sgl : ⟨ x ∈ₛ ⁅ x ⁆s ⟩
x∈sgl = SetPackage.classification (SingletonPackage x) x .snd refl
额外点经并集的右侧属于起始集合。
x∈X : ⟨ x ∈ˢ X ⟩
x∈X = cup-inr (Lset α) ⁅ x ⁆s x (∈∈ₛ {a = x} {b = ⁅ x ⁆s} .snd x∈sgl)
层的每个元素经左侧属于起始集合。
Lα∈X : (z : S) → ⟨ z ∈ˢ Lset α ⟩ → ⟨ z ∈ˢ X ⟩
Lα∈X = cup-inl (Lset α) ⁅ x ⁆s
sgl≡ : (z : S) → ⟨ z ∈ˢ ⁅ x ⁆s ⟩ → z ≡ x
sgl≡ = sgl-out x
因此，属于起始集分成两种情形：该点或者属于 Lset α，或者属于单点集 {x}。
X-mem : (z : S) → ⟨ z ∈ˢ X ⟩
→ ⟨ (z ∈ˢ Lset α) ⊔ (z ∈ˢ ⁅ x ⁆s) ⟩
X-mem = cup-out (Lset α) ⁅ x ⁆s
生成集包含于外围层：层一侧的元素沿指数包含、由层构造的单调性搬运。
X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
X⊆Lλ z z∈X = rec₁ ((z ∈ˢ Lset lam) .snd) 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α
单点一侧的元素化归为额外点，而额外点的层成员关系本是假设。
go (inr z∈sgl) = subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym (sgl≡ z z∈sgl)) x∈Lλ
生成集是传递的。若元素的元素位于层一侧，则由层的传递性它属于层，再由左包含把它放入生成集。
Xtr : isTransV X
Xtr {x = a} {y = b} b∈a a∈X = rec₁ ((b ∈ˢ X) .snd) 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 α 随即把它的每个元素放入并集的左侧。
go (inr a∈sgl) = Lα∈X b (x⊆Lα b
(subst (λ u → ⟨ b ∈ˢ u ⟩) (sgl≡ a a∈sgl) b∈a))
one∈α : ⟨ sucV ∅ ∈ˢ α ⟩
one∈α = ⊎-rec
(λ α∈ω → ⊥₀-rec (α∉ω α∈ω))
无穷即不属于 ω，序数三分法分拆各情形：属于 ω 与假设矛盾；等于 ω 则由数码一见证成员关系；ω 低于 α 则由传递性把数码一放入 α 之内。
(⊎-rec (λ α≡ω → subst (λ w → ⟨ sucV ∅ ∈ˢ w ⟩) (sym α≡ω) (#∈ω 1))
(λ ω∈α → ordα .fst (#∈ω 1) ω∈α))
(ord-tri α ordα ω ω-ord)
空集出现在第一个后继层，由基层编码沿后继层的描述搬运而来。
∅∈Lset1 : ⟨ ∅ ∈ˢ Lset (sucV ∅) ⟩
∅∈Lset1 = subst (λ w → ⟨ ∅ ∈ˢ w ⟩) (sym (Lset-suc ∅)) (∅∈𝒟ₒ ∅)
单调性先把空集提升到 Lset α，再到 Lset lam。
∅∈Lλ : ⟨ ∅ ∈ˢ Lset lam ⟩
∅∈Lλ = Lset-mono {α = lam} {β = α} α∈λ
(Lset-mono {α = α} {β = sucV ∅} one∈α ∅∈Lset1)
秩刻画随之把它提升为空集属于指数 lam 本身。余下需要证明壳的外延性，这是使其塌缩成为单射所需的最后条件。
∅∈λ : ⟨ ∅ ∈ˢ 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 α ⟩)
(∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
空集属于指数这一假设，保证 Lset α 处的 Skolem 壳具有其项代数所需的默认值。
令 M 为 Lset α 内由 X 生成的 Skolem 壳。它到该层的包含是初等的。为证明限制在 M 上的成员关系具有外延性，我们比较壳中公式与其在该层中的解释。
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 ( _⊨_ )
壳被命名；两集合的对称差在成员关系真值层面陈述：一个点在一侧之中，且可证不在另一侧之中。
M : S
M = H.T.Hull
Different : S → S → S → Type (ℓ-suc ℓ)
Different x y z = (z ∈ᵗ x × (z ∈ᵗ y → ⊥₀))
⊎ (z ∈ᵗ y × (z ∈ᵗ x → ⊥₀))
经典地，不等的集合必有一点位于其对称差中：这一截断存在由排中律判定。
different : (x y : S) → (x ≡ y → ⊥₀) → ∥ Σ[ 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₁
若没有点区分这两个集合，则每个成员关系真值都双向一致，宇宙的外延性将迫使二者相等，与假设矛盾。
go : Dec ⟨ P ⟩ → ⟨ P ⟩
go (yes p) = p
go (no np) = ⊥₀-rec (nxy (extensionalV (λ z → ⇔toPath (fwd z) (bwd z))))
where
fwd : (z : S) → z ∈ᵗ x → z ∈ᵗ y
一致的两个方向各由排中律判定，每个失败的方向都把它的点贡献给对称差。
fwd z zx = decRec (λ zy → zy)
(λ nzy → ⊥₀-rec (np ∣ z , inl (zx , nzy) ∣₁))
(FOL.Semantics.decideMembership 𝒮ᵥ lem z y)
bwd : (z : S) → z ∈ᵗ y → z ∈ᵗ x
bwd z zy = decRec (λ zx → zx)
(λ nzx → ⊥₀-rec (np ∣ z , inr (zy , nzx) ∣₁))
(FOL.Semantics.decideMembership 𝒮ᵥ lem z x)
差公式是析取式 (z ∈ x ∧ z ∉ y) ∨ (z ∈ y ∧ z ∉ x)，两个常元槽分别放入这两个壳元素。
φ : 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
存在公式的满足是截断的，因此区分点也在截断之下返回。在对称差的任一分支中，同一点都见证该公式在层中相应的析取支。
→ ∥ Σ[ 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 = sumMap
在任一分支中，外围成员关系给出肯定合取项，而不成员关系证明被提升为公式语义所需的否定。层的传递性则把区分点放入该层载体。
(λ (zu , nzv) → zu , λ zv → lift (nzv zv))
(λ (zv , nzu) → zv , λ zu → lift (nzu zu))
z∈L : ⟨ z ∈ˢ Lset α ⟩
z∈L = ⊎-rec
(λ (zx , _) → layer-trans (Lset-layer α) zx (H.Hull⊆L u u∈M))
把区分点与其层成员关系配对，便得到层载体中的见证。为证明壳的外延性，先假设壳中每个属于 x 的元素也属于 y。
(λ (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 仍不相等，则其对称差中的一点将导出矛盾。
→ (ag2 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩)
→ (x ≡ y → ⊥₀) → ⊥₀
refute x y x∈M y∈M ag1 ag2 nxy = rec₁ isProp⊥ diff (different x y nxy)
where
xS : A.SM
xS = x , x∈M
yS : A.SM
yS = y , y∈M
反驳消去差点。初等性把层对该存在公式的满足，以差点为见证，转换为壳内对同一存在公式的满足。
diff : Σ[ z ∶ S ] Different x y z → ⊥₀
diff (z , d) = rec₁ isProp⊥ inside h
where
h : ⟨ [] Mse.⊨ (∃̇ (φ xS yS)) ⟩
h = subst ⟨_⟩ (sym (E.elem 0 (∃̇ (φ xS yS)) []))
初等性给出一个满足差公式的壳中见证。消去其截断的析取后，便得到两个非对称成员关系陈述中成立的那个。
(outer x y x∈M y∈M z d)
inside : Σ[ b ∶ A.SM ] ⟨ (b ∷ []) Mse.⊨ φ xS yS ⟩ → ⊥₀
inside (b , q) = rec₁ isProp⊥ cases q
where
cases : (⟨ b .fst ∈ˢ x ⟩ × (⟨ b .fst ∈ˢ y ⟩ → Lift ⊥₀))
无论哪个析取支，都会把见证认作一个壳元素的元素而非另一个的，相应的一致性假设与该否定矛盾。这一矛盾正是壳的外延性所需要的。
⊎ (⟨ b .fst ∈ˢ y ⟩ × (⟨ b .fst ∈ˢ x ⟩ → Lift ⊥₀))
→ ⊥₀
cases (inl (bx , nby)) = lower (nby (ag1 (b .fst) (b .snd) bx))
cases (inr (by , nbx)) = lower (nbx (ag2 (b .fst) (b .snd) by))
壳的外延性由经典反证法证明。由于集合的宇宙是 h-集合，x ≡ y 是命题，排中律因此给出相等或不相等。若 x ≢ y，refute 会在壳中找到一个只属于 x、y 之一的元素，这与两个成员关系一致性前提矛盾；故 x ≡ y。
hullExt : isExt M
hullExt x y x∈M y∈M ag1 ag2 =
decRec (λ p → p) (λ np → ⊥₀-rec (bad np))
(FOL.Semantics.decideEquality 𝒮ᵥ lem x y)
where
bad 消去矛盾分支，完成壳的外延性。
bad : (x ≡ y → ⊥₀) → ⊥₀
bad = refute x y x∈M y∈M ag1 ag2
沿塌缩搬运有界公式
为比较塌缩与外围宇宙，现固定一个传递集 U。无常元的 Δ₀ 公式在 U 的元素处求值时，在 U 上的受限结构与外围结构中具有相同真值。
module Unpack (U : S) (Utr : isTrans U) where
受限载体 SM 的元素由一个集合及其属于 U 的证据组成。把这些二元组逐项投影到第一分量，便得到对应的外围环境；有界绝对性 abs₀ 比较投影前后的满足关系。
module Ab = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ U) Utr using (SM; abs₀; _⊨ᵐ_)
对无常元的 Δ₀ 公式 φ，read 先把 embed φ 看作受限载体上的公式。有界绝对性比较其受限读法与外围读法；embed-⊨ 消去由嵌入引入的改名，空常元域到任意类型的函数唯一性再同一视余下的常元解释。
read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec Ab.SM n)
→ (δ Ab.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
read {n} {φ} dφ δ =
Ab.abs₀ (mapΔ₀ ⊥*-rec dφ) δ
∙ embed-⊨ 𝒮ᵥ {K = Ab.SM} (λ p → p .fst) φ (map (λ p → p .fst) δ)
最后一条路径使用函数外延性：常元域为空，所以两种常元解释逐点相同，因而相等。随后固定 Lset lam 内构造壳所需的数据：对后继封闭的序数 lam，以及起始集合 X ⊆ Lset lam。
∙ cong (λ ι → let module I = SemV.At (⊥* {ℓ-suc ℓ}) ι in map (λ p → p .fst) δ I.⊨ φ)
(funExt (λ b → ⊥*-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 ⟩) where
还假设 ∅ ∈ lam；这是壳构造所需的基础层前提。
令 M 为 Lset lam 内由 X 生成的壳。下文使用它到该层的包含、相应的初等性概念，以及上文证明的外延性。
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 塌缩同一视所需的前提。
Mext : isExt HS.M
Mext = HE.hullExt
搬运论证显式取得包含 M → Lset lam 的初等性。它与 M 的外延性一起给出下文的两种比较：从壳到层，以及从壳到其塌缩。
module Carry (elem : A.Elementary) where
现在要比较三个结构：壳 M、层 Lset lam 与传递塌缩像 πX。塌缩同构联系第一个与第三个结构，有界绝对性则把两个传递集各自联系到外围宇宙。
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)
成员关系由塌缩直接保持：成员关系同构的正向恰是原子成员关系所需的推送。
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 在此层的实例。
atL : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec ASt.SL n)
→ (δ ASt.AbsL.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
atL dφ δ = TL.read dφ δ
塌缩像 πX 也具有传递性，因此无常元 Δ₀ 公式在那里同样具有内外一致的读法。
atπ : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec Tπ.Ab.SM n)
→ (δ Tπ.Ab.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
atπ dφ δ = Tπ.read dφ δ
壳自身载体处的读法经由初等性分解：嵌入公式先在内部读取；由于该公式无常元，改名固定不动；结果再搬运到层读法。
atM : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec A.SM n)
→ (δ CIso.I.⊨ᵐ embed φ) ≡ (map (λ p → p .fst) δ ⊨ₚ φ)
atM {n} {φ} dφ δ =
elem n (embed φ) δ
∙ cong (λ ψ → map A.inL δ ASt.AbsL.⊨ᵐ ψ) (embed-map A.inL φ)
经过层上的绝对性后，只需比较两个环境。把壳元素包含进 Lset lam 不改变其底层集合，因此先包含再投影所得的外围集合向量，等于直接投影原环境所得的向量。
∙ atL dφ (map A.inL δ)
∙ cong (λ γ → γ ⊨ₚ φ) (map-inL-fst δ)
where
map-inL-fst : {m : ℕ} (γ : Vec A.SM m)
→ map (λ p → p .fst) (map A.inL γ) ≡ map (λ p → p .fst) γ
该等式对空环境立即成立，并在环境前添加一个分量时保持。因此，对无常元 Δ₀ 公式，壳元素环境处的外围真值蕴含其塌缩值环境处的外围真值。
map-inL-fst [] = refl
map-inL-fst (q ∷ γ) = cong (q .fst ∷_) (map-inL-fst γ)
push : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec A.SM n)
→ ⟨ map (λ p → p .fst) δ ⊨ₚ φ ⟩
→ ⟨ map (λ p → p .fst) (map CIso.I.g δ) ⊨ₚ φ ⟩
从壳环境处的外围真值出发，先反向使用 atM 得到壳中的内部真值；iso-inv 把它搬到塌缩像，embed-map 消去无内容的常元改名，最后正向使用 atπ 得到塌缩值处的外围真值。
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，恢复原壳环境处的外围真值。
pull : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Vec A.SM n)
→ ⟨ map (λ p → p .fst) (map CIso.I.g δ) ⊨ₚ φ ⟩
→ ⟨ map (λ p → p .fst) δ ⊨ₚ φ ⟩
pull {n} {φ} dφ δ h =
subst ⟨_⟩ (atM dφ δ)
push 与 pull 合起来表明：对每条无常元 Δ₀ 公式及每个由壳元素组成的有限环境，把各分量换成其塌缩值不会改变外围满足。另一个引理 member-push 则直接给出成员关系的相应保持性。
(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)))