---
title: "累积层级中的小真值"
module: V.Smallness
lang: zh
site: "Bedrock"
description: "累积层级中的小真值"
stage: "环境层级"
reading_order: 21
canonical: https://bedrock.institute/zh/V.Smallness.html
html: V.Smallness.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Smallness.lagda.md
prerequisites: [Base.Prelude, Base.Impredicativity, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy]
routes: [ambient-model]
translations: [https://bedrock.institute/en/V.Smallness.md, https://bedrock.institute/ja/V.Smallness.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 累积层级中的小真值

在累积层级 `V ℓ` 上工作会不断产生形如 `x ∈ˢ a` 或 `a ≈ˢ b` 的陈述：它们是打包成 `hProp (ℓ-suc ℓ)` 元素的命题，比集合自身所在的层级 `ℓ` 高一个宇宙。这样的上宇宙命题不便使用：期望 `ℓ` 层数据的构造，例如库中的分离集合，无法接受它们。于是，若命题 `P : hProp (ℓ-suc ℓ)` 作为证明的类型等价于某个低宇宙命题 `Q : hProp ℓ`，就称它是**小的**。小性不是把 `P` 本身化简，而是一份证书：另一个更低的命题说的恰是同一件事。

本章分阶段把大真值降到小真值。`V` 的原子隶属关系与相等关系直接是小，因为每个集合都配有呈现其成员的小索引类型。小性随后经一切联结词传播，也经有界量词传播，因为后者的量化范围恰是这种索引类型。对无界量词，本章证明了量化范围本身本质小，即等价于层级 `ℓ` 的某个类型时，小性仍然保持。两项成果是：无需命题降级的 Δ₀ 分离，以及载体本质小的限制结构上全体公式真值的小性。

本章的一切都在一个固定的宇宙层级 `ℓ` 上进行，它由模块参数一次性确定。环境对象是 V.Hierarchy 章引入的累积层级 `V ℓ`，其集合是 `Type ℓ` 索引族的像。统摄全章的定义是 `isSmall`：对 `P : hProp (ℓ-suc ℓ)`，`isSmall P` 的元素是一个对子，第一分量是低宇宙命题 `Q : hProp ℓ`，第二分量是底层类型间的等价 `⟨ P ⟩ ≃ ⟨ Q ⟩`。本章的任务就是制造这样的对子。工作环境是 `ZFStructure` record，它把载体与取真值的等词、隶属关系打包在一起；把这样的 record 限制到一个类上的运算 `_↾_` 将在最后一节用到。

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

open import Base.Prelude

module V.Smallness {ℓ : Level} where

open import Base.Impredicativity using ( isSmall )
```

待压低的陈述生活在一阶形式语言中。其关系符号是表示隶属与相等的 `_∈̇_` 与 `_≐_`；联结词组合公式；语言同时具有有界量词 `∀̇∈`、`∃̇∈` 与无界量词 `∀̇`、`∃̇_`。`Δ₀` 片段在 Lévy 层级中给公式分类。`Δ₀` 不是公式上的谓词，而是一个归纳见证，证明该公式仅由原子经联结词与有界量词构成。关键在于，无界量化没有对应构造子：含有 `∀̇` 或 `∃̇_` 的公式根本无法携带 Δ₀ 见证，本章的 Δ₀ 定理正是依赖这一缺席。

```agda
open import FOL.ZFStructure using ( ZFStructure; _↾_ )
open import FOL.Syntax
  using ( Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy
  using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
```

公式的意义由语义模块给出，这里在 V.Hierarchy 的结构 `𝒮ᵥ` 上实例化：即装备成结构的累积层级，其关系取值于 `hProp (ℓ-suc ℓ)`。因此本章研究的真值恰是高一层的命题，正是 `isSmall` 所谈的那类。所有证明都建立在一套等价工具之上：等价类型 `_≃_` 及其求值 `equivFun` 与原像 `invEq`，穿越函数类型的 `equivΠ`，以及 `propBiimpl→Equiv`，它把两个命题性证明加一条双向蕴含变成等价。由于下面各等价的两端都是命题，最后这个构造子承担了大部分工作。

```agda
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; equivΠ; propBiimpl→Equiv )
import Cubical.Functions.Logic as Logic
```

要证联结词保小，需要低层 `ℓ`，即每次化归的目标宇宙，上的命题运算。它们保留限定名 `Logic`，因此 `Logic.⊓` 等名字显然作用于 `hProp ℓ`，而下文不加限定的运算作用于 `hProp (ℓ-suc ℓ)`。其余部分服务于具体的等价构造：`Σ-cong-equiv` 由逐分量的等价构造对子类型间的等价；`Sum.⊎-equiv` 处理余积；`tt*` 是单元元素；命题截断模块 `PT` 的 map 运算沿函数搬运「仅仅存在」式陈述，而不选取任何见证。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Sigma using ( Σ-cong-equiv )
import Cubical.Data.Sum as Sum
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT
```

层级本身提供原子数据。每个集合 `a` 都有一个单射呈现：小索引类型 `⟪ a ⟫` 与到 `V ℓ` 的嵌入 `⟪ a ⟫↪`。于是隶属有一个小的孪生 `_∈ₛ_`，定义为所有对 `(m : ⟪ b ⟫, ⟪ b ⟫↪ m ∼ a)` 的类型，落在 `hProp ℓ` 中；转换 `∈∈ₛ` 双向联结两种隶属，`identityPrinciple` 把双相似 `∼` 与真正的路径等同。运算 `∈-asFiber` 把 (不加截断的) 隶属变成嵌入的一个真正的纤维。`SeparationSet` 是库的分离构造，只接受已经在低宇宙取值的谓词。不加限定的联结词 `⊓ ⊔ ⇒ ¬ ⊤ ⊥` 与量词 `∀[ x ] P x` 与 `∃[ x ] P x` 直接作用于 `hProp (ℓ-suc ℓ)`。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∼_; identityPrinciple; _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module SeparationSet )
```

结构 record 在 `𝒮ᵥ` 处实例化，此后名字 `S`、`_≈ˢ_` 与 `_∈ˢ_` 就指它的载体与关系。具体地，`S` 是 `V ℓ`。关于结构成员的陈述因此是高一层的命题，而这类陈述能否小，正是本章要用力的地方。

```agda
open ZFStructure 𝒮ᵥ
```

## 何谓小

命题 `P : hProp (ℓ-suc ℓ)` 是小的 (记作 `isSmall P`)，指它配有低宇宙命题 `Q : hProp ℓ` 以及等价 `⟨ P ⟩ ≃ ⟨ Q ⟩`。该定义来自 `Base.Impredicativity`，那里的降层接口对每个命题一次性断言小性。本章不作这种假设，而是对个别的命题挣得小性，从结构的两个原子关系开始，再把这些见证经联结词与量词传递下去。

原子为何会是小的？因为 `V ℓ` 中集合的构造方式：它是某个 `⟪ a ⟫ : Type ℓ` 索引的族的像。「`x` 是 `a` 的成员」即是说某个索引呈现的成员等于 `x`，而这个陈述在小类型上量化。隶属因此有小孪生 `a ∈ₛ b`，`∈∈ₛ` 在两个方向上转换这两种关系。相等同样经恒等原理压缩为双相似 `a ∼ b`。

第一条引理把小的隶属关系打包成小性见证。要证 `isSmall (a ∈ˢ b)`，须给出一个低宇宙命题以及它与 `⟨ a ∈ˢ b ⟩` 的等价；见证取 `a ∈ₛ b`。由于两个底层类型都是命题，`propBiimpl→Equiv` 仅凭 `∈∈ₛ` 的两个方向即可造出等价。这里没有用到关于 `a`、`b` 的任何内容：无论这两个集合是什么，它们之间的隶属都是小的。注意引理没有说的内容：它不以路径等同两个关系，也不让 `∈ˢ` 本身落在低宇宙；它提供的是一个被压缩的等价物。

```agda
small-∈ : (a b : S) → isSmall (a ∈ˢ b)
small-∈ a b = (a ∈ₛ b) ,
  propBiimpl→Equiv (snd (a ∈ˢ b)) (snd (a ∈ₛ b))
    (∈∈ₛ {a = a} {b = b} .fst) (∈∈ₛ {a = a} {b = b} .snd)

small-≡ : (a b : S) → isSmall (a ≈ˢ b)
```

相等原子遵循同一模式，但用不同的小孪生。结构的相等 `a ≈ˢ b` 压缩为双相似 `a ∼ b`，即两集合有相同成员的陈述；库的恒等原理是 `⟨ a ∼ b ⟩` 与路径类型 `a ≡ b` 之间的等价，`invEquiv` 把它转向 `isSmall` 所需的方向，即从大宇宙的相等类型 `⟨ a ≈ˢ b ⟩` 到低宇宙的双相似命题。与 `small-∈` 合起来，语言的原子情形就此穷尽。

```agda
small-≡ a b = (a ∼ b) , invEquiv identityPrinciple
```

## 联结词保小

有了原子之后，下一个问题是小性能否在逻辑组合下存活。答案是肯定的：四个联结词与两个常量逐一传递小性见证；本节完成后，凡由小原子经联结词构成的真值都是小的。这也为日后对 Δ₀ 见证的归纳一次性封闭所有联结词情形铺平了道路。

每个证明取两个小性见证 `(P' , eP)` 与 `(Q' , eQ)`，其中 `eP : ⟨ P ⟩ ≃ ⟨ P' ⟩`、`eQ : ⟨ Q ⟩ ≃ ⟨ Q' ⟩`，再返回复合命题的小性见证。低宇宙分量由 `P'`、`Q'` 经层级 `ℓ` 上对应的 `Logic` 运算构成；等价分量则沿 `eP`、`eQ` 传输复合命题的证明。

合取最简单，因为 `P ⊓ Q` 的底层类型是对子 `⟨ P ⟩ × ⟨ Q ⟩`。用 `Logic.⊓` 组合两个压缩命题，其底层类型同样是乘积；等价由 `Σ-cong-equiv` 作用于 `eP`、`eQ` 得到：把一对证明映到其压缩后的一对。除了每个因子可压缩之外，不需要任何关于命题的其他内容。

```agda
small⊓ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊓ Q)
small⊓ {P} {Q} (P' , eP) (Q' , eQ) =
  (P' Logic.⊓ Q') , Σ-cong-equiv eP (λ _ → eQ)

small⊔ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊔ Q)
small⊔ {P} {Q} (P' , eP) (Q' , eQ) =
```

析取与蕴涵各需一个想法。对析取，`⟨ P ⊔ Q ⟩` 是余积的命题截断，因此压缩命题 `P' Logic.⊔ Q'` 也是截断，`PT.propTrunc≃` 把余积等价 `Sum.⊎-equiv eP eQ` 提升到截断上。截断纪律在此显现：该映射只是改记哪一侧成立，从不检视选定了哪一侧，因为截断根本不提供选定的侧。对蕴涵，`⟨ P ⇒ Q ⟩` 是函数类型 `⟨ P ⟩ → ⟨ Q ⟩`；压缩命题 `P' Logic.⇒ Q'` 在层级 `ℓ` 上形状相同，`equivΠ` 逐点地把等价穿过函数空间。

```agda
  (P' Logic.⊔ Q') , PT.propTrunc≃ (Sum.⊎-equiv eP eQ)

small⇒ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⇒ Q)
small⇒ {P} {Q} (P' , eP) (Q' , eQ) =
  (P' Logic.⇒ Q') , equivΠ eP (λ _ → eQ)

small¬ : {P : hProp (ℓ-suc ℓ)} → isSmall P → isSmall (¬ P)
```

否定是唯一一个压缩命题本身不能确定等价的情形，缘于否定的反变性：`¬ P` 的证明要消费 `P` 的证明。压缩命题取 `Logic.¬ P'`，其底层类型把 `⟨ P' ⟩` 映入空类型。两端都是命题，故 `propBiimpl→Equiv` 适用；两个方向沿相反方向使用 `eP`：要从压缩的反驳 `p'` 得到 `np : ¬ P` 的矛盾，把原像 `invEq eP p'` 喂给 `np`；反向则把 `p : ⟨ P ⟩` 的像 `equivFun eP p` 喂给 `np'`。等价的求值与逆恰好按否定的逻辑以相反的变差出现。

```agda
small¬ {P} (P' , eP) = (Logic.¬ P') ,
  propBiimpl→Equiv (snd (¬ P)) (snd (Logic.¬ P'))
    (λ np p' → np (invEq eP p'))
    (λ np' p → np' (equivFun eP p))

small⊤ : isSmall ⊤
```

两个常量收尾本节。真是小的，因为两端都是有元素的命题：压缩命题取 `Logic.⊤`，两个方向的函数都丢弃参数、返回单元元素 `tt*`。假的起点略有不同：真值 `⊥` 本就定义为 hProp 对 `(⊥* , isProp⊥*)`，故其底层类型恰是空类型 `⊥*`，压缩命题也就是打包成 hProp 的同一个空类型。于是两个函数都用荒谬来定义：空类型的参数没有任何情形可分。

```agda
small⊤ = Logic.⊤ ,
  propBiimpl→Equiv (⊤ .snd) (snd (Logic.⊤ {ℓ}))
    (λ _ → tt*) (λ _ → tt*)

small⊥ : isSmall (⊥ {ℓ = ℓ-suc ℓ})
small⊥ = (⊥* , isProp⊥*) ,
```

两个方向中的荒谬情形分析 `(λ ())` 就是假性证明的全部内容：`⊥*` 没有构造子，因此从它出发的函数无需任何定义子句。这是「构造子缺席能做真正的逻辑工作」这一主题的首次登场，它将在 Δ₀ 一节强势回归。

```agda
  propBiimpl→Equiv isProp⊥* isProp⊥* (λ ()) (λ ())
```

## 有界量词保小

联结词只够处理无量词的真值，而公式里出现一个有界量词就足以让下一节的归纳中断。本节移除这一障碍。以整个 `V ℓ` 为范围的量词在大载体 `S : Type (ℓ-suc ℓ)` 上量化，本章已有的构造本身不能压缩其真值；而**以集合 `a` 为界**的量词在语义上只在 `a` 的成员上量化，这些成员由一个小的索引类型呈现：单射呈现把 `a` 给作 `sett ⟪ a ⟫ ⟪ a ⟫↪`，其中 `⟪ a ⟫ : Type ℓ`。于是改在 `⟪ a ⟫` 上量化，得到的真值由小的命题 `sm (⟪ a ⟫↪ m)` 经 Π 或截断 Σ 构成，两者都能压缩。

两种量化之间的桥梁是 `∈-asFiber`：从 `x ∈ᵗ a` 的元素出发，它返回 `⟪ a ⟫↪` 在 `x` 上的一个真正的纤维，即索引 `m` 配路径 `⟪ a ⟫↪ m ≡ x` 的对。该纤维**不加截断**，因为 `⟪ a ⟫↪` 是嵌入，所以从 `a` 的成员回到 `⟪ a ⟫` 的索引是函数操作而非选择。两条引理的反向因此都无需任何选取。

全称有界量词陈述的是：对 `a` 的每个成员 `x`，命题 `B x` 成立。其真值是 `∀[ x ] (x ∈ˢ a) ⇒ B x`，即在整个载体上索引的蕴涵，前件 `x ∈ˢ a` 把注意限制到成员上。引理假设每个 `B x` 都小，见证为 `sm x = (B' x , e x)`，并断言整个全称陈述小。压缩命题用小孪生替换隶属、用 `⟪ a ⟫` 替换载体：它断言对每个索引 `m : ⟪ a ⟫`，命题 `B' (⟪ a ⟫↪ m)` 成立。界 `a` 作为显式参数进入，族 `B` 则保持隐式、由目标类型确定。

```agda
small-∀∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x)
small-∀∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
```

正向方向把原陈述的证明转换为压缩命题的证明。给定 `f`，它对每个 `x` 给出从 `x ∈ˢ a` 到 `B x` 的蕴涵；我们要对每个索引 `m` 产出 `B' (⟪ a ⟫↪ m)` 的证明。先在成员 `⟪ a ⟫↪ m` 处应用 `f`，这需要前件，即 `⟪ a ⟫↪ m` 是 `a` 成员的证明；转换 `∈∈ₛ` 从典范见证 `∈ₛ⟪ a ⟫↪ m` 给出它，后者不过是索引配上 `∼` 的自反性。得到的 `B (⟪ a ⟫↪ m)` 的证明再穿过等价 `e`，落入压缩命题。

```agda
  big = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x
  Qsm = ∀[ m ∶ ⟪ a ⟫ ] sm (⟪ a ⟫↪ m) .fst
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd f m = equivFun (sm (⟪ a ⟫↪ m) .snd)
                     (f (⟪ a ⟫↪ m) (∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)))
```

反向方向正是嵌入发挥价值之处。给定 `g`，它对每个索引 `m` 给出 `B' (⟪ a ⟫↪ m)` 的证明；我们要对每个满足 `x∈a : x ∈ᵗ a` 的 `x` 产出 `B x` 的证明。纤维 `mf = ∈-asFiber x∈a` 给出索引 `mf .fst` 与路径 `mf .snd : ⟪ a ⟫↪ (mf .fst) ≡ x`。在该索引处应用 `g` 得到 `B' (⟪ a ⟫↪ (mf .fst))` 的证明，逆等价把它送到 `B (⟪ a ⟫↪ (mf .fst))`；`subst` 再沿 `mf .snd` 把它传输到 `B x`。注意做调整的是路径，而非在成员间的任意选择：若纤维被截断，这一传输就无从谈起，引理在不加额外假设时将失败。

```agda
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd g x x∈a =
    subst (λ v → ⟨ B v ⟩) (mf .snd)
          (invEq (sm (⟪ a ⟫↪ (mf .fst)) .snd) (g (mf .fst)))
    where mf = ∈-asFiber {a = x} {b = a} x∈a
```

存在有界量词陈述的是：`a` 的某个成员 `x` 满足 `B x`。其真值是 `∃[ x ] (x ∈ˢ a) ⊓ B x`，即隶属与 `B` 的截断配对；压缩命题仅仅断言存在索引 `m : ⟪ a ⟫` 使 `B' (⟪ a ⟫↪ m)`。假设与结论都镜像全称情形，但证明性质不同：由于两侧都是截断的存在陈述，两个方向都不返回函数，而是把截断映到截断。

```agda
small-∃∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x)
small-∃∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
```

正向：`PT.map` 在截断内部施加逐点构造，这是允许的，因为目标即压缩命题仍是命题。逐点步骤拆开截断的三元组 `(x , x∈a , bx)`：成员、其隶属证据、以及 `B x` 的证明。这一拆开之所以合法，只因它发生在截断之下，`x` 的选取永远不必导出。随后 `x∈a` 的纤维给出索引，证明 `bx` 沿纤维的路径、按 `sym (mf .snd)` 方向传输，再经等价压缩。可与全称的正向对照：那里函数是直接到手的，这里仅仅知道这样的数据存在。

```agda
  big = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x
  Qsm = ∃[ m ∶ ⟪ a ⟫ ] sm (⟪ a ⟫↪ m) .fst
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd = PT.map λ where
    (x , x∈a , bx) →
```

反向：同样在 `PT.map` 之下，截断的对 `(m , q)`，即索引与 `B' (⟪ a ⟫↪ m)` 的证明，被转换成一个具有性质 `B` 的 `a` 的成员。成员取 `⟪ a ⟫↪ m`，其隶属证据由 `∈∈ₛ` 作用于典范见证得到，性质证明是原像 `invEq (sm _ .snd) q`。这里完全不需要传输：索引一开始就给定，无须从成员恢复。两个方向之间的不对称正是数据的不对称：一侧直接握有索引，另一侧必须从成员制造索引，而只有嵌入使这一制造成为函数。

```agda
      let mf = ∈-asFiber {a = x} {b = a} x∈a
      in mf .fst ,
         equivFun (sm (⟪ a ⟫↪ (mf .fst)) .snd)
                  (subst (λ v → ⟨ B v ⟩) (sym (mf .snd)) bx)
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
```

有了这对引理，语义中的有界量词子句已被覆盖，下一节的归纳可以穿过任何量词皆有界的公式。值得注意的是没有用到什么：两条证明都没有使用任何经典原则、选择，也没有使用降层。唯一实质的事实是隶属的单射呈现，以及 `⟪ a ⟫↪` 是嵌入这一性质。

```agda
  bwd = PT.map λ where
    (m , q) → ⟪ a ⟫↪ m , ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)
            , invEq (sm (⟪ a ⟫↪ m) .snd) q
```

## 从小性到分离

本节是小性兑现之处。库的分离构造 `SeparationSet` 对集合 `a` 与取值于**低**宇宙的谓词 `ϕ : V ℓ → hProp ℓ`，构造一个集合，其成员恰是 `a` 中满足 `ϕ` 的成员。对上宇宙谓词这种构造不可能：其内部索引类型必须落在层级 `ℓ`。下面的引理是适配器：给定 `S` 上逐点带小性见证的谓词 `P`，它产出结构中的集合 `s`，并附上成员规格「`y ∈ˢ s` 当且仅当 `y ∈ˢ a` 且 `P y`」，以模型 record 分离字段风格的路径表述。

这里也是各部件汇成计划之处。无论谓词的小性最先来自何处，是上一节的有界量词，还是最后的本质小世界，本引理都把小谓词一次性、以同一方式变成集合。

这条陈述值得细读。结果是一个依值对：结构中的集合 `s`，以及对每个 `y` 的**路径** `(y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y)`，落在类型 `hProp (ℓ-suc ℓ)` 中，而不只是底层命题间的双向蕴含。这与模型 record 分离字段的形状一致，因此该构造可以被移植进任何需要验证分离公理的结构。证明把库构造应用于 `a` 与压缩后的谓词，再由所得规格的两个方向拼装出所需的路径。

```agda
separateFromSmall : (a : S) (P : S → hProp (ℓ-suc ℓ))
                  → (∀ y → isSmall (P y))
                  → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y))
separateFromSmall a P sm = Sep.SEPAREE , λ y → ⇔toPath (fwd y) (bwd y)
  where
```

先组装压缩谓词：`ϕₛ y` 按定义就是从逐点小性见证中取出的低宇宙替身 `sm y .fst`。随后库模块 `Sep` 在 `a` 与 `ϕₛ` 处实例化，其结果集合名为 `Sep.SEPAREE`。这是本章唯一一处运行库分离的地方；本部分其余的分离都要经过这条引理。

```agda
  ϕₛ : S → hProp ℓ
  ϕₛ y = sm y .fst
  module Sep = SeparationSet a ϕₛ
  fwd : ∀ y → ⟨ y ∈ˢ Sep.SEPAREE ⟩ → ⟨ (y ∈ˢ a) ⊓ P y ⟩
  fwd y y∈s = ∈∈ₛ {a = y} {b = a} .snd (Sep.separation-ax y .fst y∈ₛs .fst)
```

两个方向都在结构隶属 `y ∈ˢ Sep.SEPAREE` 与「`y ∈ˢ a` 加 `P y`」之间翻译。正向：经 `∈∈ₛ` 把 `y∈s` 转成小隶属，喂给库规格 `separation-ax y` 的正向，得到 `y ∈ₛ a` 与压缩性质的配对；第一分量再以另一朝向经 `∈∈ₛ` 转回 `y ∈ᵗ a`，第二分量经等价 `e` 的逆展开。反向是镜像：把 `a` 中隶属转成小形式，用 `equivFun` 压缩性质证明，让 `separation-ax y` 的反向产出 `Sep.SEPAREE` 中的隶属，再经 `∈∈ₛ` 转换一次。库规格承担集合论的工作，等价承担宇宙层面的记账。

```agda
            , invEq (sm y .snd) (Sep.separation-ax y .fst y∈ₛs .snd)
    where y∈ₛs = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .fst y∈s
  bwd : ∀ y → ⟨ (y ∈ˢ a) ⊓ P y ⟩ → ⟨ y ∈ˢ Sep.SEPAREE ⟩
  bwd y yp = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .snd (Sep.separation-ax y .snd
               (∈∈ₛ {a = y} {b = a} .fst (yp .fst) , equivFun (sm y .snd) (yp .snd)))
```

## Δ₀ 公式求值小

前几节积累了小性见证的库存：两个原子、四个联结词、两个常量与两个有界量词。本节通过对 `Δ₀` 见证本身的归纳把库存变成定理。回顾 Lévy 层级一章，`Δ₀` 是归纳定义的见证，每个公式至多一个，其构造子证明该公式仅由原子经联结词与有界量词构成。定理陈述：凡带有这种见证的公式，在任何环境下的真值都小。由于见证是归纳定义的，证明就是每个构造子一个情形的归纳，而每个情形恰好就是库存中的一条引理。

情形分析有一个富有教益的省略：无界量词 `∀̇` 与 `∃̇_` 没有对应情形，因为见证类型本就没有它们的构造子。构造子的缺席正是分类的实现方式；带无界量词的公式根本无法携带 Δ₀ 见证，归纳也就永远不必面对它。Lévy 层级由此充任宇宙代价的核算：Δ₀ 恰是真值无需付出这一代价的片段。

准备工作一次性实例化语义：`SemanticsV` 是 `𝒮ᵥ` 上、真值取于 `hProp (ℓ-suc ℓ)` 的满足关系，因此公式的真值恰是全章一直在压缩的那类命题。环境类型 `S ^ n` 是长度 `n` 的向量记法。模块由常元解释 `ι : K → S` 参数化，故定理对常元的任意选取成立；恒等函数这一典范情形在本章末取用。模块内 `open SemanticsV.At K ι` 把词项求值 `⟦_⟧` 与满足 `_⊨_` 带入作用域。目标类型值得注意：`Δ₀-small` 是从 Δ₀ 见证到「对每个环境 `γ`，`γ ⊨ φ` 的小性见证」的函数。归纳针对见证进行，公式与环境在其外围被全称量化。

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

module Δ₀Small {ℓc} {K : Type ℓc} (ι : K → S) where

  open SemanticsV.At K ι

  Δ₀-small : ∀ {n} {φ : Formula K n} → Δ₀ φ → (γ : S ^ n) → isSmall (γ ⊨ φ)
```

原子情形在环境 `γ` 中求值两个词项后，直接调用前两条库存引理：隶属变为对 `t`、`u` 的值应用 `small-∈`，相等变为 `small-≡`。三个二元联结词情形同样直接：归纳假设 `Δ₀-small c γ` 与 `Δ₀-small d γ` 是子公式真值的小性见证，对应联结词的封闭引理把它们组合起来。显式实例化 `{P = γ ⊨ φ}` 只是记录见证所压缩的是哪些命题；Agda 本可推断，但写出来记录了该情形的形状。

```agda
  Δ₀-small (δ-∈ {t = t} {u}) γ = small-∈ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-≐ {t = t} {u}) γ = small-≡ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-∧ {φ = φ} {ψ} c d) γ =
    small⊓ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-∨ {φ = φ} {ψ} c d) γ =
```

其余联结词形状的情形是假，然后是两个有界量词。假完全不需要环境：见证 `δ-⊥` 不携带子公式，该情形就是 `small⊥`。有界量词情形才有意思。对 `δ-∀∈`，公式是 `∀̇∈ t φ`，其真值是 `∀[ x ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ φ)`；这恰好是 `small-∀∈` 消费的形状，其中 `a` 取 `t` 的值，族 `B x` 取体公式在扩展环境 `x ∷ γ` 下的真值。归纳假设在扩展环境处应用；这是合法的，因为见证 `c` 证明的正是体公式 `φ` 本身。

```agda
    small⊔ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-⇒ {φ = φ} {ψ} c d) γ =
    small⇒ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small δ-⊥ γ = small⊥
  Δ₀-small (δ-∀∈ {t = t} {φ = φ} c) γ =
```

存在有界情形与全称完全镜像：用 `small-∃∈` 替换 `small-∀∈`，把合取形状的真值 `∃[ x ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ)` 对上 `small-∃∈` 的结论。归纳就此闭合：见证类型的每个构造子都有情形，每个情形都是一条库存引理，而无界量词不再留下任何情形。定理 `Δ₀-small` 由此成为前几节从孤立事实转变为关于形式语言之陈述的转折点。

```agda
    small-∀∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))
  Δ₀-small (δ-∃∈ {t = t} {φ = φ} c) γ =
    small-∃∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))
```

## 无需命题降级的 Δ₀ 分离

把上一节的归纳与之前的适配器复合，本章的核心定理便出现了。取典范常元解释：语言的常元就是结构中的集合本身，`ι` 为恒等函数。此时带一个自由变量的 Δ₀ 公式 `φ` 在 `S` 上定义一个逐点小的谓词，`separateFromSmall` 把它变成集合。结果是分离公理模式限制到 Δ₀ 公式的完整实例，证明中既无命题降级原则，也无任何经典公理或选择：小性由归纳供给，其余交给库构造。模型章仍欠无限制的分离公理；本定理说明，Lévy 层级中的 Δ₀ 档无需 `V` 的表示之外的任何东西。

开头两行固定典范解释：`Δ₀Small id` 在恒等处实例化归纳，单自由变量的满足关系再导出为 `_⊨_`。定理的类型是以 `φ` 替换任意谓词的分离规格：一个集合 `s`，使得对每个 `y`，`s` 中的隶属作为真值等于 `a` 中的隶属与「`y` 在单元环境 `y ∷ []` 下满足 `φ`」的合取。证明是 `separateFromSmall` 的一次应用：传入谓词 `λ y → (y ∷ []) ⊨ φ` 及其逐点小性，后者是 `Δ₀-small c` 在每个单元环境处的应用。此外别无他物：Δ₀ 见证 `c` 恰好被归纳消费一次。

```agda
open Δ₀Small id
open SemanticsV.At S id using ( _⊨_ )

separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ
           → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ)))
separateΔ₀ a φ c = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → Δ₀-small c (y ∷ []))
```

## 本质小的世界

Δ₀ 定理把每个量词都按「在全 `V ℓ` 上量化」计价。最后这一层小性通过改变量化的位置连这个代价也免除了。设上层类型 `A` 配有从小类型 `X : Type ℓ` 出发的等价 `e : X ≃ A`。那么对 `A` 的量化可以逐步替换为对 `X` 的量化：关于 `A` 中元素 `a` 的陈述，在其原像 `equivFun e m` 处读取。有界量词引理是相关但不同的现象：那里量化范围是呈现某个集合的索引类型，隶属充当过滤器；这里不再留下任何有界性假设。于是小性不是由公式的形状承载，而是由说出它的世界的形状承载。注意假设的方向：它断言的是从 `X` 到 `A` 的等价 `e` 存在；`A` 本身仍住在上层宇宙。

先看全称版本。陈述 `∀[ x ] P x B` 对整个 `A` 量化；压缩命题改为对 `X` 量化，断言对每个 `m : X`，压缩命题 `sm (equivFun e m) .fst` 成立。由于 `e` 是等价，在 `X` 上量化与在 `A` 上量化给出等价的依值函数类型。等价分量把一族证明 `f : ∀ m → ⟨ sm (e m) ⟩` 传输为 `∀ a → ⟨ B a ⟩`，逐点再与各等价复合，`invEquiv` 按目标类型的要求把复合定向为从小 Π 到大 Π。注意与 `small-∀∈` 的对照：那里的前件 `x ∈ˢ a` 起了过滤作用；这里没有前件，仅凭等价完成化归。

```agda
small-∀ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (∀[ a ∶ A ] B a)
small-∀ {X = X} e sm = (∀[ m ∶ X ] sm (equivFun e m) .fst)
  , invEquiv (equivΠ e (λ m → invEquiv (sm (equivFun e m) .snd)))
```

存在版本沿用同一方案，只是以截断替换函数类型。压缩命题是对 `X` 的小性见证的截断 Σ；等价从对 `A` 的大见证的截断 Σ 出发：`Σ-cong-equiv` 沿 `e` 把对子的基底从 `A` 换成 `X`，各纤维沿逆的逐点等价变换，`PT.propTrunc≃` 再把对子等价提升到截断上。`invEquiv` 同样提供所需朝向。两条引理合起来说：对任何本质小类型的量化保持小性；而「本质小」在下一块代码中将指等价于层级 `ℓ` 的某个类型。

```agda
small-∃ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (∃[ a ∶ A ] B a)
small-∃ {X = X} e sm = (∃[ m ∶ X ] sm (equivFun e m) .fst)
  , invEquiv (PT.propTrunc≃ (Σ-cong-equiv e (λ m → invEquiv (sm (equivFun e m) .snd))))
```

后果是：在本质小的限制结构上，**任何**公式求值皆小，无需 Δ₀ 见证。固定结构上的类 `M`，并设其限制载体本质小，精确形式是等价 `e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))`，其中 `X : Type ℓ`。在结构 `𝒮ᵥ ↾ M` 内，量词在该限制载体上量化，于是上一块代码的两条引理对每个量词都适用，无论有界与否；原子则经第一投影归结为 `V` 的原子小性。有界性是公式的句法限制，而本质小是量化范围的性质。有了后一项假设，结构归纳便同时覆盖无界与有界量词。内部满足的这一小性，正是让可定义性步骤 (例如可构造层级在每层所做的那一步) 能以低宇宙的谓词运作的原因。

模块的参数装配出这个小世界。`M` 是载体 `S` 上的一个类，可以是真类：没有任何大小限制。假设是一对数据：小类型 `X : Type ℓ`，以及从 `X` 到限制载体 `Σ[ x ∈ S ] (x ∈ᶜ M)` 的等价；这正是「世界本质小」的精确含义。注意负担在于该等价存在，而不在于 `M` 在任何内部意义上有界。常元经 `ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)` 在限制载体中解释，因此每个常元指称一个对子，其第二分量是「第一分量属于 `M`」的证据。

```agda
module InnerSmall (M : S → hProp (ℓ-suc ℓ))
                  (X : Type ℓ) (e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M)))
                  {ℓc} {K : Type ℓc}
                  (ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)) where

  SM : Type (ℓ-suc ℓ)
```

两个缩写固定记号。`SM` 命名限制载体本身；`𝒮M` 是限制到 `M` 的结构，由 `_↾_` 构造：其载体是 `SM`，h-集合性被继承，两个关系沿第一投影拉回，因此世界内部的相等与隶属由 `V` 的底层集合决定。语义模块在 `𝒮M` 处实例化，满足与词项求值记号以上标记号改名，标示公式是在世界**内部**读取的。该改名以 public 导出，其他章节可在这些名字下读取限制后的满足关系。

```agda
  SM = Σ[ x ∈ S ] (x ∈ᶜ M)

  𝒮M : ZFStructure (ℓ-suc ℓ)
  𝒮M = 𝒮ᵥ ↾ M

  module SemanticsM = FOL.Semantics 𝒮M
  open SemanticsM.At K ι renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) public
```

定理的陈述刻意与 `Δ₀-small` 平行：对任意元数 `n` 的公式 `φ` 与任意限制元素环境 `δ : SM ^ n`，真值 `δ ⊨ᵐ φ` 是小的。这里看不到任何归纳见证，因为不需要：此处的归纳直接针对公式，载体的本质小性取代了 Δ₀ 限制。两个原子情形在世界内求值词项，得到限制元素，再对其第一投影应用原子小性引理：世界内的隶属 `(fst xm) ∈ˢ (fst ym)` 恰是环境结构的命题，其小性已知。

```agda
  ⊨ᵐ-small : ∀ {n} (φ : Formula K n) (δ : SM ^ n) → isSmall (δ ⊨ᵐ φ)
  ⊨ᵐ-small (t ∈̇ u)  δ = small-∈ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (t ≐ u)  δ = small-≡ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (φ ∧̇ ψ)  δ =
    small⊓ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
```

三个二元联结词与假的处理与之前完全相同：封闭引理 `small⊓`、`small⊔`、`small⇒` 与常量 `small⊥` 对所消费的命题是层级泛型的，因此对在世界内读取的真值原样适用。这正是先前把它们单独隔离的意义：那些证明没有提及 `V` 的任何特殊性，只涉及 `hProp (ℓ-suc ℓ)`。

```agda
  ⊨ᵐ-small (φ ∨̇ ψ)  δ =
    small⊔ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (φ ⇒̇ ψ)  δ =
    small⇒ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small ⊥̇        δ = small⊥
```

现在轮到量词，两个世界引理在此登场。无界存在量词 `∃̇ φ` 的真值是限制载体上的 `∃[ xm ] (xm ∷ δ) ⊨ᵐ φ`，归纳假设给出每个纤维 `(xm ∷ δ) ⊨ᵐ φ` 的小性。这恰是 `small-∃` 的形状，`A` 取限制载体、`e` 取其小性等价，该情形由直接应用闭合。全称情形是 `small-∀` 的镜像。注意量化确实是对限制世界进行的：`SM` 的元素是对子，因此扩展环境 `xm ∷ δ` 是以完整的限制元素扩展，体公式在这些元素处读取。

```agda
  ⊨ᵐ-small (∃̇ φ)    δ =
    small-∃ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇ φ)    δ =
    small-∀ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇∈ t φ) δ =
```

有界量词在每个情形中把两个小性来源合并。对 `∀̇∈ t φ`，真值是限制载体上有界的蕴涵：`∀[ xm ] (fst xm ∈ˢ ⟦ t ⟧ᵐ δ) ⇒ ((xm ∷ δ) ⊨ᵐ φ)`。前件的小性来自原子引理，后件的小性来自归纳假设，`small⇒` 组装蕴涵；整个陈述再经 `small-∀` 沿 `e` 而小。有趣的细节是第一投影 `fst xm`：有界性是关于限制元素底层集合的陈述，因为世界的隶属关系本就是 `V` 的拉回。

```agda
    small-∀ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⇒ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
      small⇒ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))
  ⊨ᵐ-small (∃̇∈ t φ) δ =
    small-∃ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⊓ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
```

存在有界情形是对偶的复合：真值是在截断 Σ 下把有界与体公式配对，`small⊓` 组合两个小性见证，`small-∃` 把整个陈述搬到小索引类型上。此情形完成归纳，本章的第二项主结果就此成立：在本质小的世界内，包括无界量词在内的每个公式都有小的真值。Δ₀ 小性由公式的形状承载，本质小性由量词的范围承载；无论哪种方式，一旦拿到小谓词，前一节的分离都照常适用。

```agda
      small⊓ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))
```

## 小结

小性即与低一层命题的等价 (`isSmall`)。`V` 的原子隶属与相等经库的单射呈现压缩；四个联结词与两个常量经对应的低层运算传递小性见证；有界量词通过在集合的小索引类型上量化而压缩，其间用到嵌入的非截断纤维。适配器 `separateFromSmall` 把任何逐点小的谓词变成带有分离规格的集合。归纳 `Δ₀-small` 直接给出 Lévy 层级的 Δ₀ 档，`separateΔ₀` 把它变成无需命题降级、无需任何经典公理或选择的 Δ₀ 分离。Δ₀ 之外的公式需要更多，模型章以命题降级的名义供给。最后一节引入了第二条路径：在载体本质小，即等价于 `ℓ` 层某类型的世界里，每个公式求值皆小，这正是让可定义性步骤能以低宇宙谓词运作的原因。