累积层级中的小真值

在累积层级 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 限制到一个类上的运算 _↾_ 将在最后一节用到。

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

open import Base.Prelude

module V.Smallness {ℓ : Level} where

open import Base.Impredicativity using ( isSmall )

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

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，它把两个命题性证明加一条双向蕴含变成等价。由于下面各等价的两端都是命题，最后这个构造子承担了大部分工作。

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 运算沿函数搬运「仅仅存在」式陈述，而不选取任何见证。

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

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

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

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 的任何内容：无论这两个集合是什么，它们之间的隶属都是小的。注意引理没有说的内容：它不以路径等同两个关系，也不让 ∈ˢ 本身落在低宇宙；它提供的是一个被压缩的等价物。

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-∈ 合起来，语言的原子情形就此穷尽。

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 得到：把一对证明映到其压缩后的一对。除了每个因子可压缩之外，不需要任何关于命题的其他内容。

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Π 逐点地把等价穿过函数空间。

  (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'。等价的求值与逆恰好按否定的逻辑以相反的变差出现。

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 的同一个空类型。于是两个函数都用荒谬来定义：空类型的参数没有任何情形可分。

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

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

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

  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 则保持隐式、由目标类型确定。

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，落入压缩命题。

  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。注意做调整的是路径，而非在成员间的任意选择：若纤维被截断，这一传输就无从谈起，引理在不加额外假设时将失败。

  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)。假设与结论都镜像全称情形，但证明性质不同：由于两侧都是截断的存在陈述，两个方向都不返回函数，而是把截断映到截断。

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) 方向传输，再经等价压缩。可与全称的正向对照：那里函数是直接到手的，这里仅仅知道这样的数据存在。

  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。这里完全不需要传输：索引一开始就给定，无须从成员恢复。两个方向之间的不对称正是数据的不对称：一侧直接握有索引，另一侧必须从成员制造索引，而只有嵌入使这一制造成为函数。

      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 ⟫↪ 是嵌入这一性质。

  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 与压缩后的谓词，再由所得规格的两个方向拼装出所需的路径。

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。这是本章唯一一处运行库分离的地方；本部分其余的分离都要经过这条引理。

  ϕₛ : 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 中的隶属，再经 ∈∈ₛ 转换一次。库规格承担集合论的工作，等价承担宇宙层面的记账。

            , 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 是从 Δ₀ 见证到「对每个环境 γ，γ ⊨ φ 的小性见证」的函数。归纳针对见证进行，公式与环境在其外围被全称量化。

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 本可推断，但写出来记录了该情形的形状。

  Δ₀-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 证明的正是体公式 φ 本身。

    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 由此成为前几节从孤立事实转变为关于形式语言之陈述的转折点。

    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 恰好被归纳消费一次。

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

separateΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
           → Σ[ 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 起了过滤作用；这里没有前件，仅凭等价完成化归。

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 同样提供所需朝向。两条引理合起来说：对任何本质小类型的量化保持小性；而「本质小」在下一块代码中将指等价于层级 ℓ 的某个类型。

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」的证据。

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 导出，其他章节可在这些名字下读取限制后的满足关系。

  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) 恰是环境结构的命题，其小性已知。

  ⊨ᵐ-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 ℓ)。

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

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

  ⊨ᵐ-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 的拉回。

    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-∃ 把整个陈述搬到小索引类型上。此情形完成归纳，本章的第二项主结果就此成立：在本质小的世界内，包括无界量词在内的每个公式都有小的真值。Δ₀ 小性由公式的形状承载，本质小性由量词的范围承载；无论哪种方式，一旦拿到小谓词，前一节的分离都照常适用。

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

小结

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