构造并塌缩 Skolem 壳

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

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

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

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

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

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

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

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

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

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

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

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 把后继指标处的层认同为前一层的可定义幂集。

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

  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 )

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

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 )

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

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⊥ 使目标为矛盾时可以消去命题截断。存在公式的满足以及呈现集合中的隶属用命题截断表达，因而保留存在性而不选定见证。

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 为索引类型；公式是见证码中的字段，并不自身充当码。构造部分供给空集、并、无序对与单点集构造，以及无穷序数及其后继。

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 hPropStructure 𝒮ᵥ

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

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。项代数随之开始：它以一个结构、把其载体映入外围宇宙的映射，以及该载体上的良序为参数。

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 认同为起始集合的一个呈现。垃圾值只是簿记装置，下文的构造从不检视它。

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

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

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

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

  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 的分量是当前码的直接参数子码，每个子码都可再是基码或见证码。

  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) ⊨₀ ψ ⟩ ∥₁

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

  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

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

  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) = Sum.rec (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))

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

  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)

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

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

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

  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 = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vals cs) ⊨₀ ψ) 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) (δ : SA ^ n)
          → (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
  Witness : (SA → SB) → Type (ℓ-suc ℓ)
  Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : 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) (δ : 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)))

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

    (wit : Witness g) where

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

    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

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

      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)

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

                → 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) (δ : 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) (δ : 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)

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

              → (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 ∷ δ)

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

        ∙ memRen t (g q) δ

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

      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≐。命题联结词逐分量搬运，因为命题上的合取、析取与蕴含都由其分量决定。

    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 = 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 在像中满足矩阵。证明从双否消去开始，这正是排中律进入移送之处。

    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 处满足否定矩阵；对该否定施加见证原理，返回一个内部点，其像满足否定，而该内部点处的一致便反驳「每个内部点都满足矩阵」的假设。

        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 ∷ δ) ⊨ᴬ ψ ⟩

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

      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) → ⟨ 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 搬回，一致再把内部对矩阵的满足提升到其像处，与失败相矛盾。

        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

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

            , (λ 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、矩阵经一致搬运。有界存在随之以其辅助矩阵开场：它合取边条件与矩阵本身。

        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 ] (⟨ 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，矩阵经一致。反向陈述其逆：外部见证对给出内部见证对。

        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、经一致搬回。

      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ψ) →

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

          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 = fst c , M⊆L (fst c) (snd c)

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

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

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

    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 φ) ⟩ ∥₁

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

    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 δ

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

      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 实例，而布尔与量词子句由共享主体搬运。除这两条同余与该判据外，不使用任何关于层的特殊性质。

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

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

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

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

    val-in-Hull : (c : Code) → ⟨ fst (val c) ∈ˢ 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 ⟩)

除封闭条件 p∈ 外，映射 p 还满足四条假设。iso-fwd 保持隶属，iso-bwd 反映隶属，最后两个参数陈述 M 上的单射性与到目标 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 在 M 上单射，且仅仅地满射到 PM。与保持、反映合在一起，这恰是两个结构之间隶属同构的全部数据。

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

源载体把 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 (fst m) , p∈ (fst m) (snd m)

源语义在限制于 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∈) = PT.map (λ { (y , y∈ , e) →
    (y , y∈) , Σ≡Prop (λ w → (w ∈ˢ PM) .snd) e }) (surj z z∈)

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

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

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

  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，等于在映射环境处求值映射后的项。常元固定，变元随查找而定。隶属原子由此可陈述。

    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。

        → (δ ⊨ᵐ (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 后的隶属上；反向经由同构反映该隶属，沿项等式恢复内部的隶属。

            (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 δ)) ⟩)

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

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

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

    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 由此恢复原值的相等。两个方向合起来，把相等原子变成命题之间的路径。

      (λ 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 的塌缩；沿该同一视搬运满足，即得内部见证及其在像中的满足。

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

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

        (surj' p') }) h

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

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

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

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

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

  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 上隶属与塌缩像上隶属之间的同构随即可用。

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

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

  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 = PT.map (λ { (c , e) → c , Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) e })
    (H.hull-member (fst q) (snd q))

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

  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

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

    (λ { (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 = PT.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) = 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 ψ)

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

      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 = PT.map (λ { (b , hb) →
        b , subst ⟨_⟩ (sym (body-path b)) hb }) h

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

      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 ψ) ⟩

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

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

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

        q≡a : A.inL q ≡ a
        q≡a = Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) 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 → Empty.rec* b) using ( _⊨_ )

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

_⊨ₚ_ : {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 φ

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

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

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

  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 ℓ}) 

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

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 φ ≡ )
         → Δ₀ φ → Δ₀ (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