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

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

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

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

open import Base.Prelude

module V.Hierarchy {ℓ : Level} where

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

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

```agda
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` 表示视为相等，这是内建于类型本身的外延性。这个类型并非在本章定义；本章在其上构造结构 `𝒮ᵥ`，并证明该结构的集合论性质。

```agda
  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-集合而言，两个元素之间的路径类型本来就是命题，字段只是把这个类型连同它所附带的证书一起记录下来。

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

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

```agda
  ; _∈ˢ_   = _∈_ }

open hPropStructure 𝒮ᵥ
```

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

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

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

```agda
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` 所需双向包含的向前分量。

```agda
      (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` 给出可及性。

```agda
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`。整个证明由此用到索引，却从未全局选定一个索引。

```agda
           y∈))
```

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

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

```agda
∈-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` 在这条良基关系上实例化，把步进函数变为全定义的族。此处无需重新证明良基性。

```agda
∈-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`，它对任意良基关系证明此等式，此处实例化于成员关系。

```agda
  (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`。小成员关系 `∈ₛ` 及其与 `∈` 的桥接，将在「集合的小呈现」一章处理。