The cumulative hierarchy

第三部开幕，语气随之一变。至此的模型都是假设性的：isZFModel 是一份规格书，尚无居民。本部就来交出居民，而它栖身的宇宙甚至不是本书亲手所造：cubical 库自带累积层级 V，一个沿 HoTT book 构造的高阶归纳类型。本章介绍这个类型，把它作为结构插进框架，并免费入账 record 的头两个字段。

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

open import Base.Prelude
open import Base.Truth

module V.Hierarchy {ℓ : Level} where

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

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

高阶归纳类型

生成性想法是集合论里最古老的那句话：集合无非其成员之汇集。构造子 sett 取一个小索引类型 X : Type ℓ 与一个族 ix : X → V ℓ，形成以 ix 的像为成员的集合。成员关系于是就是问原像，且仅仅是问：y ∈ sett X ix 是「存在 i : X 使 ix i ≡ y」的截断。像相同的两个族理应给出同一个集合，而在高阶归纳类型里，这句「理应」本身就是构造子：一个路径构造子 (库中名为 seteq) 让外延相等按构造成立，setIsSet 再把整个类型截断为 h-集。库文件头自陈了这笔买卖的成色：一个「ZF 减幂集」的模型。缺席的幂集与两条模式公理，正是本部余下各章必须补上的。

结构

接口严丝合缝：载体是 h-集，成员关系落在 hProp，等词径直取路径类型，由集合性打包成命题，结构章对命题侧许下的诺言在此兑现。四个字段，零适配代码，第一、二部的全部工具，语法、满足、表示、Lévy 见证、绝对性，连同模型 record 本身，即刻在 𝒮ᵥ 上可用。下标就是普通的 v，指层级。

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

open hPropStructure 𝒮ᵥ

先把层级的读法钉下，因为下一章整章围着它转：载体 V ℓ 住在 Type (ℓ-suc ℓ)，比它的索引类型高一个宇宙，真值也随之住在 hProp (ℓ-suc ℓ)。层级是由小索引数据造出的大类型。

免费入账的两个字段

模型 record 以外延与正则开篇，而层级把两者都白送。外延公理是路径构造子的兑现：字段要「逐点成员相等则相等」，库的 extensionality 要双向包含，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
      (subst ⟨_⟩ (sym (h x)) (∈∈ₛ {a = x} {b = b} .snd x∈ₛb))) )

(经 ∈∈ₛ 现身的 ∈ₛ 是库的小成员关系，下一章将细说；此处它只是胶水。)

正则公理要求成员关系良基，证明四行，全程不见公理。可及性是命题 (isPropAcc)，于是 elimProp 把 HIT 直接消去到它上面：sett X ix 的成员仅仅被 ix 截断地命中，而可及性既是命题，便沿连接路径从归纳假设搬运过来。路径构造子不产生任何义务。

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

它的第一笔红利，一行：没有集合属于自身，因为自属会构成一条无穷下降。后文诸章会不断取用。

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

沿成员关系的递归

正则性立刻付出第一笔红利。良基关系支持递归，于是库的良基归纳在成员关系上实例化：要对每个集合定义某物，只需在给定 x 各成员处取值的前提下给出 x 处的值，落点是任意类型族，递归方程命题级成立。这是不见序数的超穷递归，第四部就用它构造自己的宇宙。

∈-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 ℓ'}
  (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

小结

累积层级以高阶归纳类型的身份从库中到来：集合是小族的像，外延相等是构造子，整个类型是 h-集。𝒮ᵥ 把它插进框架，外延 (extensionalV) 与正则 (regularityV) 已然入账。尚欠的一切都住在低一层宇宙里：下一章打造为它付账的小性工具链。