累积层级内的符号化

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

FOL.Coding 中的通用编码构造只需要载体上的两个单射操作：单射的配对，以及从自然数出发的单射映射。要为累积层级上的语法编码，二者都必须在集合中找到，而层级本身提供了它们。自然数方面，层级自身的 von Neumann 数码即可胜任。较小的数码属于较大的，因为每个数码都在自己的后继之内，而没有集合属于自身；于是经自然数三歧性比较的相异序号给出相异的集合。配对方面，Kuratowski 编码即可胜任：a 与 b 的对，是以单点集 ⁅ a ⁆s 与无序对 ⁅ a , b ⁆ 为成员的那个集合。于是第一分量可作为公共元素还原，第二分量则作为另一个 (可能相等的) 元素还原。

两个论证都受类型论的一条约束。层级集合中的小隶属是命题截断的，所以对它的分情形只能消去到命题。由于 V 是 h-集合，V 中的等式是命题性的，而由这些等式构成的路径命题恰好是下文推理所需的目标。在这一消去限制下，每一步都取值于命题，从不从截断中提取任何见证。

本章在固定的宇宙层级 ℓ 上陈述：层级的结构 𝒮ᵥ 是码所寄居的载体，其隶属关系正是被分析的对象。最终的编码实例使用高一层级 hProp (ℓ-suc ℓ) 中的真值。

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

open import Base.Prelude

module V.Coding {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

数码的论证依赖层级中关于后继的两条隶属事实：一个集合总属于它自己的后继，而一个集合的成员属于该集合的后继。施于数码，第一条说 # n ∈ # (suc n)，第二条说 # n 的成员在 # (suc n) 中得以保留。自然数上的序随之判定哪个数码更小，三歧比较 m ≟ n 给出单射性证明将要分离的三种情形。

import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl )

open import Cubical.Data.Nat.Order using ( _<_; <-split; ¬-<-zero; _≟_; lt; eq; gt )
import Cubical.Data.Empty as Empty

这一消去限制的精确形式如下。小隶属陈述 ⟨ x ∈ₛ s ⟩ 经截断后是命题，因此当假设给出隶属的截断析取时，消去的目标必须是命题。由于 V 是 h-集合 (setIsSet 所证)，层级集合之间的路径类型 x ≡ y 是命题性的，所以下文每个分情形都可以消去到这种等式路径。

import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )

Kuratowski 码所需的两个集合构造都自带隶属分类。对无序对 ⁅ a , b ⁆，分类 pairing-ax 说：在截断的意义下，x 属于它仅仅当 x ≡ a 或 x ≡ b。单点集 ⁅ a ⁆s 经单点集包带有类似的分类，SetPackage.classification 负责提取这些记录。于是下文关于码的每个论证都表述为成员关系推理，而非展开嵌套花括号。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)

数码 # n 以 #_ 记之，是在层级中表示自然数 n 的 von Neumann 序数。两个字母表在手之后，hProp (ℓ-suc ℓ) 上的直接运算与结构 𝒮ᵥ 就是章末编码实例解释被编码语法之处；本章的单射性证明只使用前述的后继事实与分类。

open InfinitySet using ( #_ )

open hPropStructure 𝒮ᵥ

数码两两相异

第一个字母表是数码映射，其单射性分成两个命题。单调性说较小的数码属于较大的。归纳沿较大的那个序号进行，使每个归纳步都是句法上的后继，索引上不出现任何算术。后继一步按自然数三歧性分成严格更小的序号与相等的序号，各由一条关于后继的隶属事实解决；基例则是空洞的。单射性随之得出：若两个相异序号的码相同，单调性会把某个数码放进它自身，而隶属的无自环性禁止这一点。

垫脚石 #⊆suc 说：# n 的任何成员也是下一个数码的成员；这正是「集合的成员属于该集合的后继」这条后继事实。#mono 的基例无事可证，因为没有序号严格小于零，假设 m < 0 被直接驳倒。

#⊆suc : (n : ℕ) {x : S} → ⟨ x ∈ˢ (# n) ⟩ → ⟨ x ∈ˢ (# (suc n)) ⟩
#⊆suc n {x} = ∈sucV-inl {A = # n} {x = x}

#mono : (m n : ℕ) → m < n → ⟨ (# m) ∈ˢ (# n) ⟩
#mono m zero    m<0    = Empty.rec (¬-<-zero m<0)
#mono m (suc n) m<sucn = Sum.rec

在后继一步，<-split 只是说 m < suc n 分裂为 m < n 或 m ≡ n。第一支中归纳假设给出 # m ∈ # n，再由 #⊆suc 提升到后继。第二支中两个数码重合，而一个集合属于它自己的后继，于是沿 m ≡ n 的逆向传输把隶属 # n ∈ # (suc n) 变成所要的那一个。

  (λ m<n → #⊆suc n (#mono m n m<n))
  (λ m≡n → subst (λ M → ⟨ (# M) ∈ˢ (# (suc n)) ⟩) (sym m≡n) (self∈sucV (# n)))
  (<-split m<sucn)

单射性由序号上的三歧得出。序号相等即是结论。若 m < n，单调性给出 # m ∈ # n，而假设的等式 # m ≡ # n 把这个隶属传输为 # n ∈ # n，这与隶属的无自环性矛盾。剩下的情形 n < m 是镜像，传输沿另一方向进行。

严格更小的情形最具启发性。隶属 # m ∈ # n 说的是数码 # m；沿 # m ≡ # n 对其类型作重写后，那个集合处处被替换为 # n，得到 # n ∈ # n 的一个元素。隶属的无自环性把这个元素消去为空类型的元素，所以这种情形不可能出现。

#-inj : (m n : ℕ) → # m ≡ # n → m ≡ n
#-inj m n #m≡#n with m ≟ n
... | eq m≡n = m≡n
... | lt m<n = Empty.rec (∈-irrefl (# n)
      (subst (λ z → ⟨ z ∈ˢ (# n) ⟩) #m≡#n (#mono m n m<n)))

更大的情形完全相同，只是交换 m 与 n 的角色：单调性把 # n 放进 # m，等式沿反方向传输，而 # m 的无自环性将它驳倒。变体 #-inj′ 把同一个命题包装成序号隐式的形式，这正是编码接口所消耗的形状。

... | gt n<m = Empty.rec (∈-irrefl (# m)
      (subst (λ z → ⟨ z ∈ˢ (# m) ⟩) (sym #m≡#n) (#mono n m n<m)))

#-inj′ : ∀ {m n} → # m ≡ # n → m ≡ n
#-inj′ {m} {n} = #-inj m n

Kuratowski 配对

第二个单射字母表是 Kuratowski 对：a 与 b 的码是以单点集 ⁅ a ⁆s 与无序对 ⁅ a , b ⁆ 为成员的那个集合。注意区分记录了次序的外层有序对与不记录次序的内层无序对。单射性意为两个分量都能从码中还原，而这种还原完全由分类规格驱动：属于单点集等于等于其唯一的元素，属于无序对仅仅意味着等于两个分量之一。

单点集分类在两个方向上各命名一次。∈singl 说 ⁅ a ⁆s 的成员必等于 a，singl∈ 说等式足以保证属于。二者都是单点集包同一分类记录的投影。

private
  ∈singl : {a x : S} → ⟨ x ∈ₛ ⁅ a ⁆s ⟩ → x ≡ a
  ∈singl {a} {x} = SetPackage.classification (SingletonPackage a) x .fst

  singl∈ : {a x : S} → x ≡ a → ⟨ x ∈ₛ ⁅ a ⁆s ⟩
  singl∈ {a} {x} = SetPackage.classification (SingletonPackage a) x .snd

对无序对，分类呈截断析取的形状：⁅ a , b ⁆ 的成员仅仅等于 a 或等于 b。两条引入引理分别以截断的见证提供左右析取支，于是任一等式都能产生成员，而无需选择任何东西。

  self∈singl : (a : S) → ⟨ a ∈ₛ ⁅ a ⁆s ⟩
  self∈singl a = singl∈ refl

  inl∈⁅,⁆ : {a b x : S} → x ≡ a → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩
  inl∈⁅,⁆ {a} {b} {x} e = pairing-ax a b x .snd ∣ inl e ∣₁

  inr∈⁅,⁆ : {a b x : S} → x ≡ b → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩

单点集决定其元素：若 ⁅ a ⁆s ≡ ⁅ c ⁆s，沿这条路径传输隶属 a ∈ ⁅ a ⁆s 并对结果分类，结果必等于 c。消去指向路径命题 a ≡ c，由于 V 是 h-集合，这是允许的。

  inr∈⁅,⁆ {a} {b} {x} e = pairing-ax a b x .snd ∣ inr e ∣₁

  mem⁅,⁆ : {a b x : S} → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩ → ∥ (x ≡ a) ⊎ (x ≡ b) ∥₁
  mem⁅,⁆ {a} {b} {x} = pairing-ax a b x .fst

  singl-inj : {a c : S} → ⁅ a ⁆s ≡ ⁅ c ⁆s → a ≡ c
  singl-inj {a} {c} q = ∈singl (subst (λ s → ⟨ a ∈ₛ s ⟩) q (self∈singl a))

若一个单点集恰好等于某个无序对，则无序对的两个分量都被压到该单点集的元素。每个分量仅仅属于该无序对，于是沿 sym q 传输其隶属再分类，得到从该分量到 a 的路径；两个消去都指向路径命题的对 (c ≡ a) × (d ≡ a)。这个退化比较正是下文配对单射性的难处所在。

  singl≡pair : {a c d : S} → ⁅ a ⁆s ≡ ⁅ c , d ⁆ → (c ≡ a) × (d ≡ a)
  singl≡pair {a} {c} {d} q =
      ∈singl (subst (λ s → ⟨ c ∈ₛ s ⟩) (sym q) (inl∈⁅,⁆ {a = c} {b = d} refl))
    , ∈singl (subst (λ s → ⟨ d ∈ₛ s ⟩) (sym q) (inr∈⁅,⁆ {a = c} {b = d} refl))

配对的单射性证明现在由四条比较引理组装而成。给定 p : pr a b ≡ pr c d，码的单点集部分同时属于两侧，于是沿 p 向前传输其隶属再分类，仅仅得到 ⁅ a ⁆s ≡ ⁅ c ⁆s 或 ⁅ a ⁆s ≡ ⁅ c , d ⁆；第一支立即给出 a ≡ c，第二支经 singl≡pair 的逆向给出。无序对部分更难，因为仅凭其隶属未必能确定第二分量：当码退化时，⁅ a , b ⁆ 在左或右与一个单点集相配，而知道它配的是哪一侧并不够。于是保留两条截断记录：一条是 ⁅ a , b ⁆ 在 pr a b 中的隶属沿 p 向前传输所得，另一条是 ⁅ c , d ⁆ 在 pr c d 中的隶属沿 p 的逆向传输所得。向后那条记录恰好补上退化分支所缺的信息；在临时假设 a ≡ b 之下，即整个码退化为「单点集的单点集」的情形，它把还原出的 a ≡ b 转换为 d ≡ b。本证明中对截断析取的每次消去都指向由 h-集合 V 中路径构成的命题，因此从不选出任何见证。

码 pr a b 是以单点集 ⁅ a ⁆s 与无序对 ⁅ a , b ⁆ 为两个成员的无序对。外层表达式是有序的 Kuratowski 码，不要与它的第二个原料混淆：内层的 ⁅ a , b ⁆ 不记录次序，记录次序的是整个码。单射性是说码的等式 pr a b ≡ pr c d 决定两个输入，即给出路径 a ≡ c 与 b ≡ d。

pr : S → S → S
pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆

pr-inj : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d)
pr-inj {a} {b} {c} {d} p = a≡c , b≡d
  where

第一分量。单点集部分 ⁅ a ⁆s 经其右析取支属于 pr a b。把这个隶属沿 p 传输再分类，仅仅得到 ⁅ a ⁆s ≡ ⁅ c ⁆s 或 ⁅ a ⁆s ≡ ⁅ c , d ⁆ (这就是 H₁)。第一支由 singl-inj 直接给出 a ≡ c。第二支中比较 singl≡pair 迫使 c ≡ a，取其逆向即所求。截断析取消去到路径命题 a ≡ c，由于 V 是 h-集合，这是允许的。

  H₁ : ∥ (⁅ a ⁆s ≡ ⁅ c ⁆s) ⊎ (⁅ a ⁆s ≡ ⁅ c , d ⁆) ∥₁
  H₁ = mem⁅,⁆ (subst (λ s → ⟨ ⁅ a ⁆s ∈ₛ s ⟩) p (inl∈⁅,⁆ {b = ⁅ a , b ⁆} refl))

  a≡c : a ≡ c
  a≡c = PT.rec (setIsSet a c)
    (Sum.rec singl-inj (λ e → sym (singl≡pair e .fst))) H₁

第二分量。这里收集两条截断的记录。H₂ 来自无序对部分在 pr a b 中的成员，沿 p 向前传输：仅仅有 ⁅ a , b ⁆ 等于 ⁅ c ⁆s 或 ⁅ c , d ⁆。K 把同一论证反向运行，从 ⁅ c , d ⁆ 在 pr c d 中的成员沿 sym p 传输得到：仅仅有 ⁅ c , d ⁆ 等于 ⁅ a ⁆s 或 ⁅ a , b ⁆。两者都需要：在下文的退化情形中，每条单独的记录都留有缺口，只有另一条能补上。

  H₂ : ∥ (⁅ a , b ⁆ ≡ ⁅ c ⁆s) ⊎ (⁅ a , b ⁆ ≡ ⁅ c , d ⁆) ∥₁
  H₂ = mem⁅,⁆ (subst (λ s → ⟨ ⁅ a , b ⁆ ∈ₛ s ⟩) p (inr∈⁅,⁆ {a = ⁅ a ⁆s} refl))

  K : ∥ (⁅ c , d ⁆ ≡ ⁅ a ⁆s) ⊎ (⁅ c , d ⁆ ≡ ⁅ a , b ⁆) ∥₁
  K = mem⁅,⁆ (subst (λ s → ⟨ ⁅ c , d ⁆ ∈ₛ s ⟩) (sym p) (inr∈⁅,⁆ {a = ⁅ c ⁆s} refl))

  d≡b-from-K : a ≡ b → d ≡ b

辅助引理 d≡b-from-K 在临时假设 a ≡ b 之下处理退化情形：码的两个原料重合，pr a b 退化为无序对 ⁅ ⁅ a ⁆s , ⁅ a ⁆s ⁆。读 K：要么 ⁅ c , d ⁆ 等于单点集 ⁅ a ⁆s，其分类迫使 d ≡ a，从而 d ≡ b；要么它等于 ⁅ a , b ⁆，此时 d 仅仅等于 a 或 b，两种选择都能复合成 d ≡ b。所有消去都落入路径命题 d ≡ b。

  d≡b-from-K a≡b = PT.rec (setIsSet d b)
    (Sum.rec
      (λ e → singl≡pair (sym e) .snd ∙ a≡b)
      (λ e → PT.rec (setIsSet d b)
        (Sum.rec (λ d≡a → d≡a ∙ a≡b) (λ d≡b → d≡b))

b ≡ d 的主论证沿 H₂ 进行。在其第一支中，内层无序对 ⁅ a , b ⁆ 等于单点集 ⁅ c ⁆s；反向读取比较 singl≡pair 给出 b ≡ c，而由 a ≡ c 与 b ≡ c 的逆向复合得到路径 a ≡ b，恰好是辅助引理所消耗的假设。辅助引理随即给出 d ≡ b，取其逆向即目标。这正是反向记录 K 的用武之地：辅助引理以 K 为出发点，所以仅靠向前的分类到不了这个情形。

        (mem⁅,⁆ (subst (λ s → ⟨ d ∈ₛ s ⟩) e (inr∈⁅,⁆ {a = c} refl)))))
    K

  b≡d : b ≡ d
  b≡d = PT.rec (setIsSet b d)
    (Sum.rec

在 H₂ 的第二支中，两个内层无序对重合：⁅ a , b ⁆ ≡ ⁅ c , d ⁆。于是 b 仅仅属于 ⁅ c , d ⁆，对 b 的成员作分类给出 b ≡ c 或 b ≡ d。第二种选择已是目标；第一种经与之前相同的复合和辅助引理也归结为它。

      (λ e → let b≡c = singl≡pair (sym e) .snd
             in sym (d≡b-from-K (a≡c ∙ sym b≡c)))
      (λ e → PT.rec (setIsSet b d)
        (Sum.rec
          (λ b≡c → sym (d≡b-from-K (a≡c ∙ sym b≡c)))

两个分支合成为 b ≡ d，完成 pr-inj：Kuratowski 码的两个分量都可从码的等式中还原。每个分支都把一个截断析取消去到由 h-集合 V 中路径构成的命题；从未从截断中选出任何见证。

          (λ b≡d → b≡d))
        (mem⁅,⁆ (subst (λ s → ⟨ b ∈ₛ s ⟩) e (inr∈⁅,⁆ {a = a} refl)))))
    H₂

实例

有了两个单射字母表，FOL.Coding 的通用编码构造即可施于层级：单射的配对与单射的数码映射是它的两个参数。得到的 VCode 给层级载体上的词项与公式指派本身仍是层级集合的码。它并不把每个集合都变成码；它为被编码的语法提供取值为集合的码。

注意层级：VCode 取在 ℓ-suc ℓ 上，即ZFStructure 𝒮ᵥ 的关系取值所在的层级。这个宇宙指标是类型论意义上的层级，不是层级的层。

实例化传入层级 ℓ-suc ℓ、结构 𝒮ᵥ，以及上文确立的四份数据：pr 与 pr-inj，数码映射 #_ 与 #-inj′。没有任何经典公理、resizing 或选择假设进入；该实例只依赖分类规格与两条单射性证明。

module VCode = FOL.Coding {ℓ-suc ℓ} 𝒮ᵥ pr pr-inj #_ #-inj′

小结

通用编码所需的两个单射操作原本就在层级之中。数码单射：#-inj 由单调性与隶属的无自环性、在自然数三歧性之下得出。Kuratowski 对单射：pr-inj 经单点集与无序对的分类规格还原两个分量。于是实例 VCode 在层级 ℓ-suc ℓ 上、且不带任何经典假设地供给了 FOL.Coding 的构造。层级集合上的词项与公式如今拥有本身是 V 中集合的码，Codes 关系可用于对它们推理。