累积层级

集合论语言的每个模型都需要一个由「集合」组成的载体，连同取值于命题的等词与成员关系。本章构造这个载体。它就是累积层级 V，一个高阶归纳类型，体现的是集合论最古老的观念：集合不外乎其成员的汇集。这个类型把观念不折不扣地体现了出来。每个集合都由一个以小类型为索引的集合族呈现，每个索引对应一个成员；属于它，无非是拥有该族中一个命中此元素的索引。成员相同的两种呈现给出的是同一个集合，因此外延性不是这个模型有待要求的公理，而是类型构造的方式本身。

本章在这个载体上建立结构 𝒮ᵥ，并证明最早的一批集合论性质，从外延性直到沿成员关系的递归原理。层级原生地供给了结构所要求的一切：集合之间的等词就是路径类型，因层级是 h-集合而为命题值；成员关系取层级自身的 ∈，本就取值于 hProp。本章固定一个宇宙层级 ℓ，全章所有构造都在该层级上陈述。

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

open import Base.Prelude

module V.Hierarchy {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; module hPropStructure )

本章最难的证明依赖两个观念。其一是命题截断。「某个索引可行」这类陈述只作为纯粹存在保留，不选定任何见证，而截断后的陈述只能消去到命题。其二是可及性，即伴随良基关系的归纳数据 Acc：当一个元素向下的每一步、从该元素到它的某个成员，都落在本身可及的元素上时，这个元素是可及的。二者能配合，是因为层级的成员关系本身就是截断的。良基性的证明必须把一个纯粹存在的索引转换为可及性证明，而可及性正是命题。

import Cubical.HITs.PropositionalTruncation as PT
import Cubical.Data.Empty as Empty
import Cubical.Induction.WellFounded as WellFoundedInduction
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded; isPropAcc; wf→x≮x )
open import Cubical.HITs.CumulativeHierarchy.Base

层级本身值得细读，此后的一切论证都建立在它之上。其构造子 sett 从小索引类型和指向层级的族造出作为该族之像的集合。成员关系 y ∈ sett X ix 是截断的原像：当某个 i : X 使 ix i ≡ y 时成立，而且只以此方式成立。路径构造子把成员一致的任意两个 sett 表示视为相等，这是内建于类型本身的外延性。这个类型并非在本章定义；本章在其上构造结构 𝒮ᵥ，并证明该结构的集合论性质。

  using ( V; setIsSet; _∈_; elimProp )
open import Cubical.HITs.CumulativeHierarchy.Base
  using ( sett )  -- lint-agda: keep (prose references link through this import)
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; extensionality )

高阶归纳类型

其基本思想是集合论中最古老的表述：集合不外乎其成员的汇集。这个类型把思想落实为数据，并带有两点值得注意的约束。索引类型必须小，形如 X : Type ℓ，因此每个集合都由大小为 ℓ 的数据组装而成；整个类型经 setIsSet 而成为 h-集合，因此无论呈现如何被同一化，结果之间都不残留可区分的结构。

结构

要把层级视为一阶结构，需要给出 record 所列的各项数据；层级本身已经具备这些数据。要有一个由集合组成的载体：V ℓ 供给了它，而且 h-集合性不是额外要求，而是层级自证的事实。要有取命题值的等词：h-集合的元素之间的路径构成命题，路径类型即可充任。要有取命题值的成员关系：层级自身的 ∈ 本就落在 hProp 中。无须另造任何部分，这些字段组装成结构 𝒮ᵥ，一阶语言就在其上解释。下标就是普通的 v，指层级。

等词字段把这个选择写得很明确：_≈ˢ_ 把 x 与 y 送到由路径类型 x ≡ y 与「该类型是命题」的证明 setIsSet x y 组成的对，而这正是 hProp (ℓ-suc ℓ) 中元素的形状。同一条 h-集合性定理在结构中承担两项作用：setIsSet 充任字段 isSetS，setIsSet x y 则证明用作等词的路径类型是命题。路径本身无须任何转换：对 h-集合而言，两个元素之间的路径类型本来就是命题，字段只是把这个类型连同它所附带的证书一起记录下来。

𝒮ᵥ : ZFStructure (ℓ-suc ℓ)
𝒮ᵥ = record
  { S      = V ℓ
  ; isSetS = setIsSet
  ; _≈ˢ_   = λ x y → (x ≡ y) , setIsSet x y

成员关系字段 _∈ˢ_ 就是层级自身的 ∈，它在每一对上的取值本来就在 hProp (ℓ-suc ℓ) 之中。由于结构的关系都是命题值，后文许多论证需要的是命题的底层类型，而不是命题本身。打开 hPropStructure 𝒮ᵥ 即可得到这一读法：x ∈ᵗ y 指成员命题的元素所构成的类型 ⟨ x ∈ˢ y ⟩。二者是同一条关系的两种读法，∈ˢ 给出命题，∈ᵗ 给出其底层类型。良基性与归纳就建立在这个读法之上。

  ; _∈ˢ_   = _∈_ }

open hPropStructure 𝒮ᵥ

在证明开始之前，先看清层级的位置。载体 V ℓ 住在 Type (ℓ-suc ℓ)，比它的索引类型高一个宇宙，关系的取值也随之住在同层的 hProp (ℓ-suc ℓ) 中：层级是由小索引数据造出的大类型。经 ∈∈ₛ 与大成员关系相连的小成员关系 ∈ₛ 在下文的证明中会再次出现。

外延性与成员关系的良基性

假设两个集合 a 与 b 在每一点上一致：对每个 x，命题 x ∈ a 与 x ∈ b 之间有路径。那么 a 的任何成员沿该路径可搬运为 b 的成员，反之亦然，于是 a 与 b 互相包含。库的 extensionality 正是把这种双向包含转化为路径 a ≡ b，而 subst 沿逐点路径搬运成员资格来完成转化。层级的外延性因此是其定义的推论，而非额外假设。

extensionalV : {a b : V ℓ} → ((x : V ℓ) → (x ∈ a) ≡ (x ∈ b)) → a ≡ b
extensionalV {a} {b} h = extensionality a b
  ( (λ x x∈ₛa → ∈∈ₛ {a = x} {b = b} .fst
      (subst ⟨_⟩ (h x) (∈∈ₛ {a = x} {b = a} .snd x∈ₛa)))
  , (λ x x∈ₛb → ∈∈ₛ {a = x} {b = a} .fst

假设 h 对每个 x 给出命题 x ∈ a 与 x ∈ b 之间的路径；目标是路径 a ≡ b。库的 extensionality 期望小成员关系，因此证明经桥 ∈∈ₛ 走一个方向。输入 x∈ₛa 是 x 属于 a 的小成员关系。其转换 ∈∈ₛ .snd x∈ₛa 从小到大，产出 x ∈ a 的一个元素。然后 subst ⟨_⟩ (h x) 沿逐点路径搬运该元素；由于 h x 说两条成员命题在 x 处一致，搬运后的值落在 x ∈ b 中。最后 ∈∈ₛ .fst 从大到小转回，得到 x 属于 b 的小成员关系。这正是 extensionality 所需双向包含的向前分量。

      (subst ⟨_⟩ (sym (h x)) (∈∈ₛ {a = x} {b = b} .snd x∈ₛb))) )

第二个分量是把桥反向走一遍：x 属于 b 的小成员关系先转为大，再沿 sym (h x) 反向搬运，最后转回 x 属于 a 的小成员关系。两个分量合起来构成双向包含，extensionality 由此得到 a ≡ b，即 extensionalV 返回的路径。

(经 ∈∈ₛ 现身的 ∈ₛ 是库的小成员关系，「集合的小呈现」一章将细说；此处它只起衔接作用。)

在本书中，正则性即是「成员关系良基」这一陈述：载体的每个元素在 ∈ᵗ 下都可及，含义即上文引入的可及性数据 Acc。证明把该高阶归纳类型消去到族 λ s → Acc _∈ᵗ_ s。向任意族的消去并非总是可用；使这里合法的，是每个 Acc _∈ᵗ_ s 都是命题，而 isPropAcc s 恰好给出这份证书。在 sett 情形中，分支拿到族 ix，以及对每个索引给出 rec i : Acc _∈ᵗ_ (ix i) 的归纳假设。它要组装 Acc _∈ᵗ_ (sett X ix)；按 acc 的形状，这就是要对集合的任意成员 y 给出可及性。

regularityV : WellFounded _∈ᵗ_
regularityV = elimProp (λ s → isPropAcc s)
  (λ X ix rec → acc (λ y y∈ →
    PT.rec (isPropAcc y)
           (λ { (i , p) → subst (Acc _∈ᵗ_) p (rec i) })

对这样的成员 y，证据 y∈ 只给出一对 (i , p) 的命题截断，其中 p : ix i ≡ y。调用 PT.rec (isPropAcc y) 可以消去这个截断原像，因为真正的目标 Acc _∈ᵗ_ y 是命题，而 isPropAcc y 正是它的命题性证书。在分支内部，subst (Acc _∈ᵗ_) p (rec i) 把归纳假设从 ix i 搬运到 y。整个证明由此用到索引，却从未全局选定一个索引。

           y∈))

正则性的第一个推论是不可反性：没有集合属于自身。用可及性的语言看，这是直接的。与自身处于良基关系中的元素会同可及性数据矛盾，因为可及性要求每一步下降都落在可及的元素上。这里的推导使用的是上文证明的 Acc 陈述；本章不宣称它涵盖 Foundation 的每一个经典表述。

假设 ⟨ A ∈ˢ A ⟩ 是成员命题底层类型的一个元素，而这正是 regularityV 所针对的关系 ∈ᵗ。对任何良基关系，元素都不能与自身处于该关系中：这就是库的不可反性定理 wf→x≮x，此处以 regularityV 作为其良基性输入。结果是矛盾，以空类型 Empty.⊥ 呈现。

∈-irrefl : (A : S) → ⟨ A ∈ˢ A ⟩ → Empty.⊥
∈-irrefl A = wf→x≮x regularityV {x = A}

沿成员关系的递归

良基性有计算上的回报：良基关系支持递归。x 处的值可以依赖于 x 的每个成员 y 处的值，而由于成员关系良基，这种依赖必然终止。目标可以是任意的依赖类型族 P，而不限于命题；这使它成为递归原理而非仅仅是证明原理。这是沿成员关系的递归在类型论中的形态，且不以序数索引的层级来陈述：不是沿层指标递归，而是直接沿成员关系本身递归。其递归方程还以命题等式成立，故后续论证可据以计算。

从外向内读 ∈-induction 的类型。类型族 P 给每个集合指派任意宇宙 Type ℓ' 中的一个类型，因此被构造的值可以真正随集合变化。步进函数 e 接收集合 x，以及 x 的每个成员 y 处的递归值 P y，成员关系经由成员命题的 Type 值读法 ∈ᵗ 出现，并返回 P x。为这一构造提供依据的是 regularityV：库的 WFI.induction 在这条良基关系上实例化，把步进函数变为全定义的族。此处无需重新证明良基性。

∈-induction : ∀ {ℓ'} {P : V ℓ → Type ℓ'}
            → (∀ x → (∀ y → y ∈ᵗ x → P y) → P x)
            → ∀ x → P x
∈-induction = WellFoundedInduction.WFI.induction regularityV

∈-induction-compute : ∀ {ℓ'} {P : V ℓ → Type ℓ'}

计算法则把每个成员处的递归调用显式地作为等式呈现，而不是藏在定义之中：∈-induction e x 等于把步进函数作用于 x 与每个成员 y 处的 ∈-induction e y。该等式以命题等式的形式陈述，因此未必定义性成立；显式陈述它，使得当化归不是定义性时，后续证明仍可按这条等式改写递归定义的值。该法则即库的 WFI.induction-compute，它对任意良基关系证明此等式，此处实例化于成员关系。

  (e : ∀ x → (∀ y → y ∈ᵗ x → P y) → P x) (x : V ℓ)
  → ∈-induction e x ≡ e x (λ y _ → ∈-induction e y)
∈-induction-compute = WellFoundedInduction.WFI.induction-compute regularityV

小结

层级 V 是一个高阶归纳类型：集合是小族的像，整个类型是 h-集合。构成结构 𝒮ᵥ 后，它以路径类型为等词、以原生 ∈ 为成员关系，二者都是命题值。外延性 (extensionalV) 经小成员关系桥从外延路径构造子得到，成员关系的良基性 (regularityV) 由消去到可及性得到。良基性又给出不可反性，以及递归原理 ∈-induction 及其计算法则 ∈-induction-compute。小成员关系 ∈ₛ 及其与 ∈ 的桥接，将在「集合的小呈现」一章处理。