---
title: "累积层级内的符号化"
module: V.Coding
lang: zh
site: "Bedrock"
description: "累积层级内的符号化"
stage: "环境层级"
reading_order: 23
canonical: https://bedrock.institute/zh/V.Coding.html
html: V.Coding.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Coding.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Coding, V.Hierarchy, V.Model]
routes: [ambient-model]
translations: [https://bedrock.institute/en/V.Coding.md, https://bedrock.institute/ja/V.Coding.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 累积层级内的符号化

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

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

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

```agda
{-# 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` 给出单射性证明将要分离的三种情形。

```agda
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` 是命题性的，所以下文每个分情形都可以消去到这种等式路径。

```agda
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` 负责提取这些记录。于是下文关于码的每个论证都表述为成员关系推理，而非展开嵌套花括号。

```agda
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 ℓ)` 上的直接运算与结构 `𝒮ᵥ` 就是章末编码实例解释被编码语法之处；本章的单射性证明只使用前述的后继事实与分类。

```agda
open InfinitySet using ( #_ )

open hPropStructure 𝒮ᵥ
```

## 数码两两相异

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

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

```agda
#⊆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)` 变成所要的那一个。

```agda
  (λ 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` 的一个元素。隶属的无自环性把这个元素消去为空类型的元素，所以这种情形不可能出现。

```agda
#-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′` 把同一个命题包装成序号隐式的形式，这正是编码接口所消耗的形状。

```agda
... | 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∈` 说等式足以保证属于。二者都是单点集包同一分类记录的投影。

```agda
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`。两条引入引理分别以截断的见证提供左右析取支，于是任一等式都能产生成员，而无需选择任何东西。

```agda
  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-集合，这是允许的。

```agda
  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)`。这个退化比较正是下文配对单射性的难处所在。

```agda
  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`。

```agda
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-集合，这是允许的。

```agda
  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 ⁆`。两者都需要：在下文的退化情形中，每条单独的记录都留有缺口，只有另一条能补上。

```agda
  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`。

```agda
  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` 为出发点，所以仅靠向前的分类到不了这个情形。

```agda
        (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`。第二种选择已是目标；第一种经与之前相同的复合和辅助引理也归结为它。

```agda
      (λ 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` 中路径构成的命题；从未从截断中选出任何见证。

```agda
          (λ 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 或选择假设进入；该实例只依赖分类规格与两条单射性证明。

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

## 小结

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