数码链

本章从模型自身的空集、配对与并运算出发，在 L 内构造自然数链，并证明它投影到周遭集合层级中的冯·诺伊曼数码。

数学问题如下。集合 a 的冯·诺伊曼后继是 a ∪ {a}，而 L 的模型把自身的空集、无序对与并供给为典范实现者：每一个都是满足其成员规格的集合之可缩类型的中心，由摹状词算子 ℩ 读出。这样的中心是一个带规格的运算，而不是一条计算规则：其定义本身并未说明，它的底层集合就是周遭集合层级用自身配对与并造出的那个集合。因此，在把这条链与层级的数码链比较之前，需要一族投影等式，每一条说：模型的某个运算沿底层集合读出来，就是层级中对应的运算。

每条投影等式的论证有固定的形状。可缩类型的中心与一个显式构造的实现者比较：对配对而言，是把有界配对构造施于两个底层集的一个仅仅存在的公共层，该层由 isL-directed 供给。可缩性随后给出从中心到该实现者的路径，而把底层集合投影这个函数作用于该路径，便得到底层集合之间的等式。每一次对截断数据的消去之所以合法，只因目标是层级集合之间的等式，是命题；这又因层级的载体是 h-集合。有了投影等式，内部链与层级链逐步重合，而模型 record 向数码链要求的两条成员方程，也就沿着它们由层级自己的事实推得。

全章都是构造性的：不用排中律，不用 resize，也不需要实现者类型的可缩性之外的选择。本章不做的是把诸数码收集成一个集合；那一步收集正是无穷公理本身的内容。

关键概念是唯一实现。配对的规格是 λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)，而 hasPairL a b 证明实现它的可构造集的类型 SetOf 是可缩的：有一个典范实现者，即中心，并有从中心到每个其他实现者的路径。并由 hasUnionL 类似地规格化与证明。可缩性证明是显式数据，不是单纯的存在陈述：它同时包含中心与收缩，而下面要选的正是这个中心。这是本章用到的唯一形式的选择，且它由可缩性本身供给。

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

open import Base.Prelude
module L.Axioms.Numerals {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

投影等式让两侧相遇。模型一侧是 hasPairL 与 hasUnionL 及其实现构造 PairOf 与 UnionOf，以及内部空集 ∅ʟ。周遭集合一侧是层级的无序对 ⁅ _, _ ⁆ 与并 ⋃_、后继 sucV、数码 #_。把两侧绑在一起的输入是 isL-directed：它仅仅存在地给出一个容纳两个可构造集底层集合的公共序数层，而有界配对构造恰需这样一层才能造出实现者。这两个内部运算必须先被定义，然后才能比较。

import FOL.ZFModel
open import V.Model {ℓ} using ( pair-singleton; module NumPin )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( hasPairL; hasUnionL; module PairOf; module UnionOf; isL-directed; ∅ʟ )

投影等式是周遭集合层级集合之间的等式，例如 fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆。这个特定的等值类型之所以是命题，是因为层级的载体是 h-集合，setIsSet 证实的正是这一点。正是这个命题性使得把截断的层数据消去进去成为可能；这里并没有对任意等值类型主张命题性。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; ⋃_; module InfinitySet )

两条约定使代码可读。结构 𝒮ʟ 是呈现为集合论模型的可构造宇宙；打开其模型包即暴露 SetOf，即载体元素连同其实现规格的类型，以及 ℩，即返回可缩 SetOf 类型中心第一分量的算子。全文中，对载体 S 元素取 fst 得到周遭集合层级的底层集合，投影等式比较的恰是这些底层集合。

open InfinitySet using ( sucV; #_ )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; ℩ )

模型自己的运算

摹状词算子把实现者类型的可缩性变成运算：pairʟ 与 unionʟ 选出 hasPairL 与 hasUnionL 的中心，后继则把它们复合起来。

有一条区分主宰下文。从可缩类型选出的中心是带规格的运算，而不是计算规则。可缩性证明并未使 pairʟ a b 的底层集合化归为层级的对 ⁅ fst a , fst b ⁆；它提供的是从中心到每个实现者的路径，而下一节的投影等式正是沿这条路径把中心与显式构造的实现者比较得到的。三个运算都声明为 opaque，此后每一处使用都经它们的规格与投影等式读它们，而非经它们的构造。

算子 ℩ 接受一份可缩性证明，返回中心的第一个分量，即载体 S 的一个元素。把它用于 hasPairL a b 与 hasUnionL a，便得到可构造集上的两个函数。它们的输入是载体元素，即连同可构造性证书打包的集合，因此每个运算除输入已带的内容外无须再取实参。

opaque
  pairʟ : S → S → S
  pairʟ a b = ℩ (hasPairL a b)

  unionʟ : S → S
  unionʟ a = ℩ (hasUnionL a)

内部后继把两者复合：sucʟ a = unionʟ (pairʟ a (pairʟ a a))。内层的对是 a 与自身的无序对；稍后对底层集合施加的单点集律会把这个内层对认同为 {a}，而外层对的两个条目是 a 与该单点集，这正是该表达式坍缩为 a ∪ {a} 的方式。这里是外层的无序对及其两个条目，不是有序对，也不是它的某个分量。

  sucʟ : S → S
  sucʟ a = unionʟ (pairʟ a (pairʟ a a))

投影等式

可缩性把抽取出的运算与周遭集合层级中的无序对及并对应起来，从而给出内部后继的投影等式。

可缩类型的中心，表面上并不是层级会造出的那个集合：这里的运算是 opaque 的，因此本章用投影等式把它们与层级运算比较，而不展开其定义。但可缩性说的比存在更多：每个实现者都等于中心。因此证明用手头已有的层数据显式构造一个实现者，对它施加收缩，得到从中心到该实现者的路径。每次收缩都在一次对截断数据的消去内部施加，其目标是层级集合之间的等式；这个目标是命题，因为层级的载体是 h-集合，这正使消去合法。

陈述先固定目标：抽出的对的底层集合必须等于层级对底层集合所作的无序对。消去 PT.rec 打开 isL-directed 仅仅存在的公共层数据，而这一步合法，恰因目标是等式 fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆，而 setIsSet (fst (pairʟ a b)) ⁅ fst a , fst b ⁆ 证明这个等式类型是命题。在内部，送入的数据 σ , oσ , fa∈ , fb∈ 恰是 PairOf.mkPair 所消耗的，于是 mkPair 由它构造出一个实现者。证书提供的路径从中心指向那个实现者，方向不可颠倒。

  pairʟ-fst : (a b : S) → fst (pairʟ a b) ≡ ⁅ fst a , fst b ⁆
  pairʟ-fst a b = PT.rec (setIsSet (fst (pairʟ a b)) ⁅ fst a , fst b ⁆)
    (λ { (σ , (oσ , (fa∈ , fb∈))) →
         cong (λ (e : SetOf (PairOf.Q a b)) → fst (fst e))
           (hasPairL a b .snd (PairOf.mkPair a b σ oσ fa∈ fb∈)) })

最后一步把中心与显式构造的实现者等同。收缩 hasPairL a b .snd 对任意实现者给出一条从中心出发、终于该实现者的路径；把它用于 mkPair a b σ oσ fa∈ fb∈，得到类型 SetOf (PairOf.Q a b) 中的路径，该类型把载体元素连同其实现规格打包。把投影函数 λ e → fst (fst e) 作用于这条路径，先读出载体元素再读出其底层集合，把这条路径变成底层集合之间的等式，目标合拢。注意，截断的公共层数据只被消去到这条集合等式中，其命题性由 setIsSet 供给。并的情形是少一个输入的同一论证：UnionOf.mkUnion 只需一个容纳 fst a 的层，而证书 a .snd 正是那样的仅存层数据，消去直接消耗它。

    (isL-directed (fst a) (fst b) (a .snd) (b .snd))

  unionʟ-fst : (a : S) → fst (unionʟ a) ≡ ⋃ (fst a)
  unionʟ-fst a = PT.rec (setIsSet (fst (unionʟ a)) (⋃ (fst a)))
    (λ { (σ , (oσ , fa∈)) →
         cong (λ (e : SetOf (UnionOf.Q a)) → fst (fst e))

读这个结果：fst (unionʟ a) ≡ ⋃ (fst a)，模型并运算的底层集合就是层级对底层集合取的并。与配对等式合在一起，凡由模型的配对与并组装出的集合，沿底层集合读出来，就是由层级运算组装出的同一个集合。投影等式的用途正在于此：一步步比较两个后继运算，进而比较两条数码链。

           (hasUnionL a .snd (UnionOf.mkUnion a σ oσ fa∈)) })
    (a .snd)

后继等式就是那几条投影等式的复合，再加上层级自己对 {a, a} 与 {a} 的认同。先展开外层的并，再展开外层的对，再展开内层的对，最后消去重复的单点集，剩下的就是层级的后继。

每一步都把某个函数作用于已有等式，一次改写一个嵌套位置，所以复合从外向内进行。每个因子的方向都重要：配对等式从抽出的中心指向层级的对，于是把周遭「对取并」的函数作用于该等式，就把整个词项朝层级的形式搬运；而 pair-singleton 在最后按它陈述的方向使用。

前三个因子依次改写外层。并的投影等式在 pairʟ a (pairʟ a a) 处给出 fst (unionʟ ...) ≡ ⋃ (fst (pairʟ a (pairʟ a a)))。把函数 ⋃_ 作用于外层等式 pairʟ-fst a (pairʟ a a)，其实参改写为 ⋃ ⁅ fst a , fst (pairʟ a a) ⁆。再把函数 λ w → ⋃ ⁅ fst a , w ⁆ 作用于内层等式 pairʟ-fst a a，得到 ⋃ ⁅ fst a , ⁅ fst a , fst a ⁆ ⁆。内层重复对由 pair-singleton 等同于单点集；最后一个因子把这条等式置于同一个周遭函数内。

  sucʟ-fst : (a : S) → fst (sucʟ a) ≡ sucV (fst a)
  sucʟ-fst a =
      unionʟ-fst (pairʟ a (pairʟ a a))
    ∙ cong ⋃_ (pairʟ-fst a (pairʟ a a))
    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pairʟ-fst a a)

最后一个因子是层级自己的定律进入之处：pair-singleton (fst a) 是把重复的对 ⁅ fst a , fst a ⁆ 认同为单点集 ⁅ fst a ⁆ 的路径。把同一个函数作用于这条路径，它把词项变为 ⋃ ⁅ fst a , ⁅ fst a ⁆ ⁆，而后者恰是 sucV (fst a)。这串因子因此验证了那个陈述：内部后继沿底层集合读出来就是层级的后继。

    ∙ cong (λ w → ⋃ ⁅ fst a , w ⁆) (pair-singleton (fst a))

链

原始递归从内部零与后继定义 numeralL，归纳则证明 numeralL-fst，即它与周遭数码相等。

有了后继等式，链就可以沿自然数用普通递归写出，而一次归纳即说明它投影到层级的数码上。第零阶段是内部空集，其底层集合严格就是空集。

本节提供的是每个数码作为载体的元素，连同它的成员行为。它不把所有数码收集成一个集合，也不证明无穷公理；链只是后继等式的迭代，因此归纳只有一步有内容，零的情形是一次计算。

定义有两条子句。第零阶段是 ∅ʟ，即内部空集；其后每个阶段是把内部后继用于前一阶段。由于递归在自然数索引上进行，链是一个显式函数 ℕ → S：每个阶段都是载体的元素，因为 ∅ʟ、pairʟ 与 unionʟ 都返回这样的元素，而内部后继在每次迭代中都保持这一点。于是每个阶段都连同其可构造性证书一起到手。

  numeralL : ℕ → S
  numeralL zero    = ∅ʟ
  numeralL (suc n) = sucʟ (numeralL n)

  numeralL-fst : (n : ℕ) → fst (numeralL n) ≡ # n
  numeralL-fst zero    = refl

与周遭数码的对齐按 n 归纳证明。在零处，两边都计算为空集，路径是 refl。在后继处，把 sucʟ-fst 施于 numeralL n，把 fst (numeralL (suc n)) 认同为 sucV (fst (numeralL n))；再对归纳假设 fst (numeralL n) ≡ # n 把函数 sucV 作用于，把归纳步搬进后继内部。复合恰有 # (suc n) 的定义递归的形状，于是两条链在每个阶段都一致。

  numeralL-fst (suc n) = sucʟ-fst (numeralL n) ∙ cong sucV (numeralL-fst n)

两条成员方程

numeralL-zero 证明内部零没有成员，而 numeralL-suc 刻画下一数码的成员恰为前一数码的成员及前一数码自身。

模型 record 向数码链索取这两条律：零必须为空，且每个后继的成员恰是前者的成员连同前者自身，两条都经隶属陈述，而非经派生运算。正是这个措辞使证明很短：每一条都是关于层级数码的事实，沿投影族 numeralL-fst 搬运过来。全程从不展开摹状词算子。

NumPin 统一给出这一论证：它接受取值于周遭集合层级的链 a : ℕ → V ℓ 连同对齐 q : (n : ℕ) → a n ≡ # n，返回该链的两条成员方程。我们的链供给底层集族 λ k → fst (numeralL k) 与对齐 numeralL-fst。

零方程式取反驳的形状：链第零阶段的一个成员 z 导出空宿主类型的一个元素，所得函数类型在 hProp 设定下自身也是命题。pinZero 把假设的隶属沿第零处的对齐传输，把「属于 fst (numeralL zero)」变成「属于 # zero」，然后层级自己关于 ∅ 无成员的事实合拢证明。传输只走一个方向：从链到库数码。

numeralL-zero : (z : S) → ⟨ z ∈ˢ numeralL zero ⟩ → Empty.⊥
numeralL-zero z = NumPin.pinZero (λ k → fst (numeralL k)) numeralL-fst (fst z)

numeralL-suc : (n : ℕ) (z : S)
             → (⟨ z ∈ˢ numeralL (suc n) ⟩
                  → ⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩)

后继方程是一对蕴涵，其第二个分句使用结构关系 ≈ˢ；对当前限制结构，它的底层正是路径 fst z ≡ fst (numeralL n)。正向：numeralL (suc n) 的成员沿 suc n 处的对齐被传输为 # (suc n) 的成员，在那里层级自己对 sucV 成员的分析把它，仅仅存在地，分为「# n 的成员」与「就是 # n」两种情形；每个分支再沿 n 处的逆向对齐传回链上。反向：numeralL n 的成员被传输为 # n 后经 ∈sucV-inl 放进 # (suc n)，而与 numeralL n 相等的元素则把路径传到 # n，再使用层级自己「集合属于自己的后继」的事实。两个方向就是 pinSuc 对链 λ k → fst (numeralL k) 与对齐 numeralL-fst 的输出，实例化在 fst z 上。

             × (⟨ (z ∈ˢ numeralL n) ⊔ (z ≈ˢ numeralL n) ⟩
                  → ⟨ z ∈ˢ numeralL (suc n) ⟩)
numeralL-suc n z = NumPin.pinSuc (λ k → fst (numeralL k)) numeralL-fst n (fst z)

小结

numeralL 是 L 内部的冯·诺伊曼数码副本，满足模型 record 所要求的精确零与后继成员律。

本章的论证有三层。内部后继由唯一存在交出的、作为可缩中心的运算组装而成，投影等式在命题层面把这些运算的底层集合与层级的无序对、并及后继认同起来。然后沿自然数递归，从内部空集出发迭代内部后继，归纳证明 numeralL-fst，即把每个阶段的底层集合与周遭数码 # n 对齐的路径族。最后，把 NumPin 应用于这条对齐便得 numeralL-zero 与 numeralL-suc，两条成员律对内部链成立，而全部分情形分析都发生在层级的数码上。

这里确立的只是逐个数码的事实：每个 numeralL n 存在于 L 内并有正确的成员行为。本章没有把各阶段收集成一个集合的陈述，也没有证明无穷。投影等式的用途不止于数码：凡由模型的配对与并组装出的东西，沿底层集合读出来，就是用层级运算组装出的同一个东西。