L 内部的基数与编码单射

讨论 L 内部的基数，需要区分两种相互关联的比较。宿主可以用实际函数比较集合的小呈现类型；在 L 内部作出的陈述，则必须由本身可构造的图来见证。本章同时发展这两种概念，并明确保留它们的逻辑强度：具体函数与图码携带数据，后文所用的基数比较则只保留存在性。

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

论证在基础词汇章所介绍的宿主语言中进行。它唯一的经典资源，是对 Type (ℓ-suc ℓ) 中命题的排中律。这是一条受宇宙层级限制的假设，并非不受限制的排中律或选择原理。单射与图码的定义本身并不选取见证；经典推理在构造序数良序，以及后文利用该良序寻找最小元时才发挥作用。

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

因此，宇宙层级和这份排中律实例都明列为整章的参数。下面每项构造都相对于同一个 lem，途中不再加入其他公理。本章的目标是为后续基数论证准备精确的概念与有界次序，而不是已经断言基数代表或后继基数的存在。

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

后文始终同时涉及两种数学环境。累积层级提供外围集合以及取命题值的隶属关系；可构造模型则提供属于 L 的集合，以及在这些集合上解释的关系。基本事实 a ∈ sucV a 表明每个集合都属于其集合论后继 a ∪ {a}，它稍后会为一次有界搜索提供一个特定点。

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( self∈sucV )

每个外围集合还有一个典范的小呈现。呈现中的索引指名该集合的全部成员，member 把索引化为隶属证明，fiber 则从隶属恢复索引。有序对使一个集合能够表示关系。在可构造一侧，模型元素把外围集合与其属于 L 的证书配成一对；L 的传递性又把可构造性从集合传给它的每个成员。这些事实将把小呈现与可构造的图码联系起来。

open import V.Presentation {ℓ} using ( member; fiber )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )

有界搜索将使用序数隶属关系在呈现上诱导的严格良序。它的三歧性最终使用 lem，良基性则来自外围隶属关系的正则性。另一些材料在对象语言中描述图的性质：单值性、恰当定义域与单射性。稍后用命题截断隐藏具体图码时，区分这些序论材料与逻辑材料十分重要。

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.SquareLaw {ℓ} lem using ( ordSWO )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ} using ( SWO; module SWO )
open import L.Coding.Model {ℓ} using ( svAt; domAt )
open import L.Coding.Injection {ℓ} lem using ( injAt )

对集合 a，以 ⟪ a ⟫ 表示索引其成员的小类型，以 ⟪ a ⟫↪ 表示把索引送到其所指成员的映射。集合论后继 sucV a 包含 a 的每个成员，也包含 a 本身。因此，当 a 是序数时，⟪ sucV a ⟫ 是一个小搜索空间，其中既有指名所有更小序数的索引，也有指名 a 的索引。

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

本书常用命题截断有意减弱存在性。∥ X ∥₁ 的元素断言 X 有元素，却不透露具体元素。它可以消去到命题，例如用来表达反驳的空类型，却不能消去到任意数据。这条规则稍后会把 InjCode 中的具体图信息与 InjL 所断言的单纯存在严格区分开来。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

下面的记号标明一条陈述属于哪种环境。对外围结构，_∈ˢ_ 是层级中裸集合之间取命题值的隶属关系。与此相对，S 是可构造结构的载体；元素 a : S 由底层外围集合 fst a 与其可构造性的命题值证书组成。因此，⟨ fst x ∈ˢ fst a ⟩ 是关于底层外围集合的宿主层命题，而对 x : S 的量化只遍历可构造集合。对象语言的语法则通过下面引入的满足关系另行进入。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ using ( S )

可构造结构还带有取命题值的逐点包含关系。⟨ a ⊆ˢ b ⟩ 的证明对每个 x : S，把 x 属于 a 的证明送到 x 属于 b 的证明；其中的量化因此遍历可构造载体。L 的传递性保证这与底层集合通常的包含读法一致。当 a 与 b 都是序数时，这正是它们的非严格次序。因此，后继基数的最小性条款以包含为结论，而严格比较则用隶属关系表达。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( _⊆ˢ_ )

满足记号 _⊨_ 固定表示可构造结构中的解释。在判断 γ ⊨ φ 中，环境 γ 列出 S 的元素，所以 φ 中的无界量词遍历可构造集合。这正是 InjCode 前三个条件的语义内容；它们是在 L 内部成立的对象语言陈述，尽管其证明由宿主处理。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

首先在宿主层定义单射。X ↪ Y 的元素由函数 f : X → Y 及其单射性证明组成；该证明表明，f x 与 f y 相等便推出 x 与 y 相等。函数是可以从这对数据中投影出的具体数据。定义不包含满射性或逆函数，也不涉及集合、可构造性证书、满足判断或截断。稍后，它的典型两端是两个外围集合的小呈现类型。

_↪_ : Type ℓ → Type ℓ → Type ℓ
X ↪ Y = Σ[ f ∈ (X → Y) ] ((x y : X) → f x ≡ f y → x ≡ y)

现在固定一个可构造集合 α，并假设其底层集合是序数。为了稍后寻找大小合适的序数，只需在 sucV (fst α) 的典范呈现中搜索。这个集合包含 α 的每个成员及 α 本身，所以搜索空间既是小类型，又带有一个自然起点。此处的定义只建立这个带序的搜索空间；后续论证才会给出候选谓词并执行最小元选择。

module LeastCardInjL (α : S) (oα : IsOrd (fst α)) where

第一项任务是证明这个集合论后继本身属于 L。由 oα 两次应用序数后继，可知 sucV (sucV (fst α)) 是序数。序数属于下一可构造层的定理把 sucV (fst α) 放入这个明确给出的层，而属于某一层便给出其可构造性。因此，证明指明了一个包含该后继的具体层，并未诉诸「可构造性一般地对 sucV 封闭」这样的结论。

  hSucα : ⟨ isL (sucV (fst α)) ⟩
  hSucα = Lset→isL (sucV (sucV (fst α))) (suc-ord (suc-ord oα)) (sucV (fst α))
            (ord∈Lset-suc (sucV (fst α)) (suc-ord oα))

呈现中的每个索引 m 都指名 sucV (fst α) 的一个成员。这个后继已经证明可构造，而 L 具有传递性，所以被指名的成员也可构造。于是 up 保留 m 所指名的底层集合，并附上恰好由此得到的证书，从而产生 S 的元素。它只定义在这个有界呈现上，并不会把任意外围集合变成可构造集合。

  up : ⟪ sucV (fst α) ⟫ → S
  up m = ⟪ sucV (fst α) ⟫↪ m
       , isL-trans (member (sucV (fst α)) m) hSucα

序数的隶属关系为这些索引排序。把 ordSWO 应用于序数 sucV (fst α)，便在 ⟪ sucV (fst α) ⟫ 上得到严格良序 w：它依照所指集合之间的隶属关系作比较，三歧性依赖 lem，良基性则来自正则性。把这个值声明为不透明，只控制它在后续证明中是否展开，并不改变该关系、它的定律或这些定律所依赖的假设。

  opaque
    w : SWO (⟪ sucV (fst α) ⟫)
    w = ordSWO (sucV (fst α)) (suc-ord oα)

路径 w-lt 给出这个次序的可用描述。对索引 m 与 n，「m 在 w 下先于 n」这一命题，与「m 所指集合属于 n 所指集合」这一命题相等。这是命题类型之间的相等，并非集合之间的相等。后续证明可沿这条路径双向传输证据，在索引比较与序数隶属之间往返，同时无需展开良序的构造。

  opaque
    unfolding w
    w-lt : (m n : ⟪ sucV (fst α) ⟫)
         → SWO._<∙_ w m n ≡ ⟨ ⟪ sucV (fst α) ⟫↪ m ∈ˢ ⟪ sucV (fst α) ⟫↪ n ⟩
    w-lt m n = refl

这个搜索空间有一个指名 fst α 的特定索引。证明 self∈sucV (fst α) 给出该序数属于其集合论后继，而 fiber 把这条隶属化为一个索引以及描述其像的等式。层级中的隶属虽然取命题值，但呈现映射是嵌入，所以它的纤维本身是命题；因此可以把截断消去到这个唯一纤维，而无须调用选择原理。self 是由此恢复的索引，并不是该序数。

  self : ⟪ sucV (fst α) ⟫
  self = fiber (sucV (fst α)) (self∈sucV (fst α)) .fst

伴随等式准确说明 self 指名什么：它在呈现映射下的像等于 fst α。这条相等发生在底层外围集合之间；此处没有断言相应 S 元素相等，因为那还需要处理两边的可构造性证书。self 与 self-eq 合在一起，为后续搜索提供一个可以检验 α 之性质的具体索引。

  self-eq : ⟪ sucV (fst α) ⟫↪ self ≡ fst α
  self-eq = fiber (sucV (fst α)) (self∈sucV (fst α)) .snd

内部单射与后继基数

一个具体的可构造集合 F，首先通过 L 内部的三条满足条件来编码从 a 到 b 的单射。第一条说成对形状的条目具有单值性：同一输入不能有两个不相等的输出。第二条说定义域恰为 a，而且包含两个方向：每个成对形状条目的第一分量属于 a，a 的每个成员则仅仅存在某个输出。第三条说图具有单射性：输出相同的两个条目必有相等的输入。在三条判断中，环境都把 F 放在第一项、a 放在第二项，所有无界量词都遍历 S。

InjCode : S → S → S → Type (ℓ-suc ℓ)
InjCode F a b =
    ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩

第四条条件直接在宿主中陈述。对任意 x,y : S，若它们的底层集合组成的有序对属于底层图，则底层输出属于 b。因此，b 是所有取值的陪域上界；条件并不说 b 的每个成员都被取到。InjCode 也没有断言 F 的每个成员都是有序对。它的条件只检查成对形状的成员，所以其他形状的附加成员不会影响从图码读出的函数。这个宿主层的值域约束必须与前三条对象语言满足判断区分开来。

  × ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst b ⟩)

InjL a b 忘去是哪一个具体图满足这四条条件。它是依值对「F 与 InjCode F a b」的命题截断，所以只断言在 L 内部存在从 a 到 b 的编码单射。无法从中投影出特定图或宿主层函数。只有当目标是命题时，才能在局部分支中打开它；后续对单射作复合或变换的构造，会在这样的分支内使用图，再把所得图放回命题截断。方向也是陈述的一部分：InjL a b 本身并不蕴含 InjL b a。

InjL : S → S → Type (ℓ-suc ℓ)
InjL a b = ∥ Σ[ F ∈ S ] InjCode F a b ∥₁

当 κ 是序数时，基数性由初始性表达。冯·诺伊曼序数的每个成员 δ 都是更小的序数，而 IsCardinalL κ 反驳「存在满足 InjCode F κ δ 的可构造图」这一命题截断。用刚定义的记号说，它排除 InjL κ δ，并不排除 InjL δ κ。这两个都是内部编码单射的命题，不是宿主层类型 _↪_ 的实例；一般也不能从它们的截断中抽取后一种宿主层单射。这一定义也可对一般可构造集合形成，其中没有 κ 为序数的证明；后续使用处会另行提供 IsOrd (fst κ)，然后才作初始序数的解释。由于反驳以空类型为目标，所需的命题截断消去是正当的。

IsCardinalL : S → Type (ℓ-suc ℓ)
IsCardinalL κ =
  (δ : S) → ⟨ fst δ ∈ fst κ ⟩
          → (∥ Σ[ F ∈ S ] InjCode F κ δ ∥₁ → Empty.⊥)

SuccCardL δ κ 的参数次序规定，δ 是候选后继基数，κ 是它所超越的对象。前三个条款分别说：δ 的底层集合是序数，δ 满足初始性谓词，并且 κ ∈ δ；在序数语境中，最后一点表示 δ 严格大于 κ。这些条款只描述给定一对对象的性质，并不产生这样的 δ，也不要求 κ 本身是序数或基数。定义的最后一个条款还会加入全局最小性。这里没有出现 sucV：后继基数不是集合论后继 κ ∪ {κ}。

SuccCardL : S → S → Type (ℓ-suc ℓ)
SuccCardL δ κ =
    IsOrd (fst δ)
  × IsCardinalL δ
  × ⟨ fst κ ∈ fst δ ⟩

最后一个字段表达 κ 之上所有内部序数基数中的最小性。给定任意 c : S，若其底层集合是序数，满足 IsCardinalL c，且包含 κ，该字段就给出内部包含 δ ⊆ˢ c。第一个字段已经说明 δ 是序数，因此包含关系在此就是序数的非严格比较：δ 不大于每个这样的 c。结论使用包含而非成员关系，因为它还必须适用于 c 就是 δ 的情形。对 S 的量化与 _⊆ˢ_ 都作用于可构造载体，所以这是 L 中可见候选者之间的最小性。该字段对 κ 只假设 κ ∈ c；断言 κ 本身是序数和内部基数的假设，由使用这个谓词的各定理提供。

这个字段不构造任何单射图。InjCode F a b 保留一个特定的可构造码 F 及其四项单射条件，而 InjL a b 是 ∥ Σ[ F ∈ S ] InjCode F a b ∥₁ 的命题截断。因此，把假设 IsCardinalL c 与 c 的序数性合在一起，它说的是：不存在从 c 到其任一较小序数成员的 InjL 单射。SuccCardL δ κ 本身是固定之对 δ, κ 的未截断性质：它既不证明合适的 δ 存在，也不选定一个 δ。后文的 succCardExists 在 κ 是序数内部基数且不是有限序数时，证明这种 δ 的命题截断存在性；所用的经典假设仍只是模块参数 LEM (ℓ-suc ℓ)。集合论后继 sucV 并未出现在这个定义中。

  × ((c : S) → IsOrd (fst c) → IsCardinalL c → ⟨ fst κ ∈ fst c ⟩
             → ⟨ δ ⊆ˢ c ⟩)