序数指标、Gödel 对序与有穷指标

本章为后续计数论证提供三项具体工具：序数指标上的隶属良序、指标对上的 Gödel 序，以及有穷序数成员与 Fin 之间的对应。

第一个构造通过指标所指名的序数元素之间的隶属关系来比较两个指标；序数的三歧性与正则性把这个比较变成指标类型上的严格良序。第二个构造用该序下坐标的最大值为指标对分级，并对共享最大坐标的对按字典序排列；三歧性、非自反性与传递性直接证明，而良基性则通过把下降嵌入两层字典序乘积得到。第三个构造把无穷序数 ω 的每个成员读作数码，并在有穷序数 # n 的指标与 Fin n 之间作双向转换。随后它把一个准确的不可能性归约为有穷鸽笼原理：若一个类型容纳任意大小的有穷类型的单射像，它就不能单射到某个固定有穷类型的平方中。

本章在固定的宇宙层级 ℓ 上工作，并取一个经典假设作为模块参数：层级 ℓ-suc ℓ 上每个命题的判定。后文建立的比较需要它，因为序数三歧与最小元搜索各自要用排中律裁决一个单纯存在性问题。把这个假设保留为显式参数，恰好记录了每个构造消耗的是哪一份经典输入。

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

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

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

数学背景是累积层级 V：其集合构成一个类型 S，隶属是「存在某个指标」的截断陈述。每个集合 a 自带一份选定的小呈现：指标类型 ⟪ a ⟫ 与嵌入 ⟪ a ⟫↪，后者的像正是 a。于是讨论 a 的成员就变成讨论指标，而嵌入的单射性把指名同一元素的指标等同起来。下面的构造处理带证书 IsOrd α 的任意序数 α：von Neumann 意义下传递集且成员皆传递的集合。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import V.Model {ℓ} using ( ω-specV; numeralV; numeralV≡# )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import L.Constructible {ℓ} using ( IsOrd )

严格良序把同一关系的四项性质结合起来：任意两点可作三歧比较，没有点严格小于自身，严格比较具有传递性，并且每条递降链都是良基的。自然数给出典型例子。leastOf 利用这一结构与排中律，从仅仅有元素的命题值族中选出最小见证；稍后，序数三歧为序数成员提供同样的三向比较。

open import L.Ordinal {ℓ} using ( mem-ord; ∈#-elim )
open import V.Coding {ℓ} using ( #-inj′; #mono )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( SWO; Tri; lt; eq; gt; leastOf; natOrder; module SWO )

逻辑词汇与待证陈述的形状相配。反驳是映到空类型的函数；隶属证明是截断命题的居民；三路比较是其各情形的和，由 inl 与 inr 标注。序对之间与记录之间的路径由标准引理 Σ≡Prop 与 ΣPathP 处理：当相关分支类型是命题时，它们从分量的路径构造出进入依赖对的路径。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Sigma using ( Σ≡Prop; ΣPathP )

有穷计数部分需要算术与标准有穷类型。自然数乘法 _·_ 度量有穷类型的平方，库中的等价 factorEquiv 把 Fin n × Fin n 与 Fin (n · n) 等同起来。鸽笼定理给出本章末尾论证的锚点：从 Fin (suc n) 到 Fin n 不存在单射。自然数上的序还附带「≤ 是命题」这一事实，这使得到 Fin 的比较与其界的证明无关性相容。

open import Cubical.Data.Nat using ( _·_ )
import Cubical.Data.Fin.Base as FB
open import Cubical.Data.Fin.Properties using ( factorEquiv; pigeonhole )
open import Cubical.Data.Nat.Order using ( _<_; isProp≤; ≤-refl )
open import Cubical.Foundations.Equiv using ( equivFun; invEq; retEq )

对每个集合 a，呈现映射 ⟪ a ⟫↪ 把指标送到它所指名的成员，因此它在 # k 上的原像恰由指名该数码的指标组成。当 k < n 时，数码的单调性把 # k 置于 # n 内，选取相应原像中的点便定义了从 Fin n 到有穷序数指标类型的转换。反向转换将使用最小元搜索，因为任意指标并不自带其数码标号。

open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )

良基性由可及性谓词承载：当 x 的每个 R-前驱都可及时，Acc R x 成立；acc 打包这一数据；WellFounded R 要求每个元素都可及。本章的下降论证正是逐层向下传递这些可及性证书。最后，层级 ℓ-suc ℓ 的 hProp 直接运算在此可用，使命题上的合取等逻辑运算可供序数一节使用的结构机制调用。

open InfinitySet using ( #_; ω )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )

open hPropStructure 𝒮ᵥ

本章稍后，Gödel 对序的良基性将通过把其下降嵌入嵌套的字典序下降而得到。所需的一般构造是：给定 X 上的严格良序与 Y 上任意良基关系，乘积 X × Y 带有自然的严格序，且该序良基。本节恰好构造这一点，此外无他。

两点塑造了这个构造。其一，乘积序先用良序比较第一坐标，只有当两个方向的严格比较都不成立，即第一坐标相等时，才查阅第二个关系；从两次失败的比较中恢复相等，正是联结性引理所做的。其二，证明同时携带第一坐标与第二坐标的可及性证书，与这个序的两级优先次序相对应。

严格良序使任意两个元素三歧：比较数据 Tri 返回「a 低于 b」的证明、路径 a ≡ b，或「b 低于 a」的证明。因此若两个严格方向都被反驳，只剩下中间情形，而它恰好携带我们要的相等。这个联结性引理把这一情形分析打包；它不是新的序定律，而是在两个反驳下对三歧数据的解读。

connex : {ℓc : Level} {A : Type ℓc} (w : SWO A) (a b : A)
       → (SWO._<∙_ w a b → Empty.⊥) → (SWO._<∙_ w b a → Empty.⊥) → a ≡ b
connex w a b ¬ab ¬ba with SWO.tri∙ w a b
... | lt h = Empty.rec (¬ab h)
... | eq p = p

乘积以一般方式建立。第一因子带 X 上的严格良序 u，从而可使用其关系、三歧性与良基性。第二因子带 Y 上任意良基的关系 _<ᵥ_；不要求它有三歧性或传递性，因为乘积只需沿它下降。两个关系都取值于层级 ℓ-suc ℓ，即后文序数比较所处的层级。

... | gt h = Empty.rec (¬ba h)


module _ {ℓx ℓy : Level} {X : Type ℓx} {Y : Type ℓy} (u : SWO X)
         (_<ᵥ_ : Y → Y → Type (ℓ-suc ℓ)) (wfv : WellFounded _<ᵥ_) where

  private
    module U = SWO u

乘积序 _≺×_ 比较两个方式把 (a , x) 排在 (b , y) 之下：或者 a 在良序下严格低于 b；或者第一坐标相等，以对两个严格方向的反驳为证，且 x 在第二个关系下低于 y。这就是以和类型陈述的字典序优先级：先查良序，仅在平局时查第二个关系。与序并列，证明也计划好了其数据：accProd 将从每个坐标的可及性证书造出序对的可及性证书。

  _≺×_ : X × Y → X × Y → Type (ℓ-suc ℓ)
  (a , x) ≺× (b , y) =
    (a U.<∙ b) ⊎ (((a U.<∙ b) → Empty.⊥) × ((b U.<∙ a) → Empty.⊥) × (x <ᵥ y))

  private
    accProd : (a : X) → Acc U._<∙_ a → (x : Y) → Acc _<ᵥ_ x → Acc _≺×_ (a , x)

下降遵循两级优先次序。已知 a 在良序中可及且 x 在第二个关系中可及，任何 ≺×-前驱 (b , y) 落入和的两个分支之一。若第一坐标严格下降，则 b 是 a 在良序中的前驱，其可及性证书 ru b h 适用，而 y 贡献自己的证书 wfv y；对这两个严格更小的证书递归，就造出 (b , y) 的证书。

    accProd a (acc ru) = inner
      where
      inner : (x : Y) → Acc _<ᵥ_ x → Acc _≺×_ (a , x)
      inner x (acc rv) = acc λ where
        (b , y) (inl h) → accProd b (ru b h) y (wfv y)

平局情形正是联结性引理的用武之地：第二个分支断言两个严格比较都失败，于是 connex 产生路径 b ≡ a，可把该对沿此路径搬运到第一坐标相等的对上，把下降约化为只在第二个关系上进行，那里的证书 rv y h 适用。把这两个子句叠起来，每个序对都可及：良序使每个第一坐标可及，假设使每个第二坐标可及。这就是 prodWF，本章其余部分消耗的关于乘积的唯一陈述。

        (b , y) (inr (¬ba , ¬ab , h)) →
          subst (λ z → Acc _≺×_ (z , y)) (sym (connex u b a ¬ba ¬ab))
            (inner y (rv y h))

  prodWF : WellFounded _≺×_
  prodWF (a , x) = accProd a (U.wf∙ a) x (wfv x)

序数指标上的隶属序

序数 α 是传递集且成员皆传递，其成员按隶属线性有序；经典输入 ord-tri 使这个序三歧。但后续章节的计数论证需要的不是成员本身上的序，而是 α 的固定呈现的指标上的序：小类型 ⟪ α ⟫，其嵌入 ⟪ α ⟫↪ 的像正是 α。本节把隶属序从成员搬运到指标上。

两个区分使这个搬运忠实。其一，指标 m 本身不是层级中的集合；它所指名的元素是 ⟪ α ⟫↪ m，一切比较都发生在这些被指名的元素层面，而嵌入的单射性从元素相等恢复指标相等。其二，每个被指名的元素本身也是序数，这是 α 的传递性的推论，正是它允许在每个指标处使用传递性与经典三歧。结果是 ⟪ α ⟫ 上的严格良序 ordSWO，即下一节 Gödel 对序据以分级的基底实例。

指标上的关系 ≺₁ 由被指名元素间的隶属定义：m ≺₁ n 成立，当且仅当 ⟪ α ⟫↪ m 按结构的隶属命题是 ⟪ α ⟫↪ n 的成员。本节其余内容都围绕这个定义展开。第一个支撑事实是：每个被指名元素本身也是序数。由于 α 传递而指标 m 指名 α 的一个成员，把证书 mem-ord 应用于隶属证明 member α m 便得到被指名元素的 IsOrd。这个证书 ord-inord 在下文还要再用三次。

module _ (α : S) (oα : IsOrd α) where

  _≺₁_ : ⟪ α ⟫ → ⟪ α ⟫ → Type (ℓ-suc ℓ)
  m ≺₁ n = ⟪ α ⟫↪ m ∈ᵗ ⟪ α ⟫↪ n

  ord-inord : (m : ⟪ α ⟫) → IsOrd (⟪ α ⟫↪ m)
  ord-inord m = mem-ord {A = α} oα (⟪ α ⟫↪ m) (member α m)

指标的三歧来自被指名元素的三歧。经典定理 ord-tri 比较两个序数成员，返回和类型：第一个是第二个的成员的证明、元素相等的路径，或相反方向的证明。辅助函数 go 匹配这三种情形：两个隶属分支直接成为 lt 与 gt，因为 ≺₁ 正是定义为被指名元素间的隶属。

  tri₁ : (m n : ⟪ α ⟫) → Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m)
  tri₁ m n = go (ord-tri (⟪ α ⟫↪ m) (ord-inord m) (⟪ α ⟫↪ n) (ord-inord n))
    where
    go : (⟨ ⟪ α ⟫↪ m ∈ˢ ⟪ α ⟫↪ n ⟩
          ⊎ ((⟪ α ⟫↪ m ≡ ⟪ α ⟫↪ n) ⊎ ⟨ ⟪ α ⟫↪ n ∈ˢ ⟪ α ⟫↪ m ⟩))

相等的分支是唯一实质性使用呈现之处。序数三歧返回的是被指名元素的相等，而目标是指标的相等，两者是不同的类型。嵌入的单射性 ↪-inj 把元素路径反映为指标间的路径。处理好这个分支后，tri₁ 就是 ⟪ α ⟫ 上的三情形比较数据 Tri。

       → Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m)
    go (inl h)       = lt h
    go (inr (inl p)) = eq (↪-inj {a = α} p)
    go (inr (inr h)) = gt h

  irr₁ : (m : ⟪ α ⟫) → (m ≺₁ m → Empty.⊥)

非自反性与传递性从被指名元素继承。没有集合属于自身，故 m ≺₁ m 自我反驳。对传递性，m ≺₁ n 与 n ≺₁ k 都是关于 ⟪ α ⟫↪ k 的隶属事实，而由 ord-inord 它是序数；IsOrd 证书的第一个分量断言序数成员间隶属的传递性，因此直接把两个事实串联。可及性同样搬运：若被指名元素 ⟪ α ⟫↪ m 的每个成员在隶属下可及，则 m 的每个 ≺₁-前驱 n 指名一个成员，把指标 n 的隶属事实喂给其证书，acc₁ 便返回 m 在 ≺₁ 下的可及性。

  irr₁ m h = ∈-irrefl (⟪ α ⟫↪ m) h

  trans₁ : (m n k : ⟪ α ⟫) → m ≺₁ n → n ≺₁ k → m ≺₁ k
  trans₁ m n k h h' = ord-inord k .fst h h'

  acc₁ : (m : ⟪ α ⟫) → Acc _∈ᵗ_ (⟪ α ⟫↪ m) → Acc _≺₁_ m
  acc₁ m (acc r) = acc (λ n n≺m → acc₁ n (r (⟪ α ⟫↪ n) n≺m))

≺₁ 的良基性只差一步：环境层级上的正则性把隶属下的可及性证书交给每个集合，故每个被指名元素 ⟪ α ⟫↪ m 可及，而 acc₁ 把它提升为指标 m 的可及性。这就是 wf₁，有穷一节的搜索将复用的良基性。随后记录 ordSWO 把关系与其四条定律打包进接口 SWO，与严格良序一章的自然数实例供给的是同样的五个字段。

  wf₁ : WellFounded _≺₁_
  wf₁ m = acc₁ m (regularityV (⟪ α ⟫↪ m))

  ordSWO : SWO ⟪ α ⟫
  ordSWO = record
    { _<∙_   = _≺₁_

组装 ordSWO 正是本节的要点：这是一个实例，而非新的数学。此后任何以 SWO 为输入的构造都能运行在任意序数的指标上，下一节的对序消耗的正是这个实例。这里对 ω 或有穷序数没有任何特殊处理；论证只用到了 α 的传递性、嵌入、经典三歧与正则性。

    ; tri∙   = tri₁
    ; irr∙   = irr₁
    ; trans∙ = trans₁
    ; wf∙    = wf₁ }

经典的 Gödel 配对想法是给指标对排一个序，使对上的下降能按坐标逐层分析。这里用的序不是普通的字典序：它先用两坐标的 ≺₁-最大值分级，使坐标都小的对无论怎样排列都沉到有大坐标的对之下，只有共享最大等级的对才按第一坐标、再按第二坐标比较。本节定义这个序，并从 ≺₁ 的相应定律直接证明三歧、非自反与传递；其良基性需要前文的字典序乘积，在下一段代码中给出。

最大值需要一个预备：≺₁ 的自反伴随 ≤₁，定义为严格关系与相等之和。由于三歧数据是显式的三情形数据，两个指标的最大值通过检查比较、返回两个输入之一来计算，而证书 max-spec 记录使返回值成为真正最大值的两个 ≤₁-事实。

非严格伴随 ≤₁ 收集了「一个指标不严格高于另一个」的两种方式：m ≤₁ n 成立，或者因为 m ≺₁ n，或者因为 m 与 n 相等。借助它，最大值由比较数据定义：maxGo 以 m 与 n 的三情形比较为参数，返回较大者，m 严格低于时返回 n，其余两种情形返回 m。

  _≤₁_ : ⟪ α ⟫ → ⟪ α ⟫ → Type (ℓ-suc ℓ)
  m ≤₁ n = (m ≺₁ n) ⊎ (m ≡ n)

  maxGo : (m n : ⟪ α ⟫) → Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m) → ⟪ α ⟫
  maxGo m n (lt _) = n
  maxGo m n (eq _) = m

函数 maxOrd 是完全化的最大值：先计算比较 tri₁ m n，再把 maxGo 应用于该数据。由于 tri₁ 是经典输入，maxOrd 是一个取值依赖该数据的定义函数，而非单独证明的完全性断言。规格 max-spec 陈述使结果成为最大值的内容：每个输入都 ≤₁ 输出，其证明也走同一情形分析，接下来的 where 块执行之。

  maxGo m n (gt _) = m

  maxOrd : ⟪ α ⟫ → ⟪ α ⟫ → ⟪ α ⟫
  maxOrd m n = maxGo m n (tri₁ m n)

  max-spec : (m n : ⟪ α ⟫) → (m ≤₁ maxOrd m n) × (n ≤₁ maxOrd m n)
  max-spec m n = go (tri₁ m n)

前两个比较情形直接认证两条 ≤₁ 事实。若 m ≺₁ n，则 m ≤₁ n 使用严格分支，而 n ≤₁ n 使用相等分支；当 m 与 n 相等时，路径的对称性给出第二条等式。

    where
    go : (t : Tri (m ≺₁ n) (m ≡ n) (n ≺₁ m))
       → (m ≤₁ maxGo m n t) × (n ≤₁ maxGo m n t)
    go (lt h) = inl h , inr refl
    go (eq p) = inr refl , inr (sym p)

余下情形与之对称：若 n ≺₁ m，则选出的最大值是 m。因此 max-spec 恰好断言两个输入在自反序 ≤₁ 中都不超过计算所得的最大值。

    go (gt h) = inr refl , inl h

类型 Pair 收集指标的平方：一个元素是 α 的指标对 (a , b)。Pair 上的序 ≺ 以嵌套和定义出它的三级优先次序。第一个分支比较等级：maxOrd a b 严格低于 maxOrd c d。若等级持平，第二个分支要求等级相等，再比较坐标：a 严格低于 c，或在 a 等于 c 时 b 严格低于 d。

  Pair : Type ℓ
  Pair = ⟪ α ⟫ × ⟪ α ⟫

  _≺_ : Pair → Pair → Type (ℓ-suc ℓ)
  (a , b) ≺ (c , d) =

三歧性的证明由外向内镜像定义的嵌套。外层分析 M-case 用 tri₁ 比较两个等级；当等级严格有序时，整对就在任一方向上被第一个分支严格排序。只有平局情形才需要内层，tri≺ 作为单个函数组装而成，对任意两对返回三情形数据。

    (maxOrd a b ≺₁ maxOrd c d)
      ⊎ ((maxOrd a b ≡ maxOrd c d) × ((a ≺₁ c) ⊎ ((a ≡ c) × (b ≺₁ d))))

  tri≺ : (p q : Pair) → Tri (p ≺ q) (p ≡ q) (q ≺ p)
  tri≺ (a , b) (c , d) = M-case (tri₁ (maxOrd a b) (maxOrd c d))
    where

最深的情形 Y-case 处理等级与第一坐标都一致的对，比较第二坐标。b 与 d 的严格比较按相应方向使两对严格有序，两个等式作为「外层确实持平」的见证一并携带；反方向对称。

    Y-case : (e : maxOrd a b ≡ maxOrd c d) (f : a ≡ c)
           → Tri (b ≺₁ d) (b ≡ d) (d ≺₁ b)
           → Tri ((a , b) ≺ (c , d)) ((a , b) ≡ (c , d)) ((c , d) ≺ (a , b))
    Y-case e f (lt h) = lt (inr (e , inr (f , h)))
    Y-case e f (gt h) = gt (inr (sym e , inr (sym f , h)))

当第二坐标也一致时，两对相等，pairing 构造子上的 cong₂ 把两个坐标路径变成对之间的路径；这正是比较数据的相等分支携带实际路径而非裸标签的原因。向上一层，X-case 比较第一坐标：严格比较在该层决定次序，平局情形带着 b 与 d 的比较下降到 Y-case。

    Y-case e f (eq g) = eq (cong₂ _,_ f g)

    X-case : (e : maxOrd a b ≡ maxOrd c d)
           → Tri (a ≺₁ c) (a ≡ c) (c ≺₁ a)
           → Tri ((a , b) ≺ (c , d)) ((a , b) ≡ (c , d)) ((c , d) ≺ (a , b))
    X-case e (lt h) = lt (inr (e , inl h))

最后是顶层：M-case 比较等级本身。两个严格情形直接应用 ≺ 的第一个分支。M-case 的签名明确其输入正是两个等级的三歧数据，于是 tri≺ 的整个证明可以读作逐层进行的一次三重情形分析，每一层消耗下一层的比较数据。

    X-case e (gt h) = gt (inr (sym e , inl h))
    X-case e (eq f) = Y-case e f (tri₁ b d)

    M-case : Tri (maxOrd a b ≺₁ maxOrd c d)
                 (maxOrd a b ≡ maxOrd c d)
                 (maxOrd c d ≺₁ maxOrd a b)

M-case 的三个情形结束分析：等级严格，或平局经第一坐标再到第二坐标下降。有了 tri≺，序 ≺ 作为数据是三歧的，这正是后续唯一性论证要消耗的性质。

           → Tri ((a , b) ≺ (c , d)) ((a , b) ≡ (c , d)) ((c , d) ≺ (a , b))
    M-case (lt h) = lt (inl h)
    M-case (gt h) = gt (inl h)
    M-case (eq e) = X-case e (tri₁ a c)

  irr≺ : (p : Pair) → (p ≺ p → Empty.⊥)

对序的非自反性很简短，因为每一层已知道如何反驳自己的严格比较。若 (a , b) ≺ (a , b)，其见证落入嵌套定义的三个分支之一；每个都是关于某坐标或某等级的严格 ≺₁-事实，相应的 irr₁ 把它变成矛盾。等级情形在 maxOrd a b 处用 irr₁，第一坐标情形在 a 处，第二坐标情形在 b 处。

  irr≺ (a , b) (inl h)              = irr₁ (maxOrd a b) h
  irr≺ (a , b) (inr (e , inl h))    = irr₁ a h
  irr≺ (a , b) (inr (e , inr (f , h))) = irr₁ b h

  trans≺ : (p q r : Pair) → p ≺ q → q ≺ r → p ≺ r
  trans≺ (a , b) (c , d) (e , f) = goM

传递性是实质的定律，其证明围绕三个等级组织：M₁ 是 (a , b) 的等级，M₂ 是 (c , d) 的，M₃ 是 (e , f) 的。引理 goY 与 goX 先处理内层。goY 不过是把 ≺₁ 的传递性应用于第二坐标；它是下文最内层情形的复合论证。

    where
    M₁ = maxOrd a b
    M₂ = maxOrd c d
    M₃ = maxOrd e f

    goY : (b ≺₁ d) → (d ≺₁ f) → (b ≺₁ f)

引理 goX 复合两个严格步骤在坐标层面的裁决。当两步都在第一坐标严格时，≺₁ 的传递性复合它们。当一步严格而另一步是第一坐标相等时，严格事实沿该路径搬运，因为 a ≺₁ c 与 c ≡ e 经代入给出 a ≺₁ e。两者皆相等是剩余情形，交给第二坐标处理。

    goY = trans₁ b d f

    goX : ((a ≺₁ c) ⊎ ((a ≡ c) × (b ≺₁ d)))
        → ((c ≺₁ e) ⊎ ((c ≡ e) × (d ≺₁ f)))
        → ((a ≺₁ e) ⊎ ((a ≡ e) × (b ≺₁ f)))
    goX (inl h) (inl h') = inl (trans₁ a c e h h')

剩余情形从 goX 交给第二坐标的对，其相等路径拼接起来见证两端点的等级重合。这两个引理备好后，goM 的签名在顶层陈述复合问题：从 M₁ 与 M₂ 之间的严格步骤或平局，以及 M₂ 与 M₃ 之间的相应裁决，产出 M₁ 与 M₃ 之间的相应裁决。其结构恰好是 goX 向上一层的镜像。

    goX (inl h) (inr (e₂ , _)) = inl (subst (λ w → a ≺₁ w) e₂ h)
    goX (inr (e₁ , _)) (inl h') = inl (subst (λ w → w ≺₁ e) (sym e₁) h')
    goX (inr (e₁ , s₁)) (inr (e₂ , s₂)) = inr (e₁ ∙ e₂ , goY s₁ s₂)

    goM : ((M₁ ≺₁ M₂) ⊎ ((M₁ ≡ M₂) × ((a ≺₁ c) ⊎ ((a ≡ c) × (b ≺₁ d)))))
        → ((M₂ ≺₁ M₃) ⊎ ((M₂ ≡ M₃) × ((c ≺₁ e) ⊎ ((c ≡ e) × (d ≺₁ f)))))

goM 的四个分支正是 goX 上移一层之后的模样。若两个极大值之间的两步都是严格步骤，就用 ≺₁ 的传递性把 M₁ ≺₁ M₂ 与 M₂ ≺₁ M₃ 复合起来。若其中一步严格而另一步在极大值处是等值，则严格事实沿等值路径搬运：由 M₁ ≺₁ M₂ 和 M₂ ≡ M₃ 经替换得到 M₁ ≺₁ M₃；等值在前时对称地使用 sym e₁。只有当两步都是极大值处的等值时才留在本层：记 e₁ ∙ e₂ 为级差等值的拼接路径，并把第二坐标交给 goX 处理。

        → ((M₁ ≺₁ M₃) ⊎ ((M₁ ≡ M₃) × ((a ≺₁ e) ⊎ ((a ≡ e) × (b ≺₁ f)))))
    goM (inl h) (inl h') = inl (trans₁ M₁ M₂ M₃ h h')
    goM (inl h) (inr (e₂ , _)) = inl (subst (λ w → M₁ ≺₁ w) e₂ h)
    goM (inr (e₁ , _)) (inl h') = inl (subst (λ w → w ≺₁ M₃) (sym e₁) h')
    goM (inr (e₁ , s₁)) (inr (e₂ , s₂)) = inr (e₁ ∙ e₂ , goX s₁ s₂)

为了借用字典序乘积的良基性，把每个序对重新呈现为三元组：f 把级差 maxOrd a b 记在序对 (a , b) 之前。这个映射的单射性几乎是显然的：三元组之间的路径可以投影到存放在第二分量中的序对上，投影 cong snd 直接还原出序对的相等。

  f : Pair → ⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)
  f (a , b) = maxOrd a b , (a , b)

  f-inj : {p q : Pair} → f p ≡ f q → p ≡ q
  f-inj {a , b} {c , d} e = cong snd e

  _≺²_ : (⟪ α ⟫ × ⟪ α ⟫) → (⟪ α ⟫ × ⟪ α ⟫) → Type (ℓ-suc ℓ)

现在以序数序为外层分量实例化两个字典序乘积。关系 _≺²_ 比较指标的序对：先比较左坐标上的 ≺₁，当两个方向都不成立时再比较右坐标上的 ≺₁；prodWF 恰好为这种形状给出良基性。再堆叠一次得到 _≺³_，它比较 f 所落入的带级三元组，于是 _≺³_ 下的递降是三级字典序递降：级差、第一坐标、第二坐标。

  _≺²_ = _≺×_ ordSWO _≺₁_ wf₁

  wf² : WellFounded _≺²_
  wf² = prodWF ordSWO _≺₁_ wf₁

  _≺³_ : (⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)) → (⟪ α ⟫ × (⟪ α ⟫ × ⟪ α ⟫)) → Type (ℓ-suc ℓ)
  _≺³_ = _≺×_ ordSWO _≺²_ wf²

wf³ 只是 prodWF 的第二次应用，因此 _≺³_ 无需进一步工作便是良基的。辅助事实 ¬<₁ 记录了反自反性的一个小推论：若指标 m 与 n 相等，则步骤 m ≺₁ n 不可能存在，因为把该步骤沿等式向后搬运就得到 m ≺₁ m。这正是乘积关系所需的簿记，因为 _≺×_ 只有在外层两个方向都不成立时才降到第二层。有了这一点，subrel 的类型便是把序对序的每个步骤 p ≺ q 转换成带级三元组之间的步骤 f p ≺³ f q。

  wf³ : WellFounded _≺³_
  wf³ = prodWF ordSWO _≺²_ wf²

  ¬<₁ : (m : ⟪ α ⟫) {n : ⟪ α ⟫} → m ≡ n → (m ≺₁ n → Empty.⊥)
  ¬<₁ m {n} q h = irr₁ m (subst (λ w → m ≺₁ w) (sym q) h)

  subrel : {p q : Pair} → p ≺ q → f p ≺³ f q

subrel 的前两种情形是直接的。当级差已经严格有序时，步骤 inl h 本身就是 _≺³_ 的顶层步骤，因为两个关系共用外层分量 ≺₁。当级差相等而第一坐标严格有序时，目标关系要求在降层之前证明级差的两个方向都不成立；对等值路径及其对称各用一次 ¬<₁ 恰好给出这两个反驳，随后 inl h 把严格的第一坐标步骤放到第二层。

  subrel {a , b} {c , d} (inl h) =
    inl h
  subrel {a , b} {c , d} (inr (e , inl h)) =
    inr (¬<₁ (maxOrd a b) e , ¬<₁ (maxOrd c d) (sym e) , inl h)
  subrel {a , b} {c , d} (inr (e , inr (f , h))) =

完全相等的情形更深一层嵌套：级差相等、第一坐标相等、第二坐标严格有序，因此 subrel 必须先反驳级差的两个方向、再反驳第一坐标的两个方向，才能把 h 放到最内层。序对序的良基性随后由沿 f 拉回可达性得到：wf≺ p 从 f p 在 _≺³_ 中的可达性出发，而这正是 wf³ 所提供的。私有辅助函数 go 的陈述方式使得可达性证明的指标就确定了它所关心的序对，从而下方的递归得以重新进入自身。

    inr (¬<₁ (maxOrd a b) e , ¬<₁ (maxOrd c d) (sym e)
       , inr (¬<₁ a f , ¬<₁ c (sym f) , h))

  wf≺ : WellFounded _≺_
  wf≺ p = go (wf³ (f p))
    where

go 的计算规则展开可达性数据：由 acc r (其中 r 把 f q 的每个 _≺³_ 前驱映到可达性) 在序对一侧产生 acc。给定带 q' ≺ q 的前驱 q'，先经 subrel 把该步骤推前为 f q' ≺³ f q，交给 r，再对结果应用 go。于是序对的每个递降链都映为带级三元组的递降链，而 _≺³_ 的良基性禁止后者，故序对序不存在无穷递降。

    go : {q : Pair} → Acc _≺³_ (f q) → Acc _≺_ q
    go {q} (acc r) = acc (λ q' q'≺q → go (r (f q') (subrel {q'} {q} q'≺q)))

在有穷序数与 Fin 之间转换

ω 的每个成员都是数码，但 ω 的成员资格是截断命题，只能给出数码标号「仅仅存在」。而在有穷序数 # n 内部情况更好：命题「该指标表示 # k 且 k < n」是一个 hProp，排中律因此适用，最小元搜索会返回一个被选出的最小标号。这个标号就是转换 toFin : ⟪ # n ⟫ → Fin n，而 #mono 提供的纤维给出返回之路。

搜索命题 P 对 # n 的每个指标 m 和每个自然数 k，打包了 k < n 与「m 表示数码 # k」这两者的合取。它的命题性由两个事实组装而成：序关系 k < n 是命题，而所表示元素之间的等式生活在集合中，其等式类型因此也是命题。把这个合取包成 hProp，正是后面得以对它应用排中律的原因。

module FiniteBase where

  P : (n : ℕ) (m : ⟪ # n ⟫) → ℕ → hProp (ℓ-suc ℓ)
  P n m k = ((k < n) × (⟪ # n ⟫↪ m ≡ # k))
          , isProp× isProp≤ (isSetS (⟪ # n ⟫↪ m) (# k))

  ω-mem→numeral : (β : S) → ⟨ β ∈ˢ ω ⟩ → ∥ Σ[ n ∈ ℕ ] (β ≡ # n) ∥₁

β 属于 ω 本身只以截断的方式说 β 是一个数码：ω 的刻画给出一个提升自然数与近似证书的截断序对。辅助函数 hit 把这份数据精化为一条路径：近似 β ≈ˢ numeralV n 与 numeralV≡# n 复合得到 β ≡ # n。结果保持在 ∥_∥₁ 之内，所以该定理给出数码标号的仅仅存在而非被选出的标号；要得到见证就需要把截断消入非命题性目标。

  ω-mem→numeral β β∈ω = PT.map hit (subst ⟨_⟩ (ω-specV β) β∈ω)
    where
    hit : Σ[ n ∈ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] ⟨ β ≈ˢ numeralV (lower n) ⟩
        → Σ[ n ∈ ℕ ] (β ≡ # n)
    hit (n , p) = lower n , p ∙ numeralV≡# (lower n)

对有穷序数 # n 的指标，存在具体的出发点：所表示元素属于 ⟪ # n ⟫ 这一事实经 ∈#-elim 蕴含某个 k < n 满足 P。把这个截断见证交给 leastOf natOrder lem，在自然数序上使用排中律，把仅仅存在转化为被选出的最小序对 s。其第一分量是标号 k，其证书的第一分量是界 k < n，而这正是 Fin n 打包的数据。

  toFin : (n : ℕ) → ⟪ # n ⟫ → FB.Fin n
  toFin n m = k , k<n
    where
    s = leastOf natOrder lem (P n m) (∈#-elim n (⟪ # n ⟫↪ m) (member (# n) m))
    k : ℕ

toFin 的刻画比类型上的界说得更多：最小标号 k 满足 P 的完整的第二个合取支，即指标 m 表示 # k。这是最小元搜索返回证书的第二个分量，也是下面单射性证明要消费的那条路径。

    k = fst s
    k<n : k < n
    k<n = fst (fst (snd s))

  toFin-spec : (n : ℕ) (m : ⟪ # n ⟫) → ⟪ # n ⟫↪ m ≡ # (fst (toFin n m))
  toFin-spec n m = snd (fst (snd s))

toFin 的单射性沿标号相等的假设搬运两条刻画路径而得。若 toFin n m₁ 与 toFin n m₂ 相等，则其第一分量相等，于是 # (fst (toFin n m₁)) 与 # (fst (toFin n m₂)) 之间有路径；与两条刻画拼接便得到所表示元素之间的路径，而 ↪-inj 把所表示元素的相等反射回指标的相等，正如序数序处那样。

    where
    s = leastOf natOrder lem (P n m) (∈#-elim n (⟪ # n ⟫↪ m) (member (# n) m))

  toFin-inj : (n : ℕ) (m₁ m₂ : ⟪ # n ⟫) → toFin n m₁ ≡ toFin n m₂ → m₁ ≡ m₂
  toFin-inj n m₁ m₂ e = ↪-inj {a = # n}
    (toFin-spec n m₁ ∙ cong (λ k → # k) (cong fst e) ∙ sym (toFin-spec n m₂))

反方向从 #mono 出发：只要 k < n，它就见证 # k 是 # n 的成员。由于指标类型 ⟪ # n ⟫ 呈现 # n 的成员，这个成员资格附带一个纤维：一个所表示元素为 # k 的指标，连同恰为 fromFin-spec 所记录形状的证书。于是 fromFin n (k , k<n) 就是这个纤维的第一分量，由呈现方式选定，而非由最小元搜索选定。

  fromFin : (n : ℕ) → FB.Fin n → ⟪ # n ⟫
  fromFin n (k , k<n) = fiber (# n) (#mono k n k<n) .fst

  fromFin-spec : (n : ℕ) (i : FB.Fin n) → ⟪ # n ⟫↪ (fromFin n i) ≡ # (fst i)
  fromFin-spec n (k , k<n) = fiber (# n) (#mono k n k<n) .snd

  fromFin-inj : (n : ℕ) (i₁ i₂ : FB.Fin n) → fromFin n i₁ ≡ fromFin n i₂ → i₁ ≡ i₂

fromFin 的单射性利用了 Fin n 是子类型这一事实：其第二分量是有界自然数，一个取命题值的族，于是序对的相等可归约为第一分量的相等。由两条刻画与 e 得到的所表示元素之间的路径经 #-inj′ 转换为自然数之间的路径，Σ≡Prop 再把它提升为 Fin n 中的路径。本节随后引入 factor，定义为标准等价 factorEquiv : Fin n × Fin n ≃ Fin (n · n) 的正向部分，它用单个位置枚举位置对。

  fromFin-inj n i₁ i₂ e = Σ≡Prop (λ _ → isProp≤)
    (#-inj′ (sym (fromFin-spec n i₁) ∙ cong (⟪ # n ⟫↪) e ∙ fromFin-spec n i₂))

  factor : (n : ℕ) → FB.Fin n × FB.Fin n → FB.Fin (n · n)
  factor n = equivFun (factorEquiv {n = n} {m = n})

  factor-inj : (n : ℕ) (x y : FB.Fin n × FB.Fin n)

由于 factor 是等价而不只是函数，其单射性无需新的情形分析：若 factor n x 与 factor n y 相等，对两侧应用逆映射并使用往返定律 retEq，便回到 x 与 y 自身。证明就是 sym (retEq ...) x、被搬运的等式与 retEq ... y 的拼接。这正是前面指出的模式：形如逆映射的映射在逆定律补齐之前还不是逆映射，而这里由库中的等价提供了逆定律。

             → factor n x ≡ factor n y → x ≡ y
  factor-inj n x y e =
    sym (retEq (factorEquiv {n = n} {m = n}) x)
      ∙ cong (invEq (factorEquiv {n = n} {m = n})) e
      ∙ retEq (factorEquiv {n = n} {m = n}) y

鸽笼命题是后面矛盾的有限内核：不存在单射的函数 Fin (suc n) → Fin n。库中的结果 pigeonhole 以自反性见证 ≤-refl {m = suc n} 应用于 f，产出两个位置 i 与 j，连同「它们不同而 f i ≡ f j」的证书；把单射性假设与该等式复合，便得到空类型的元素。

  no-inj-Fin : (n : ℕ) → (f : FB.Fin (suc n) → FB.Fin n)
             → ((x y : FB.Fin (suc n)) → f x ≡ f y → x ≡ y) → Empty.⊥
  no-inj-Fin n f finj = i#j (finj i j feq)
    where
    i = fst (pigeonhole (≤-refl {m = suc n}) f)

这里的拆解把鸽笼证书分成末行所需的各部分：i 与 j 是两个碰撞位置，i#j 是它们的相异性，feq 是其像的等式。于是计算 i#j (finj i j feq) 把单射性假设应用于得到 i ≡ j，再交给相异性，产生矛盾。

    j = fst (snd (pigeonhole (≤-refl {m = suc n}) f))
    prf = snd (snd (pigeonhole (≤-refl {m = suc n}) f))
    i#j = fst prf
    feq : f i ≡ f j
    feq = snd prf

最后的模块从 ω 中抽象出来。它由族 E : ℕ → Type ℓ 参数化，并带有单射的编码器 toFinE : E n → Fin n 与单射的解码器 fromFinE : Fin n → E n。注意假设了什么、没有假设什么：每个方向各自带有自己的单射性证明，但不要求两者互逆，也不声称 E n 与 Fin n 之间存在等价。进入论证的只有这两个单射性。

  module AbstractChase (E : ℕ → Type ℓ)
                       (toFinE : (n : ℕ) → E n → FB.Fin n)
                       (toFinE-inj : (n : ℕ) (m₁ m₂ : E n) → toFinE n m₁ ≡ toFinE n m₂ → m₁ ≡ m₂)
                       (fromFinE : (n : ℕ) → FB.Fin n → E n)
                       (fromFinE-inj : (n : ℕ) (i₁ i₂ : FB.Fin n) → fromFinE n i₁ ≡ fromFinE n i₂ → i₁ ≡ i₂) where

在此设定内，内层模块 NoInj 固定一个类型 A，它从每个 E m 接收单射 into m，且该单射在每个层级上都是单的。其定理 no-inj 说：对任意 n，不存在单射 A → E n × E n。归约是直接的，因为所展示的证明只是把构造出的有限函数 g 连同其单射性交给 no-inj-Fin (n · n)。全部工作在于定义 g 并证明 g-inj。

    module NoInj (A : Type ℓ) (into : (m : ℕ) → E m → A)
                 (into-inj : (m : ℕ) (i₁ i₂ : E m) → into m i₁ ≡ into m i₂ → i₁ ≡ i₂) where

      no-inj : (n : ℕ) → (f : A → E n × E n)
             → ((x y : A) → f x ≡ f y → x ≡ y) → Empty.⊥
      no-inj n f finj = no-inj-Fin (n · n) g g-inj

映射 g 就是被禁止的单射 Fin (suc (n · n)) → Fin (n · n)，由复合构造而成。从比 n · n 大一的位置 i 出发，解码器 fromFinE 产生 E (suc (n · n)) 的元素，单射 into 把它送入 A，假设的映射 f 把它送到 E n 的一对元素，编码器 toFinE 再把每个分量变成 Fin n 中的位置。最后由 factor 把这对位置压缩为 Fin (n · n) 中的单个位置。

        where
        g : FB.Fin (suc (n · n)) → FB.Fin (n · n)
        g i = factor n ( toFinE n (fst (f (into (suc (n · n)) (fromFinE (suc (n · n)) i))))
                       , toFinE n (snd (f (into (suc (n · n)) (fromFinE (suc (n · n)) i)))))
        g-inj : (x y : FB.Fin (suc (n · n))) → g x ≡ g y → x ≡ y

g 的单射性把矛盾沿其构造的每一层向后传播。设 g x ≡ g y。由于 factor 是单射，编码位置的序对相等；由于 toFinE 是单射，该序对的两个分量作为 E n 的元素相等；由于 f 是单射，A 中的两个元素相等；由于 into 是单射，E (suc (n · n)) 中的两个元素相等；最后由于 fromFinE 是单射，得到 x ≡ y。所展示的项恰好沿这条链从内向外读。

        g-inj x y e = fromFinE-inj (suc (n · n)) x y
          (into-inj (suc (n · n))
            (fromFinE (suc (n · n)) x) (fromFinE (suc (n · n)) y)
            (finj Xx Xy pair-eq))
          where

where 块为中间值命名以保持链条可读。Xx 与 Xy 是把位置 x 与 y 解码再注入而得的 A 的两个元素；它们正是需要证明其 f 之下像相等的输入。命题 p-eq 记录了中间目标：两组编码位置一致。

          Xx : A
          Xx = into (suc (n · n)) (fromFinE (suc (n · n)) x)
          Xy : A
          Xy = into (suc (n · n)) (fromFinE (suc (n · n)) y)
          p-eq : (toFinE n (fst (f Xx)) , toFinE n (snd (f Xx)))

中间目标 p-eq 恰好由 factor 的单射性给出：对压缩位置之间的假设等式 e 应用 factor-inj，便把它转换回 Fin n 中位置对的相等，这里是 f Xx 与 f Xy 的两个分量的 toFinE 像所成的位置对。

               ≡ (toFinE n (fst (f Xy)) , toFinE n (snd (f Xy)))
          p-eq = factor-inj n
                   (toFinE n (fst (f Xx)) , toFinE n (snd (f Xx)))
                   (toFinE n (fst (f Xy)) , toFinE n (snd (f Xy))) e
          fst-eq : toFinE n (fst (f Xx)) ≡ toFinE n (fst (f Xy))

用 cong fst 与 cong snd 投影序对的相等，把它拆成第一与第二编码位置各自的相等。随后由编码器的单射性 toFinE-inj 把每一个转换回 f Xx 与 f Xy 相应分量的相等，得到 fst-eq′，以及一行之后的第二坐标对应版本。

          fst-eq = cong fst p-eq
          snd-eq : toFinE n (snd (f Xx)) ≡ toFinE n (snd (f Xy))
          snd-eq = cong snd p-eq
          fst-eq′ : fst (f Xx) ≡ fst (f Xy)
          fst-eq′ = toFinE-inj n (fst (f Xx)) (fst (f Xy)) fst-eq

两条分量相等由 ΣPathP 重新组装为序对的相等：它把第一分量的路径与第二分量的路径打包成依赖序对之间的路径。这个 pair-eq 恰好是最外层的单射性假设 finj 所消费的，从而完成了从 g-inj 开始的向后链条。

          snd-eq′ : snd (f Xx) ≡ snd (f Xy)
          snd-eq′ = toFinE-inj n (snd (f Xx)) (snd (f Xy)) snd-eq
          pair-eq : f Xx ≡ f Xy
          pair-eq = ΣPathP (fst-eq′ , snd-eq′)