对后继封闭的序数层中的数码

有限序数提供公式码所用的数码。本章证明，当层的序数指标包含零且对后继封闭时，每个数码都属于该层。我们先处理任意单调且在后继层包含原序数的层族，再将结论应用于可构造层级。

本章固定一个宇宙层级 ℓ，并把层级 ℓ-suc ℓ 上的排中律作为显式参数 lem。把数码放进序数的初等归纳并不使用它；这里之所以携带这个假设，是因为可构造特化的一项原料，即序数出现在以其后继为指标的层这一定理，来自经典的序数层章节。

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

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

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

必须区分数码的两种呈现。周遭数码 # k 是 V ℓ 中的有穷 von Neumann 序数；模型数码 numeralL k 是 L 的元素，其底层集合为 # k。论证先为周遭序数证明界，随后才用投影等式 numeralL-fst 把结论转到模型呈现。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; Lset; Lset-mono )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Ordinal {ℓ} using ( numeral-ord )

周遭数码就生活在累积层级自身之中：∅ 是其中的空集，# k 是有 k 个成员的有限冯·诺伊曼序数，sucV 是后继步骤 a ↦ a ∪ {a}。注意 # (suc k) 定义地就是 sucV (# k)，因此 λ 对 sucV 封闭就自动覆盖零之后的每个数码。这里的真值是层级 ℓ-suc ℓ 上的命题，直接打包在 hProp 中，所以每条隶属断言都是命题。

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; module InfinitySet )
open InfinitySet using ( #_; sucV )

论证中的三种隶属各有作用：# k ∈ λ 把有穷序数置于指标之下；# k ∈ T (sucV (# k)) 把它置于自身的后继层；# k ∈ T λ 才是所求的界。它们都作为命题陈述，因而归纳与后续搬运不依赖证明的选择；三者之间的推导仍分别依靠后继封闭、序数层性质与单调性假设。

open hPropStructure 𝒮ᵥ

单调层族的界

设 λ 包含零且对后继封闭。归纳法先把每个数码 # k 放入 λ。要把同一个数码放入 T λ，先以 numeral-ord k 和后继层假设得到 # k ∈ T (sucV (# k))；后继封闭给出指标关系 sucV (# k) ∈ λ，单调性随即推出 # k ∈ T λ。

本节在固定载体 S 及其隶属 ⟨_∈ˢ_⟩ 上、其上的任意映射 T 以及关于 T 的两条假设来陈述。第一条 T-mono 把层指标的隶属 β ∈ α 连同 x ∈ T β 转换为 x ∈ T α。第二条 T-ord 是锚点：序数 δ 属于以其自身后继为指标的层 T (sucV δ)。

module BoundOver
  (T : S → S)
  (T-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ T β ⟩ → ⟨ x ∈ˢ T α ⟩)
  (T-ord : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ T (sucV δ) ⟩)
  (lam : S) (ordλ : IsOrd lam)

其余参数刻画指标 λ：它是一个集合，被证明为序数，包含 ∅，且对 sucV 封闭。证书 ordλ 记录 λ 自身是合法的序数层指标；两条封闭事实则是归纳法将要消耗的全部。

  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

每个周遭数码都落入 λ，其证明只使用刚才假设的两条封闭事实。这是论证中纯粹归纳的一半：不用排中律，不用 T 的任何性质，甚至连 λ 的序数证书也不参与。

对 k 归纳。基例恰是假设 ∅∈λ，因为 # 0 就是 ∅。归纳步中，# (suc k) 定义地就是 sucV (# k)，故把归纳假设 # k ∈ λ 交给 succλ 即得 # (suc k) ∈ λ。小情形显出形状：0 = ∅ ∈ λ，接着 {∅} = sucV ∅ ∈ λ，再接着数码 2 = sucV (sucV ∅) ∈ λ，每一步消耗一次后继封闭。

  #∈λ : (k : ℕ) → ⟨ (# k) ∈ˢ lam ⟩
  #∈λ zero    = ∅∈λ
  #∈λ (suc k) = succλ (# k) (#∈λ k)

属于 λ 是指标层面的陈述；属于层 T λ 是另一条不同的陈述，它需要 T 的两条性质，而不仅是 λ 的封闭性。路径要经过数码自身的后继层。

两步复合而成。第一步，在 δ = # k 处使用 T-ord，并以 numeral-ord k 证明该数码是序数，把 # k 放进 T (sucV (# k))。第二步，T-mono 把隶属从指标 sucV (# k) 提升到指标 λ：所需前提 # (suc k) ∈ λ 正是 #∈λ (suc k)，而它展开后就是 sucV (# k) ∈ λ，恰好是 T-mono 要求的指标间隶属。于是元素 # k 落入 T λ，序数证书在第一步中发挥了实际作用。

  #∈Tλ : (k : ℕ) → ⟨ (# k) ∈ˢ T lam ⟩
  #∈Tλ k = T-mono {α = lam} {β = sucV (# k)} (#∈λ (suc k))
    {x = # k} (T-ord (# k) (numeral-ord k))

可构造层级中的数码

可构造层具有单调性，每个序数也属于以后继为指标的层，因此一般的界适用于 L。我们还用模型内部的数码来表述这一隶属关系。

把抽象实例化只需指名见证。层族 T 取为 Lset，Lset-mono 提供沿序数指标隶属的单调性，ord∈Lset-suc 提供锚点：每个序数属于 Lset (sucV α)。定理 ord∈Lset-suc 携带这一特化所需的经典假设；数码归纳本身仍是前面给出的初等封闭论证。关于 λ 的假设原样传入，因此 BoundOver 内部关于 T λ 证明的一切，对 Lset lam 都同样可用。

module Bound (lam : S) (ordλ : IsOrd lam)
             (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
             (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

  open BoundOver Lset Lset-mono ord∈Lset-suc lam ordλ succλ ∅∈λ public

在模型内部，数码不是环境序数本身，而是一个序对 numeralL k，其第一分量指称该序数。这条界通过一次搬运转移到该呈现上，而不必重做归纳。

等式 numeralL-fst k 是宿主理论中的一条路径 fst (numeralL k) ≡ # k。沿这条路径搬运隶属类型族，即可把关于 # k 的隶属证明变为关于 fst (numeralL k) 的证明。使用 sym 把路径定向为：从已经证明的 # k 的隶属，得到所求的 fst (numeralL k) 的隶属；于是 #∈Tλ k 化为关于模型数码的陈述。

  num∈λ : (k : ℕ) → ⟨ fst (numeralL k) ∈ˢ Lset lam ⟩
  num∈λ k = subst (λ w → ⟨ w ∈ˢ Lset lam ⟩) (sym (numeralL-fst k)) (#∈Tλ k)