泛等结构集合论 (4) 序数的定义及其泛等原理

泛等结构集合论 (4) 序数的定义及其泛等原理

交流Q群: 893531731
本文源码: Ordinal.Base.lagda.md
高亮渲染: Ordinal.Base.html

本章将复刻质料集合论的重要概念: 序数.

{-# OPTIONS --cubical --safe #-}
{-# OPTIONS --lossy-unification #-}
{-# OPTIONS --hidden-argument-puns #-}

module Ordinal.Base where
open import Preliminary

序关系的一些性质

说白了, 一个序数就是由一个集合以及该集合上的一个满足一定性质的序关系所组成的结构. 我们先定义这个序关系需要满足的性质.

给定类型 A : Type 𝓊 及其上的序关系 _≺_ : A → A → Type 𝓋

module BinaryRelation {A : Type 𝓊} (_≺_ : A → A → Type 𝓋) where

命题性

我们说 _≺_ 是一个 命题 (propositional) 关系, 当且仅当对任意 x y : A, x ≺ y 是一个命题.

  Propositional : Type _
  Propositional = ∀ x y → isProp (x ≺ y)

命题性本身是一个命题.

  isPropPropositional : isProp Propositional
  isPropPropositional = isPropΠ2 λ _ _ → isPropIsProp

反自反性

我们说 _≺_ 是一个 反自反 (irreflexive) 关系, 当且仅当对任意 x : A, x ⊀ x.

  _⊀_ : A → A → Type 𝓋
  x ⊀ y = ¬ x ≺ y

  Irreflexive : Type _
  Irreflexive = ∀ x → x ⊀ x

反自反性是一个命题.

  isPropIrreflexive : isProp Irreflexive
  isPropIrreflexive = isPropΠ2 λ _ _ → isProp⊥

传递性

我们说 _≺_ 是一个 传递 (transitive) 关系, 当且仅当对任意 x y z : A, x ≺ y 与 y ≺ z 蕴含 x ≺ z.

  Transitive : Type _
  Transitive = ∀ x y z → x ≺ y → y ≺ z → x ≺ z

如果_≺_ 是一个命题关系, 那么传递性是一个命题.

  isPropTransitive : Propositional → isProp Transitive
  isPropTransitive prop = isPropΠ5 λ _ _ _ _ _ → prop _ _

外延性

我们说 _≺_ 是一个 外延 (extensional) 关系, 当且仅当对任意 x y : A, 如果对任意 z : A 都有 z ≺ x 当且仅当 z ≺ y, 那么 x ≡ y.

  Extensional : Type _
  Extensional = ∀ x y → (∀ z → z ≺ x ↔ z ≺ y) → x ≡ y

如果 A 是集合, 那么外延性是命题.

  isPropExtensional : isSet A → isProp Extensional
  isPropExtensional A-set = isPropΠ3 λ _ _ _ → A-set _ _

引理 如果 _≺_ 同时具有命题性和外延性那么 A 是集合.
证明梗概 由引理 Collapsible≡→isSet, 只要证明 A 上的相等类型 x ≡ y 可折叠, 就证明了 A 是集合. 可折叠是说能构造 x ≡ y 的自映射 f 且 f 是一个 2-常函数 (∀ x y → f x ≡ f y). 只要用作为自变量的那个 eq : x ≡ y 替换外延性的前提 z ≺ x ↔︎ z ≺ y 就能得到另一个 x ≡ y. 由于 _≺_ 是命题, 所以 z ≺ x ↔︎ z ≺ y 是命题, 所以 f 是 2-常函数. ∎

  open import Cubical.Foundations.Function using (2-Constant)
  open import Cubical.Relation.Nullary using (Collapsible; Collapsible≡→isSet)

  Extensional→isSet : Propositional → Extensional → isSet A
  Extensional→isSet prop ext = Collapsible≡→isSet λ x y → collapser x y , didCollapse x y
    where
    collapser : ∀ x y → x ≡ y → x ≡ y
    collapser x y eq = ext x y λ z → →: (subst (z ≺_) eq) ←: (subst (z ≺_) (sym eq))
    didCollapse : ∀ x y → 2-Constant (collapser x y)
    didCollapse x y p q = cong (ext x y) $ funExt λ _ → isProp↔ (prop _ _) (prop _ _) _ _

可及性

我们说在 _≺_ 关系下, 一个 x : A 可及 (accessible), 当且仅当对任意 y ≺ x, y 也可及.

  data Acc (x : A) : Type (𝓊 ⊔ 𝓋) where
    acc : (∀ y → y ≺ x → Acc y) → Acc x

可及性是一个命题. 下面的证明中暴露了 cubical 的底层机制, 就是那个间点 i, 以使证明更简洁. 也可以不暴露, 只需证 H₁ 等于 H₂, 它们都具有 ∀ y → y ≺ x → Acc y 类型. 由归纳假设, Acc y 是命题, 所以这个Π类型也是命题, 所以它的两个项 H₁ 与 H₂ 相等.

  isPropAcc : ∀ x → isProp (Acc x)
  isPropAcc x (acc IH₁) (acc IH₂) i = acc λ y y≺x → isPropAcc y (IH₁ y y≺x) (IH₂ y y≺x) i

可及性的消去规则 acc-elim 可以看作是数学归纳法的更一般形式, 它说如果对任意 x 我们都能通过证明任意 y ≺ x 有 P y 来证明 P x, 那么任意可及的 x 都有 P x.

  acc-elim : {P : A → Type 𝓌} → (∀ x → (∀ y → y ≺ x → P y) → P x) → ∀ x → Acc x → P x
  acc-elim {P} H = aux where
    aux : ∀ x → Acc x → P x
    aux x (acc IH) = H x λ y y≺x → aux y (IH y y≺x)

有时我们还要用到双参数形式的消去规则.

  acc-elim2 : {R : A → A → Type 𝓌}
    → (∀ x y → (∀ u v → u ≺ x → v ≺ y → R u v) → R x y)
    → ∀ x y → Acc x → Acc y → R x y
  acc-elim2 {R} H = aux where
    aux : ∀ x y → Acc x → Acc y → R x y
    aux x y (acc IHx) (acc IHy) = H x y λ u v u≺x v≺y → aux u v (IHx u u≺x) (IHy v v≺y)

良基性

我们说 _≺_ 是一个 良基 (well-founded) 关系, 当且仅当任意 x : A 都可及.

  WellFounded : Type _
  WellFounded = ∀ x → Acc x

良基性也是一个命题.

  isPropWellFounded : isProp WellFounded
  isPropWellFounded = isPropΠ λ _ → isPropAcc _

在 acc-elim 的基础上, 以良基性取代 x 的可及条件, 就得到了良基关系的消去规则 wf-elim.

  wf-elim : {P : A → Type 𝓌} → WellFounded → (∀ x → (∀ y → y ≺ x → P y) → P x) → ∀ x → P x
  wf-elim wf H x = acc-elim H x (wf x)

  wf-elim2 : {R : A → A → Type 𝓌} → WellFounded →
    (∀ x y → (∀ u v → u ≺ x → v ≺ y → R u v) → R x y) → ∀ x y → R x y
  wf-elim2 wf H x y = acc-elim2 H x y (wf x) (wf y)

注意这里说的 P 指任意以 A 为索引的类型 A → Type 𝓌. 把 P 看作谓词, wf-elim 可以看作是一种归纳法.

用常函数实例化 P , wf-elim 则可以看作是一种递归原理.

  wf-rec : {B : Type 𝓌} → WellFounded → (∀ x → (∀ y → y ≺ x → B) → B) → A → B
  wf-rec = wf-elim

由良基消去可以立即证明良基性蕴含反自反性.

  WellFounded→Irreflexive : WellFounded → Irreflexive
  WellFounded→Irreflexive wf = wf-elim wf λ x IH x≺x → IH x x≺x x≺x

良序性

我们说 _≺_ 是一个 良序 (well-ordered) 关系, 当且仅当: _≺_ 有命题性, 传递性, 外延性和良基性.

  record WellOrdered : Type (𝓊 ⊔ 𝓋) where
    constructor mkWellOrdered
    field
      ≺-prop    : Propositional
      ≺-trans   : Transitive
      ≺-ext     : Extensional
      ≺-wf      : WellFounded

良序关系是反自反的, 且其底层类型必是集合, 我们今后称之为底集 (underlying set). 经典数学里面一般是把这里的外延性换成了三歧性, 但在直觉主义中外延性更容易处理. 此外, HoTT Book 也有相应的定义, 见 Def 10.3.17, 它要求 “A 是集合”, 但这不是必须的, Escardó 首先证明了这一点

    ≺-irrefl : Irreflexive
    ≺-irrefl = WellFounded→Irreflexive ≺-wf

    underlying-set : isSet A
    underlying-set = Extensional→isSet ≺-prop ≺-ext

由于良序性里面的每个条件都是命题, 所以良序性也是一个命题.

  opaque
    isPropWellOrdered : isProp WellOrdered
    isPropWellOrdered = isOfHLevelRetractFromIso 1 WellOrderedIsoΣ $ aux
      where
      unquoteDecl WellOrderedIsoΣ = declareRecordIsoΣ WellOrderedIsoΣ (quote WellOrdered)
      aux : ∀ x y → x ≡ y
      aux x _ = ΣPathP (isPropPropositional _ _
              , ΣPathP (isPropTransitive ≺-prop _ _
              , ΣPathP (isPropExtensional underlying-set _ _
              , isPropWellFounded _ _)))
        where open WellOrdered (Iso.inv WellOrderedIsoΣ x)

序数的定义

为了方便 𝒮ᴰ-Record 宏处理, 我们遵循 cubical 库的做法, 先用 record 类型定义序数结构, 然后用Σ类型把序数定义为类型宇宙配备上序数结构.

序数结构

一个类型 A 配备上一个良序 _≺_ 就构成了一个序数结构 OrdStr. 注意我们这里让 _≺_ 与底集 A 居留于同一宇宙, 这可以让形式更简单, 反正 _≺_ 是命题, 而我们有 PR 可以随时降级命题宇宙.

record OrdStr (A : Type 𝓊) : Type (𝓊 ⁺) where
  constructor mkOrdStr
  open BinaryRelation
  field
    _≺_ : A → A → Type 𝓊
    ≺-wo : WellOrdered _≺_
  open WellOrdered ≺-wo public

我们有序数底层结构的良基消去及其计算规则.

  elim : {P : A → Type 𝓌} → (∀ x → (∀ y → y ≺ x → P y) → P x) → ∀ x → P x
  elim = wf-elim _≺_ ≺-wf

  elim2 : {R : A → A → Type 𝓌} → (∀ x y → (∀ u v → u ≺ x → v ≺ y → R u v) → R x y) → ∀ x y → R x y
  elim2 = wf-elim2 _≺_ ≺-wf

  rec : {B : Type 𝓌} → (∀ x → (∀ y → y ≺ x → B) → B) → A → B
  rec = elim

序数宇宙

类型宇宙配备上序数结构就构成了序数宇宙 Ord. 注意 Ord 后面跟的 𝓊 指的是底集所在的宇宙, 而 Ord 本身位于 𝓊 ⁺ 宇宙.

Ord : (𝓊 : Level) → Type (𝓊 ⁺)
Ord 𝓊 = TypeWithStr 𝓊 OrdStr

我们今后都用 α β γ 等符号表示序数.

variable α β γ δ : Ord 𝓊

底集

我们用 ⟨ α ⟩ 表示序数的底集, 可以证明它确实是一个集合.

ordSet : isSet ⟨ α ⟩
ordSet {α} = OrdStr.underlying-set (str α)

底序

当同时讨论多个序数中的 ≺ 关系时, 我们用 x ≺⟨ α ⟩ y 的记法标记 ≺ 所属的序数. 我们把 ≺⟨ α ⟩ 叫做 α 的底序, 与底集相对应, 它们共同组成了一个序数的底层结构. 若把 ≺ 看作”属于”关系, ∀ z → z ≺⟨ α ⟩ x → z ≺⟨ α ⟩ y 则可以看作是”包含”关系, 记作 ≼. 但要注意这些都只是类比的说法, x 和 y 本身不是集合.

以下代码定义了一个支持 x ≺⟨ α ⟩ y 和 x ≼⟨ α ⟩ y 记法的类型类 (typeclass) Underlying.

record Underlying {𝓊} (O : Type (𝓊 ⁺)) : Type (𝓊 ⁺) where
  field
    underlyingSet : O → Type 𝓊
    underlyingRel : (α : O) → underlyingSet α → underlyingSet α → Type 𝓊
  syntax underlyingRel α x y = x ≺⟨ α ⟩ y

  underlyingPoRel : (α : O) → underlyingSet α → underlyingSet α → Type 𝓊
  underlyingPoRel α x y = ∀ z → z ≺⟨ α ⟩ x → z ≺⟨ α ⟩ y
  syntax underlyingPoRel α x y = x ≼⟨ α ⟩ y

open Underlying ⦃...⦄ public

我们对序数实装 Underlying 类型类.

instance
  underlying : Underlying (Ord 𝓊)
  underlyingSet ⦃ underlying ⦄ = ⟨_⟩
  underlyingRel ⦃ underlying ⦄ = OrdStr._≺_ ∘ str

序数等价

我们说两个序数的底集间的同伦等价 e : A ≃ B 是一个序数等价, 当且仅当 e 保持序关系. 注意这里的”保持序关系”也必须用同伦等价来表达, 今后叫它序等价, 记作 hPres≺, 定义为对任意 x y : A 有 x ≺₁ y 与 f x ≺₂ f y 同伦等价, 其中 ≺₁ 和 ≺₂ 分别是 A 和 B 上的序关系, f 是 A ≃ B 的底层函数.

module _ {A : Type 𝓊} {B : Type 𝓊′} (a : OrdStr A) (f : A ≃ B) (b : OrdStr B) where

  record IsOrdEquiv : Type (𝓊 ⊔ 𝓊′) where
    constructor mkIsOrderEquiv
    open OrdStr a renaming (_≺_ to _≺₁_)
    open OrdStr b renaming (_≺_ to _≺₂_)
    field
      hPres≺ : (x y : A) → x ≺₁ y ≃ (f ⁺¹) x ≺₂ (f ⁺¹) y

由同伦等价的命题性, “是序数等价”也是一个命题. 这是很有用的性质, 会在下一章用到.

  isPropIsOrdEquiv : isProp IsOrdEquiv
  isPropIsOrdEquiv = isOfHLevelRetractFromIso 1 IsOrdEquivIsoΣ $ aux
    where
    unquoteDecl IsOrdEquivIsoΣ = declareRecordIsoΣ IsOrdEquivIsoΣ (quote IsOrdEquiv)
    aux : ∀ x y → x ≡ y
    aux = isPropΠ2 λ _ _ → isPropΣ (isProp→ $ ≺-prop _ _) (λ _ → isPropIsEquiv _)
      where open OrdStr b

序数间的同伦等价 α ≃ₒ β 定义为保持序关系的底集间同伦等价 A ≃ B.

_≃ₒ_ : Ord 𝓊 → Ord 𝓊′ → Type (𝓊 ⊔ 𝓊′)
α ≃ₒ β = Σ f ∶ ⟨ α ⟩ ≃ ⟨ β ⟩ , IsOrdEquiv (str α) f (str β)

可以证明序数等价确实是等价关系, 由同伦等价的自反性, 对称性和传递性即得.

≃ₒ-refl : α ≃ₒ α
≃ₒ-refl = idEquiv _ , mkIsOrderEquiv λ x y → idEquiv _

≃ₒ-sym : α ≃ₒ β → β ≃ₒ α
≃ₒ-sym {α} {β} (α≃β , eqv) = invEquiv α≃β ,
  mkIsOrderEquiv λ x y → invEquiv $
    subst2 (λ u v → _ ≺⟨ α ⟩ _ ≃ u ≺⟨ β ⟩ v)
      (secIsEq (snd α≃β) x) (secIsEq (snd α≃β) y)
      (hPres≺ (α≃β ⁻¹ $ x) (α≃β ⁻¹ $ y))
  where open IsOrdEquiv eqv

≃ₒ-trans : α ≃ₒ β → β ≃ₒ γ → α ≃ₒ γ
≃ₒ-trans (α≃β , eqv₁) (β≃γ , eqv₂) = compEquiv α≃β β≃γ ,
  mkIsOrderEquiv λ x y → compEquiv
    (hPres≺ eqv₁ x y) (hPres≺ eqv₂ (α≃β ⁺¹ $ x) (α≃β ⁺¹ $ y))
  where open IsOrdEquiv

序数等价推导链记号:

infixr 2 _≃ₒ⟨_⟩_ _≃ₒ˘⟨_⟩_ _≃ₒ⟨⟩_
infix  3 _≃ₒ∎

_≃ₒ⟨_⟩_ : (α : Ord 𝓊) {β : Ord 𝓋} {γ : Ord 𝓌} → α ≃ₒ β → β ≃ₒ γ → α ≃ₒ γ
_ ≃ₒ⟨ α≃ₒβ ⟩ β≃ₒγ = ≃ₒ-trans α≃ₒβ β≃ₒγ

_≃ₒ˘⟨_⟩_ : (α : Ord 𝓊) {β : Ord 𝓋} {γ : Ord 𝓌} → β ≃ₒ α → β ≃ₒ γ → α ≃ₒ γ
_ ≃ₒ˘⟨ β≃ₒα ⟩ β≃ₒγ = ≃ₒ-trans (≃ₒ-sym β≃ₒα) β≃ₒγ

_≃ₒ⟨⟩_ : (α : Ord 𝓊) {β : Ord 𝓋} → α ≃ₒ β → α ≃ₒ β
_ ≃ₒ⟨⟩ α≃ₒβ = α≃ₒβ

_≃ₒ∎ : (α : Ord 𝓊) → α ≃ₒ α
_ ≃ₒ∎ = ≃ₒ-refl

序数的泛等原理

我们使用宏 𝒮ᴰ-Record 得到序数的泛等原理. 不需要深究其语法, 只需认为它是一种 boilerplate (样板代码), 在 cubical 的代数模块里面也被大量使用. 简而言之, 这段代码说, 序数包括两个”字段”, 一个是 _≺_, 它被同伦等价保持了, 再一个是 ≺-wo, 它是个命题, 不影响结构. 这样就可以用 𝒮ᴰ-Record 拿到 𝒮ᴰ-Ord : DUARel ... 这一串东西.

𝒮ᴰ-Ord : DUARel (𝒮-Univ 𝓊) OrdStr 𝓊
𝒮ᴰ-Ord = 𝒮ᴰ-Record (𝒮-Univ _) IsOrdEquiv
  (fields:
    data[ _≺_ ∣ autoDUARel _ _ ∣ hPres≺ ]
    prop[ ≺-wo ∣ (λ _ _ → isPropWellOrdered _) ])
  where
  open OrdStr
  open IsOrdEquiv
  open BinaryRelation

然后就可以用 ∫ 从 𝒮ᴰ-Ord 中取出序数的泛等原理: 两个序数的等价等价于它们的相等.

OrdPath : (α β : Ord 𝓊) → (α ≃ₒ β) ≃ (α ≡ β)
OrdPath = ∫ 𝒮ᴰ-Ord .UARel.ua

有了序数的泛等原理之后, 就可以在序数等价与序数相等之间相互转化, 并且这种转化是单射. 这体现了泛等基础的好处, 我们不需要商掉某个等价关系, 也不用像质料集合论那样处理良序结构与冯诺依曼集之间的编码问题. 因为我们直接把良序结构视作序数, 两个同构的良序结构保证相等.

≃ₒ→≡ : α ≃ₒ β → α ≡ β
≃ₒ→≡ = OrdPath _ _ ⁺¹

≡→≃ₒ : α ≡ β → α ≃ₒ β
≡→≃ₒ = OrdPath _ _ ⁻¹

≃ₒ→≡-inj : injective (≃ₒ→≡ {𝓊} {α} {β})
≃ₒ→≡-inj = equivFunInjective $ OrdPath _ _

≡→≃ₒ-inj : injective (≡→≃ₒ {𝓊} {α} {β})
≡→≃ₒ-inj = equivFunInjective $ invEquiv $ OrdPath _ _