传递良基关系的塌缩

一个关系自身能携带多少集合论结构？取带良基传递关系 _≺_ 的小类型 A，该关系取值于 Type ℓ。Mostowski 的回答是：仅凭这个关系，就能用递归确定一个函数 col : A → SV.S，满足

col p = { col r | r ≺ p }，

即每个点被送到其前驱的塌缩值所成的集合。一条计算律刻画每个值中的隶属关系，而关系的传递性使每个塌缩值成为这里所说的序数，即自身传递且每个成员也传递。

一个有限的例子可以展示机制。取三点 s、r、p，有 s ≺ r、r ≺ p，以及传递性所要求的 s ≺ p，且无其他关系。递归没有强制 col s 的任何成员，col r = { col s }，col p = { col s, col r }，这正是 von Neumann 的 0、1、2 图景。递归从不检视点本身，只检视它们的前驱锥。

设定的三个特征决定其后的一切。其一，A 与每个纤维 x ≺ y 都在 Type ℓ 中，故对每个 p，前驱锥是小类型 Σ[ r ∈ A ] (r ≺ p)；层级 V 的 sett 构造子恰好把这样的小族变成 SV.S 中的集合。其二，sett 集合中的隶属按构造就是命题截断：⟨ b ∈ˢ a ⟩ 说的是纯粹存在该族的某个索引，使族在该处的值等于 b，而非选定的索引可得。因此本章在一个方向上从给出的数据证明隶属 (r ≺ p 给出 col r ∈ˢ col p)，在另一方向上只得到纯粹存在的前驱加一条塌缩值等式。其三，之后消去的目标都是命题，如集合间的等式或 isTransV x，故向它们消去截断是合法的。这里没有对 _≺_ 的外延性假设，前驱锥相同的两点不被区分：塌缩是典范的，但并不声称单射。整个构造只用良基递归与传输；这里没有假设任何经典原理。

塌缩落在累积层级的集合层载体中，因此其输出由真正的集合构成，而非 A 的点。该载体在下文记作 SV.S；它是 h-集合，也就是任意两元素之间的相等类型都是命题。其成员关系 _∈ˢ_ 把每条隶属陈述打包成一个 hProp：底层类型 ⟨ b ∈ˢ a ⟩ 连同该类型为命题的证明。因此，隶属与传递性都可以直接用层级自身的关系陈述。

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

open import Base.Prelude

module L.Mostowski {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

构造由两个要素驱动。其一是层级的像运算 sett：从小索引类型 X 和族 X → V ℓ 造出该族取值的集合，隶属仅在某个索引命中目标时纯粹地成立。其二是良基性证书 WellFounded _≺_，即 A 的每个元素沿 ≺ 可及；其归纳原理构造递归定义的函数，配套的计算律记录该函数在每点的行为。命题截断经由 ∥ _ ∥₁ 与其引入 ∣ _ ∣₁ 进入，因为像中的隶属按设计就是截断的。序数目标 IsOrd、传递性 isTransV 及其命题性证明 isPropIsTransV 来自 L 的构造，只在最后定理需要它们时出现。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; isTransV; isPropIsTransV )

open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.Induction.WellFounded using ( WellFounded; module WFI )
import Cubical.HITs.PropositionalTruncation as PT

层级结构的等词与隶属关系取值于层级 ℓ-suc ℓ 的 hProp。另一方面，A 与每个纤维 x ≺ y 都在 Type ℓ 中，所以每个前驱锥都是可供 sett 使用的小索引类型。构造只需要这些大小事实，不需要排中律。

open PT using ( ∣_∣₁; ∥_∥₁ )

module SV = hPropStructure 𝒮ᵥ
open SV using ( _∈ˢ_ )

下面完成两个任务。首先证明塌缩的两条隶属律：给定一个前驱即可构造相应成员，而从一个成员反推时，只能得到纯粹存在的前驱及其塌缩值等式。随后在良基归纳中使用这两条定律，证明每个 p 都满足 IsOrd (col p)。显式输入与截断输出之间的不对称在两步中都不可省略。

良基性为递归提供依据。由 wf 得到的归纳原理说：要在 A 上定义一族 P，只需对每个 p，从所有前驱 r ≺ p 处 P 的值构造 P p。传递性见证 ≺-trans 不参与 col 的定义；它在随后证明所得集合传递时才使用。

module Mostowski (A : Type ℓ) (_≺_ : A → A → Type ℓ)
                 (wf : WellFounded _≺_)
                 (≺-trans : {x y z : A} → x ≺ y → y ≺ z → x ≺ z) where

  module W = WFI wf using ( induction; induction-compute )

  colStep : (p : A) → (∀ r → r ≺ p → SV.S) → SV.S

递归步就是前驱锥的像。给定 p 和已经知道每个 r ≺ p 的 col r 的递归调用 rec，该步造出 sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z))：索引类型是偶对 (r , r ≺ p) 的全空间，族把这样的偶对送到 rec r。抽象地说，这正是本章宣告的塌缩方程 { col r | r ≺ p }。注意步型对任意的步函数 rec 做了量化，这使同一份数据既用于定义，也经由下面的计算律用于推理。

  colStep p rec = sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z))

  opaque
    col : A → SV.S
    col = W.induction {P = λ _ → SV.S} colStep

    col-eq : (p : A) → col p ≡ sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → col (fst z))

函数 col 由良基归纳定义。其计算律 col-eq 把 col p 等同于前驱锥在 col 下的像。随后的隶属证明用这条等式在递归定义的值与显式像之间转换，而在显式像中，隶属具有 sett 给出的截断原像分类。

    col-eq = W.induction-compute colStep

  col-in : (p r : A) → r ≺ p → ⟨ col r ∈ˢ col p ⟩
  col-in p r rp =
    subst (λ v → ⟨ col r ∈ˢ v ⟩) (sym (col-eq p)) ∣ (r , rp) , refl ∣₁

  col-out : (p : A) (b : SV.S) → ⟨ b ∈ˢ col p ⟩

隶属在两个方向上各有一条计算律，且两者有意味深长的不对称。正向：若给定 r ≺ p，则 col r 是 col p 的成员。其见证是偶对 (r , rp) 连同记录 col r 在索引 r 处被命中的路径 refl；沿 col-eq p 传输 (取 sym 形式，因为方程是按另一方向证明的) 把这个显式像的成员移入类型 ⟨ col r ∈ˢ col p ⟩。反向：任意的隶属 ⟨ b ∈ˢ col p ⟩ 只给出截断的陈述：纯粹地存在某个 r ≺ p 使 col r ≡ b。证明沿 col-eq p 把隶属传输回显式像中的隶属；该隶属按构造就是截断的原像，再把索引数据改写为带等式的前驱。这里没有任何一步选定具体的 r；截断 ∥ _ ∥₁ 忠实记录了隶属所能揭示的信息。

          → ∥ Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ b)) ∥₁
  col-out p b b∈ =
    PT.map (λ z → fst (fst z) , snd (fst z) , snd z)
      (subst (λ v → ⟨ b ∈ˢ v ⟩) (col-eq p) b∈)

  col-ord : (p : A) → IsOrd (col p)

最后的定理说每个塌缩值都是序数，其中 IsOrd (col p) 展开为一对：col p 传递，且其每个成员都传递。证明对 p 做良基归纳，故归纳假设 rec 对每个前驱 r ≺ p 提供 IsOrd (col r)，目标由其两个分量组装。这是假设 ≺-trans 发挥作用的地方；在阅读两个子句之前，先想象三点链 s ≺ r ≺ p：关系的传递性正是让关于 col r 的隶属事实能在 col p 内重演的关键。

  col-ord = W.induction {P = λ p → IsOrd (col p)} ih
    where
    ih : (p : A) → (∀ r → r ≺ p → IsOrd (col r)) → IsOrd (col p)
    ih p rec = tr , mem
      where

第一个子句说 col p 的每个成员都传递。证明从 col-out p x x∈ 出发：成员 x 是某个纯粹存在的前驱 r ≺ p 的 col r，并带等式 e : col r ≡ x。归纳假设提供 isTransV (col r)，subst isTransV e 沿该等式把这一证明传送到类型 isTransV x。截断消去合法，因为目标 isTransV x 是命题，由 isPropIsTransV x 证明；这里没有抽取见证，只是从纯粹存在的情形分析中确立一个命题。

      mem : (x : SV.S) → ⟨ x ∈ˢ col p ⟩ → isTransV x
      mem x x∈ = PT.rec (isPropIsTransV x)
        (λ z → subst isTransV (snd (snd z)) (rec (fst z) (fst (snd z)) .fst))
        (col-out p x x∈)
      tr : isTransV (col p)

第二个子句证明 col p 自身传递：给定 y ∈ x 与 x ∈ col p，要证 y ∈ col p。先把 x ∈ col p 经 col-out 剥开，纯粹地得到某个 r ≺ p 使 col r ≡ x。该等式把已给的 y ∈ x 传输入 ⟨ y ∈ˢ col r ⟩，运行示例中的中间环节 r 正是在这里把链条两端接了起来。

      tr {x} {y} y∈x x∈col = PT.rec (snd (y ∈ˢ col p)) outer (col-out p x x∈col)
        where
        outer : Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ x)) → ⟨ y ∈ˢ col p ⟩
        outer (r , rp , e) =
          PT.rec (snd (y ∈ˢ col p)) inner

现在链条闭合。从 y ∈ col r 出发，在 r 处应用 col-out 纯粹地给出某个 s ≺ r 使 col s ≡ y；记其等式为 e2。关系传递性把 s ≺ r 与 r ≺ p 复合成 s ≺ p，col-in p s 把 col s 提升为 col p 的成员。最后沿 e2 用 subst 在隶属目标中把 col s 换成 y，得到 ⟨ y ∈ˢ col p ⟩。两次截断消去都落在命题 ⟨ y ∈ˢ col p ⟩ 中，整个论证只用良基递归、传输和传递性假设：本章任何地方都没有经典原理进入。

            (col-out r y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x))
          where
          inner : Σ[ s ∈ A ] ((s ≺ r) × (col s ≡ y)) → ⟨ y ∈ˢ col p ⟩
          inner (s , sr , e2) =
            subst (λ v → ⟨ v ∈ˢ col p ⟩) e2 (col-in p s (≺-trans sr rp))