为序数选取基数代表

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

L 内部的计数以基数表述，而具体构造往往只产生任意序数。对 L 中的序数 α，本章找出包含于 α 的内部基数 μ，并给出两个方向的内部单射。因此，μ 在模型内部代表 α 的基数。构造在 α 的后继中搜索，选取 α 能够内部单射到的最小序数。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.GCH.CardinalRepresentative {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

假设在层级 ℓ-suc ℓ 上成立排中律。良序搜索与序数三分法都会使用这个假设。结论中的单射全部位于 L 内部：它们由可构造的图见证，并非外部函数。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Presentation {ℓ} using ( member; fiber )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL; isL-trans )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )

这里同时出现两个结构。外围层级提供成员关系以及搜索所用的小呈现；可构造结构提供序数、基数与内部单射谓词。可构造性沿成员关系向下传递，所以在外围层级中找到的成员可以重新进入 L 的论域。

open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL; module LeastCardInjL )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( IsLeast; leastOf; module SWO )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )

搜索建立在呈现序数的索引良序之上；这个次序与所指元素之间的成员关系一致。包含关系的编码把包含化为内部单射，单射的传递性则复合连续的内部单射。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )

候选集合取为后继 sucV α。命题截断表达适当代表的存在，而不在外部选择一个代表；和类型与空类型用于后面的三分法论证。

open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( inl; inr )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

以 SV.S 表示外围集合，以 SL.S 表示可构造集合。SL.S 的元素由外围集合及其可构造性证书组成。成员关系比较作用于第一分量，而 InjL 与 IsCardinalL 以完整的可构造元素为对象。

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

给定序数 α，定理仅仅断言存在满足五项性质的 μ：μ 是序数，是内部基数，满足 μ ⊆ α，并且存在内部单射 α ↪ μ 与 μ ↪ α。截断使整个结论成为命题。

cardOf :
    (α : SL.S) → IsOrd (fst α)
  → ∥ Σ[ μ ∈ SL.S ]
       ( IsOrd (fst μ) × IsCardinalL μ

最终见证由代表 μ 与下面构造的五项证明组成。由于目标已经截断，只要这些分量齐备，放入这个依值对即可完成定理。

       × ((z : SV.S) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩)
       × InjL α μ × InjL μ α ) ∥₁

关于 α 的辅助搜索准备提供后继的可构造性、指名 α 自身的索引及相应等式，还提供呈现索引上的良序 w。w 的次序关系就是所指序数之间的成员关系。

cardOf α oα = ∣ μ , oμ , cardμ , μ⊆α , α↪μ , μ↪α ∣₁
  where
  module LC = LeastCardInjL α oα using ( hSucα; self; self-eq; w; w-lt )

令 T 为序数 α 的底层集合的后继。后继仍是序数，因此 T 的每个成员都是序数，搜索全程都可使用由成员关系给出的次序。

  T : SV.S
  T = sucV (fst α)

  oT : IsOrd T
  oT = suc-ord oα

集合 T 是可构造的。这个证书不可或缺，因为搜索索引最初只指名 T 的外围成员；可构造性的向下封闭把该成员化为 SL.S 的元素。

  opaque
    hT : ⟨ isL T ⟩
    hT = LC.hSucα

对 T 的呈现索引 b，upL b 把所指成员与其可构造性证明配成依值对。后一个证明由该成员属于 T 以及 T 的可构造性得到。

  upL : ⟪ T ⟫ → SL.S
  upL b = ⟪ T ⟫↪ b , isL-trans (member T b) hT
  Good : ⟪ T ⟫ → hProp (ℓ-suc ℓ)
  Good b = ∥ Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ b) × InjL α δ) ∥₁ , squash₁

若索引 b 所指的成员是某个可构造集合 δ 的底层集合，并且存在内部单射 α ↪ δ，就称 b 为好索引。Good b 中的等式连接索引呈现与可构造见证，截断则使好索引性取值于命题。

  selfGood : ⟨ Good LC.self ⟩
  selfGood = ∣ α , sym LC.self-eq , inclusion-coded α α (λ z z∈α → z∈α) ∣₁

  nonempty : ∥ Σ[ b ∈ ⟪ T ⟫ ] ⟨ Good b ⟩ ∥₁
  nonempty = ∣ LC.self , selfGood ∣₁

指名 α 的索引是好的：它所指成员等于 α，恒等包含则编码出从 α 到自身的内部单射。因此，好索引的类型仅仅非空。

  least : Σ[ b ∈ ⟪ T ⟫ ] IsLeast LC.w Good b
  least = leastOf LC.w lem Good nonempty

  m : ⟪ T ⟫
  m = fst least

对良序 w 与命题值谓词 Good 应用最小元搜索。排中律判定好索引性，非空性保证存在最小的好索引；把它记作 m。

  μ : SL.S
  μ = upL m

  μ∈T : ⟨ fst μ ∈ˢ T ⟩
  μ∈T = member T m

把选中的索引 m 提升到可构造论域，并把所得元素记作 μ。依定义，μ 的底层集合就是 m 在 T 中指名的成员。

  oμ : IsOrd (fst μ)
  oμ = mem-ord {A = T} oT (fst μ) μ∈T

呈现定理给出 μ ∈ T。由于 T 是序数，其每个成员仍是序数，所以 μ 具有所需的序数性。

  α↪μ : InjL α μ
  α↪μ = PT.rec squash₁ from (fst (snd least))
    where
    from : Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ m) × InjL α δ) → InjL α μ

最小索引的好索引性在截断之下给出可构造集合 δ、其底层集合与 m 所指成员之间的等式，以及单射 α ↪ δ。目标 InjL α μ 是命题，所以可以把截断见证消去到这个目标中。

    from (δ , e , α↪δ) =
      injl-trans α δ μ α↪δ
        (inclusion-coded δ μ (λ z z∈δ → subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈δ))

沿索引等式搬运可知 δ 包含于 μ；包含关系的编码把它化为内部单射 δ ↪ μ。再与已有的 α ↪ δ 复合，便得到 α ↪ μ。

  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = snd (snd least) b bGood b<m
    where
    δ∈T : ⟨ fst δ ∈ˢ T ⟩
    δ∈T = oT .fst {x = fst μ} {y = fst δ} δ∈μ μ∈T

为证明 μ 是基数，假设某个成员 δ ∈ μ 允许内部单射 μ ↪ δ。序数 T 的传递性给出 δ ∈ T，于是 T 的呈现产生一个指名 δ 的索引 b。

    b : ⟪ T ⟫
    b = fiber T δ∈T .fst
    bδ : ⟪ T ⟫↪ b ≡ fst δ

纤维定理同时给出索引 b 以及把它所指成员识别为 δ 的等式。这些数据使成员关系与单射陈述可以在索引成员和可构造元素 δ 之间搬运。

    bδ = fiber T δ∈T .snd
    bGood : ⟨ Good b ⟩
    bGood = ∣ δ , sym bδ , injl-trans α μ δ α↪μ μ↪δ ∣₁

索引 b 是好的：把 α ↪ μ 与假设的 μ ↪ δ 复合，再用纤维等式匹配索引所指的成员。于是 b 是同一次搜索中的另一个候选。

    b<m : SWO._<∙_ LC.w b m
    b<m = transport (λ i → sym (LC.w-lt b m) i)
            (subst (λ z → ⟨ z ∈ˢ fst μ ⟩) (sym bδ) δ∈μ)

而且 b < m。良序 w 的关系就是所指序数之间的成员关系，假设 δ ∈ μ 搬运后恰好给出这个比较。最小好索引之下不可能再有好索引，所以这样的单射 μ ↪ δ 不存在；因此 μ 是内部基数。

  μ⊆α : (z : SV.S) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩
  μ⊆α = go (ord-tri (fst μ) oμ (fst α) oα)
    where
    go : Tri (fst μ) (fst α) → (z : SV.S) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩

还需证明 μ ⊆ α。序数三分法比较二者的底层序数。若 μ ∈ α，由 α 的传递性得到包含；若 μ = α，沿等式搬运即可。

    go (inl μ∈α)       z z∈μ = oα .fst z∈μ μ∈α
    go (inr (inl e))   z z∈μ = subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈μ

第三种情形 α ∈ μ 与最小性矛盾。指名 α 的索引是好的，而 α ∈ μ 表明这个索引在良序 w 中严格位于 m 之前。因此只剩三分法的前两种情形。

    go (inr (inr α∈μ)) z z∈μ =
      Empty.rec (snd (snd least) LC.self selfGood
        (transport (λ i → sym (LC.w-lt LC.self m) i)
          (subst (λ v → ⟨ v ∈ˢ fst μ ⟩) (sym LC.self-eq) α∈μ)))

包含 μ ⊆ α 编码出内部单射 μ ↪ α。连同 α ↪ μ 以及 μ 的序数性和基数性，这就完成了所承诺的代表。此后关于序数大小的论证可以在不离开 L 的前提下转到这个内部基数上。

  μ↪α : InjL μ α
  μ↪α = inclusion-coded μ α μ⊆α

代表 μ 是一个序数基数；它可以内部单射到 α，α 也可以内部单射到它，并且包含于 α。由此，任意可构造序数上的基数算术都可以化归为内部基数上的基数算术。