序数由隶属关系线性排序

任两个序数，或一者属于另一者，或二者相等。本章把这种比较所需的经典步骤单独列出，并说明为何需要显式假设。

迄今关于序数的一切都是闭包：零是序数，后继是，并也是，上界存在。闭包陈述关乎建造；它们从不需要判定任何东西。三歧要判定。给定两个彼此之间不假设任何关系的序数，它要回答三种互斥情形中的哪一种成立，本章从显式的排中律参数取得这一判定。所以本章把排中律取作模块参数，采用基础层定下的逐层级打包形式，使用 ord-tri 的模块都显式接收这个参数。

来自环境层级的两样材料使证明比教科书版本更短。正则性给出良基归纳，而且要用两次，两个自变量各一次。外延性意味着互相包含就是相等，故相等那一情形无须另行处理。排中律既判定两个方向的包含，也判定把包含失败转成截断反例时所需的成员关系命题。

全章只在模块参数的形式下使用一条经典假设：LEM (ℓ-suc ℓ) 的一个实例。回顾基础层的形状：对每个命题 P : hProp (ℓ-suc ℓ)，它返回 ⟨ P ⟩ 的证明，或一个反驳，即从 ⟨ P ⟩ 映入空类型的映射。这个层级恰好匹配 ⊆ᵇ-prop A B : hProp (ℓ-suc ℓ) 以及反例论证中被判定的成员关系命题。把假设保留为显式模块参数，会在每次使用本模块时记录经典输入。

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

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

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

证明直接在环境层级 V 中进行，而不经由对象语言。载体与结构隶属 ∈ˢ 来自打包在 𝒮ᵥ 上的 ZF 结构，因此 ⟨ x ∈ˢ A ⟩ 是一个 hProp 真值的底层命题。V 的两条原理承担数学重任：extensionalV 把一族成员关系的双向蕴含转换为相等的路径；regularityV 使隶属关系良基，从而支持其上的归纳。L 侧其余的导入 mem-ord 在每次递归调用处起作用：它表明序数的任何成员自身也是序数，这正是归纳假设能在下层使用的原因。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ} using ( IsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

判定程序要回答三种情形中哪一种成立，因此返回类型由三向和构造：左边是隶属关系，中间是相等，右边是隶属关系。还需要从双向蕴含到路径的转换，外延性论证将对载体的每一点使用它。空类型全程扮演反驳的角色：反驳一个命题，就是把它映入一个没有元素的类型。

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
import Cubical.Induction.WellFounded as WF

最后为整个文件打开两项约定。hProp 上的直接运算提供成员关系陈述所用的命题联结词，结构词汇把 S 固定为载体、∈ˢ 固定为其隶属关系，于是代码读起来是集合论而非逻辑管道。这些约定让后面的论证能直接追踪序数元素的隶属、相等与良基递归。

open hPropStructure 𝒮ᵥ

包含，及其失败的见证

证明围绕一个关系展开：逐点包含。若它双向成立，外延性使两个序数相等；若它在某一方向失败，排中律给出一个截断的反例成员；良基归纳与传递性再把这个反例转成严格比较。本小节固定这个关系及其打包方式。注意层级运算已经说明的事：包含住在 Type (ℓ-suc ℓ)，这正是所给排中律实例能判定它的那一层。

A 包含于 B 在这里不是初始概念而是定义出来的：A 的每个成员 x，在结构意义下，必须是 B 的成员。每个成员关系 x ∈ˢ A 是 hProp 中的命题，因此定义量化了载体 S 与 ℓ 层的命题，把整个关系放进 Type (ℓ-suc ℓ)。配套的 hProp 打包附上命题性的证明：到命题的依赖函数仍是命题，把这一点对两层嵌套的函数类型各用一次。这很重要，因为排中律是逐 hProp 判定的，而证明交给 lem 的正是这个打包后的陈述。

_⊆ᵇ_ : S → S → Type (ℓ-suc ℓ)
A ⊆ᵇ B = (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ B ⟩

⊆ᵇ-prop : (A B : S) → hProp (ℓ-suc ℓ)
⊆ᵇ-prop A B = (A ⊆ᵇ B) , isPropΠ (λ x → isPropΠ (λ _ → snd (x ∈ˢ B)))

ext-⊆ᵇ : {A B : S} → A ⊆ᵇ B → B ⊆ᵇ A → A ≡ B

三歧中的相等情形由层级的外延性免费给出。给定双向包含，载体的每一点 x 都给出 ⟨ x ∈ˢ A ⟩ 与 ⟨ x ∈ˢ B ⟩ 之间的双向蕴含；⇔toPath 把它变成路径，extensionalV 再把路径族组装成相等 A ≡ B。这里完全没有用到经典输入：外延性本身就是 V 的定理。

ext-⊆ᵇ {A} {B} s₁ s₂ = extensionalV (λ x → ⇔toPath (s₁ x) (s₂ x))

这里是真正经典的那一步。从包含失败出发，证明需要一个见证它的成员，而从「B 的成员并非都含于 A」过渡到「某个成员不含于 A」不是构造性的。排中律直接判定那个存在陈述：若没有这样的见证，则可以逐个判定成员关系，证明 B 的每个成员终究含于 A，与假设的失败矛盾。得出的见证仍是命题截断的，而这已经足够，因为三歧证明对它唯一要做的事就是把它消去成一个成员关系命题。

陈述是条件式的：若包含 A ⊆ᵇ B 可被反驳，则存在一个截断的见证，即 A 的一个成员 a 使 a ∉ B。结论刻意写成 ∥ ∥₁ 下的存在陈述，而非选定的对。第一步经典动作是判定截断的存在陈述 Witness 本身。注意层级的记账：见证陈述是 ℓ-suc ℓ 处的 hProp，恰好是模块的 lem 适用的地方，因此无须抬升。正分支中见证已在手；有趣的是负分支。

¬⊆ᵇ→witness : (A B : S) → (A ⊆ᵇ B → Empty.⊥)
            → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
¬⊆ᵇ→witness A B ¬sub = decide (lem Witness)
  where
  Witness : hProp (ℓ-suc ℓ)

设 Witness 可被反驳。那么对包含的反驳本身也可被反驳：对任意的 x，单独判定成员关系 x ∈ˢ B；在负分支中，把成员 x 连同 x ∈ˢ A 与对 x ∈ˢ B 的反驳组装成 Witness 的一个元素，与所给反驳矛盾。于是包含终究成立，把它交给假设的对包含的反驳就得到空类型。这正是上面宣布的模式：对 Witness 的一次全局判定，加上对每个 x ∈ˢ B 的逐点判定，共同把「不存在见证」转化为「包含成立」。

  Witness = ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
          , PT.isPropPropTrunc
  decide : ⟨ Witness ⟩ ⊎ (⟨ Witness ⟩ → Empty.⊥) → ⟨ Witness ⟩
  decide (inl wit)  = wit
  decide (inr ¬wit) = Empty.rec (¬sub sub)

逐点判定值得停一停，因为它显示了截断的结论如何容纳截断的输入。要从 x ∈ˢ A 证明 x ∈ˢ B，用 lem 判定这一个成员关系。若成立则完成。若失败，对 x ∈ˢ B 的反驳连同 x ∈ˢ A 与 x 恰好是见证的数据，其截断 ∣ x , (x∈A , ¬x∈B) ∣₁ 是 Witness 的一个元素，与负分支的假设矛盾。

    where
    sub : A ⊆ᵇ B
    sub x x∈A = at (lem (x ∈ˢ B))
      where
      at : ⟨ x ∈ˢ B ⟩ ⊎ (⟨ x ∈ˢ B ⟩ → Empty.⊥) → ⟨ x ∈ˢ B ⟩

把各部分组装起来：对 Witness 的外层判定在正情形直接返回截断见证；在负情形，从假设的包含失败导出矛盾。辅助引理 ¬⊆ᵇ→witness 现在可供三歧论证的两个方向使用，而且它承诺的从来不超过一个截断见证。保持截断显式正是使后面的消去合法的原因：命题截断只能消去到命题，而下一小节消去进入的成员关系陈述恰好是命题。

      at (inl x∈B)  = x∈B
      at (inr ¬x∈B) = Empty.rec (¬wit ∣ x , (x∈A , ¬x∈B) ∣₁)

三歧

主要定理的准备工作已经齐备。比较写成三向和：或者 A 是 B 的成员，或者二者由一条路径相等，或者 B 是 A 的成员。证明对两个自变量各作一次良基归纳，使得在叶子处可以递归到任一序数的成员内部。两个包含 A ⊆ᵇ B 与 B ⊆ᵇ A 在每个叶子处由排中律判定；上一小节完成了其余工作。读者在情形分析中应当带上的方向记账是：B ⊆ᵇ A 失败产生一个属于 B 而不属于 A 的成员，结论是 A ∈ˢ B；A ⊆ᵇ B 失败产生一个属于 A 而不属于 B 的成员，结论是 B ∈ˢ A。

陈述 Tri A B 把三种可能的答案打包进一个类型，由嵌套的和构造。外侧两种情形是结构意义的成员关系；中间情形是相等的路径。类型位于 Type (ℓ-suc ℓ)，这是其内部的成员关系命题所要求的层级。

Tri : S → S → Type (ℓ-suc ℓ)
Tri A B = ⟨ A ∈ˢ B ⟩ ⊎ ((A ≡ B) ⊎ ⟨ B ∈ˢ A ⟩)

ord-tri : (A : S) → IsOrd A → (B : S) → IsOrd B → Tri A B
ord-tri = WF.WFI.induction regularityV {P = P} stepA
  where

定理的形状是正则性供给的良基归纳。被证的谓词 P A 说的是：A 与任何与之比较的序数 B 都表现正确，并把两个序数性证明当作假设。于是正则性给出对第一个自变量的归纳：要证 P A，只需对 A 的每个成员 A' 证 P A'。这是两层嵌套归纳中的第一层；第二层对 B，将出现在步内。

  P : S → Type (ℓ-suc ℓ)
  P A = IsOrd A → (B : S) → IsOrd B → Tri A B

  stepA : (A : S) → (∀ A' → ⟨ A' ∈ˢ A ⟩ → P A') → P A
  stepA A IHA ordA =
    WF.WFI.induction regularityV {P = λ B → IsOrd B → Tri A B} stepB

外层步拿到 A 每个成员的归纳假设，随即运行第二个良基归纳，这次对 B，谓词是 λ B → IsOrd B → Tri A B。在内层归纳步中，两个包含由 lem 应用于打包命题 ⊆ᵇ-prop A B 与 ⊆ᵇ-prop B A 来判定。这两个判定开启经典的分情形；前面的辅助引理也使用排中律，把每个包含失败转成截断的反例。

    where
    stepB : (B : S) → (∀ B' → ⟨ B' ∈ˢ B ⟩ → IsOrd B' → Tri A B')
          → IsOrd B → Tri A B
    stepB B IHB ordB = decide (lem (⊆ᵇ-prop A B)) (lem (⊆ᵇ-prop B A))
      where

第一个失败情形假设 B ⊆ᵇ A 失败，于是仅仅存在 B 的一个不属于 A 的成员 b。辅助引理 fromB 表明这样一个显式的对能给出什么：由于 b 是序数 B 的成员，mem-ord 证明 b 自身是序数，内层归纳假设 IHB 便可比较 A 与 b。其第一种结果是 A ∈ˢ b；序数的传递性，即 IsOrd B 的第一个分量，再把它经由 b ∈ˢ B 提升为 A ∈ˢ B。

      fromB : Σ[ b ∈ S ] (⟨ b ∈ˢ B ⟩ × (⟨ b ∈ˢ A ⟩ → Empty.⊥)) → ⟨ A ∈ˢ B ⟩
      fromB (b , (b∈B , ¬b∈A)) = at (IHB b b∈B (mem-ord {A = B} ordB b b∈B))
        where
        at : Tri A b → ⟨ A ∈ˢ B ⟩
        at (inl A∈b)       = ordB .fst A∈b b∈B

比较 A 与 b 的另外两种结果依次处理。若 A ≡ b 是一条路径，则沿该路径把 b ∈ˢ B 反向搬运，即用 subst 配 sym 所做的，得到 A ∈ˢ B。若 b ∈ˢ A，则与 b 被选为 A 之外直接矛盾。三个分支都落入同一命题 ⟨ A ∈ˢ B ⟩，这正是仅仅存在的见证在此够用的原因：截断的对被消去进命题，从不消去进数据。

        at (inr (inl A≡b)) = subst (λ w → ⟨ w ∈ˢ B ⟩) (sym A≡b) b∈B
        at (inr (inr b∈A)) = Empty.rec (¬b∈A b∈A)

      fromA : Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) → ⟨ B ∈ˢ A ⟩
      fromA (a , (a∈A , ¬a∈B)) =
        at (IHA a a∈A (mem-ord {A = A} ordA a a∈A) B ordB)

镜像的辅助引理 fromA 覆盖另一个失败：A ⊆ᵇ B 失败，于是 A 的某个成员 a 不在 B 内。此时由外层归纳假设承担工作，因为它比较 A 的成员，并在 a 处应用。若 a 结果属于 B，则与 a 的选取矛盾；若 a ≡ B，搬运给出 B ∈ˢ A；若 B ∈ˢ a，则 A 的传递性把它经由 a ∈ˢ A 提升。注意镜像引入的不对称：相等分支沿路径搬运 a ∈ˢ A 而非反向搬运，因为这次被比较的一对方向相反。

        where
        at : Tri a B → ⟨ B ∈ˢ A ⟩
        at (inl a∈B)       = Empty.rec (¬a∈B a∈B)
        at (inr (inl a≡B)) = subst (λ w → ⟨ w ∈ˢ A ⟩) a≡B a∈A
        at (inr (inr B∈a)) = ordA .fst B∈a a∈A

两个转换器在手后，四种裁决组合归入三种答案。若两个包含都成立，由上一小节可知互相包含就是相等，返回中间答案。若 A ⊆ᵇ B 成立而 B ⊆ᵇ A 失败，则用 PT.rec 消去该失败的截断见证，这之所以合法，恰恰因为目标 ⟨ A ∈ˢ B ⟩ 是命题，其命题性由成员 hProp 的第二个分量提供。结果是左侧答案 A ∈ˢ B：这正是 B ⊆ᵇ A 失败而结论为 A 属于 B 的分支。

      decide : (A ⊆ᵇ B) ⊎ ((A ⊆ᵇ B) → Empty.⊥)
             → (B ⊆ᵇ A) ⊎ ((B ⊆ᵇ A) → Empty.⊥) → Tri A B
      decide (inl A⊆B) (inl B⊆A) = inr (inl (ext-⊆ᵇ A⊆B B⊆A))
      decide (inl A⊆B) (inr ¬B⊆A) =
        inl (PT.rec (snd (A ∈ˢ B)) fromB (¬⊆ᵇ→witness B A ¬B⊆A))

最后一种组合覆盖 A ⊆ᵇ B 的失败，无论第二个裁决如何，镜像转换器交付 B ∈ˢ A。与上面两种情形合并，每个叶子现在都返回 Tri A B 的一个元素，于是双层归纳闭合，ord-tri 成为关于任意序数 A 与 B 的定理。后续关于层序与基数的章节，例如 L.GCH.CardinalSquareLaw，把它当作自己的比较原语。

      decide (inr ¬A⊆B) _ =
        inr (inr (PT.rec (snd (B ∈ˢ A)) fromA (¬⊆ᵇ→witness A B ¬A⊆B)))

小结

结合层级成员关系已有的非自反性和 IsOrd 所含的传递性，ord-tri 现在给出任意两个序数的比较。这些比较定律构成后续层单调性与基数论证的序论基础。

ord-tri 比较任意两个序数，而本书为它提供一份排中律实例，并把它取作模块参数。这正是奠基部分为使其可审计而搭建的那道边界：无一处 postulate，使用 ord-tri 时必须提供本模块的排中律参数。随后的章节把这个比较用在它被需要的那个问题上：哪些序数出现在可构造层级的哪个层。