L 中的无穷公理

L 内构造性定义的数码链 numeralL 为每个自然数给出一个内部数码。但一条由各自分离的集合组成的链还不是无穷集合：无穷公理要求一个可构造集合，其成员恰为诸数码。本章给出这个集合，并顺带指出把候选集合放进可构造层级时所用的经典依赖：所导入的层定理依赖序数比较，因此以模块参数 lem 为参数。

模块只带一个假设 lem : LEM (ℓ-suc ℓ)，即比工作层级 ℓ 高一层级的命题的判定。本章所需的一切，要么是构造性的，要么由这一个参数导出，因此后文的证明可以带着「哪些步骤是经典的」这一精确账目来读。

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

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

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

周遭集合层级提供 ω 与后继 sucV，而 numeralL-fst 把每个内部数码同 ω 的相应成员联系起来。以 lem 实例化的层定理 ord∈Lset-suc 把序数置于其后继层。下述证明只在这里调用以排中律为参数的结果。

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL )
open import L.Ordinal {ℓ} using ( suc-ord; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )

命题截断表达单纯存在：∣_∣₁ 把给定见证置于这一截断中。运算 ⇔toPath 把真值间的两个蕴涵转换为真值间的路径，这正是集合规格所要求的形式。

open import L.Axioms.Basic {ℓ} using ( uniqueL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )

这里的真值是 hProp 封装；其索引析取 ∃[ x ] P x 表达沿某个载体的单纯存在。对可构造结构 𝒮ʟ，∈ˢ 表示属于，≈ˢ 表示结构相等，其底层等式是周遭集合之间的等式。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

open hPropStructure 𝒮ʟ

最后，SetOf 指名一个类的实现者类型：一个可构造集合，连同「对每个元素，其属于真值等于该类的值」的证明。模型 record 的无穷字段将要求这个类型具有可缩性，而 uniqueL 会从单独一个实现者提供它。

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

收集这条链

周遭集合 ω 的成员是库中的数码，因此它是自然的候选。其可构造性证明把 ord∈Lset-suc 应用于 ω；这条导入的层定理以模块参数 lem 实例化。数码链及其成员规格的定义本身不调用该参数。

命题 ω∈L 具有 isL 定义所规定的截断形式。截断前的一个见证是层 sucV ω：ω-ord 说明 ω 是序数，suc-ord 说明其冯·诺伊曼后继 sucV ω 仍是序数，而 ord∈Lset-suc 把 ω 置于该层。元素 ωʟ 把周遭集合 ω 与这一可构造性证明配对，因此 x ∈ˢ ωʟ 就是对其底层周遭集合的属于关系。

ω∈L : ⟨ isL ω ⟩
ω∈L = ∣ sucV ω , (suc-ord ω-ord , ord∈Lset-suc ω ω-ord) ∣₁

ωʟ : S
ωʟ = ω , ω∈L

余下的工作是核实 ωʟ 的成员恰是内部数码。类 isNumeralL 对元素 x 说：存在某个自然数 n，使 x 结构上等于链的第 n 节；作为索引析取，它仅仅断言某个下标可行，而不选定任何一个。规格 ω-specL 接着证明，属于 ωʟ 与 isNumeralL 作为真值逐点一致；hasInfinityL 再把这个实现者提升为公理字段所要求的可缩性。规格的两个方向都经过同样两件素材：ω 中属于关系的周遭刻画，以及链的投影方程 numeralL-fst。

类 isNumeralL 沿载体 Lift ℕ 析取命题族 x ≈ˢ numeralL (lower n)。这里的 Lift 值得一提：∃[ x ] P x 要求载体住在工作层级，而 ℕ 住在 ℓ-zero；提升是纯粹的对齐层级的调整，恰带同样的元素，lower 取回普通下标。规格 ω-specL 把目标写成真值之间的一条路径 (x ∈ˢ ωʟ) ≡ isNumeralL x，而 ⇔toPath 把这条路径的证明化归为两个蕴涵的证明。

isNumeralL : S → hProp (ℓ-suc ℓ)
isNumeralL x = ∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralL (lower n)

ω-specL : (x : S) → (x ∈ˢ ωʟ) ≡ isNumeralL x
ω-specL x = ⇔toPath
  (PT.map (λ { (k , p) → lift (lower k)

两个方向都在命题截断内部映射见证。正向把提升后的下标写成 k : Lift ℕ，并令 n = lower k。ω 中的周遭属于关系给出 p : # n ≡ fst x，于是 sym p ∙ sym (numeralL-fst n) 证明 x ≈ˢ numeralL n。反向从 q : fst x ≡ fst (numeralL n) 构造路径 sym (q ∙ numeralL-fst n) : # n ≡ fst x，得到所需的周遭属于见证。因此 ωʟ 的成员恰为内部数码。最后，uniqueL 以显式实现者 (ωʟ , ω-specL) 为可缩中心，并给出从该中心到任意其他实现者的路径，从而证明 SetOf isNumeralL 可缩。

             , (sym p ∙ sym (numeralL-fst (lower k))) }))
  (PT.map (λ { (n , q) → lift (lower n)
             , (sym (q ∙ numeralL-fst (lower n))) }))

hasInfinityL : isContr (SetOf isNumeralL)
hasInfinityL = uniqueL isNumeralL (ωʟ , ω-specL)

小结

可构造集合 ωʟ 恰好收集数码链 numeralL。显式实现者与外延唯一性给出无穷字段所要求的可缩性。证明在确立 ω 的可构造性时通过 ord∈Lset-suc 使用排中律参数；成员规格本身则由上述两个投影路径得到。