---
title: "作为集合的语法"
module: FOL.Coding
lang: zh
site: "Bedrock"
description: "作为集合的语法"
stage: "一阶逻辑"
reading_order: 19
canonical: https://bedrock.institute/zh/FOL.Coding.html
html: FOL.Coding.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Coding.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.Coding.md, https://bedrock.institute/ja/FOL.Coding.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 作为集合的语法

模型只能对其载体中的元素量化，而词项与公式起初存在于外部的类型论中。为了让模型内部能够使用语法，本章给每个词项和公式指派一个载体元素。一个码是带标签的对：数字标签识别最外层构造子，载荷保存各直接组成部分的码。集合常元已经属于载体，因此可以直接充当载荷。

构造假设有一个单射配对运算和一个从自然数出发的单射；这两个条件保证带标签对的两部分都能恢复。本章先证明词项编码为单射，再为公式的十个构造子定义编码。它还通过 `CodesT` 与 `Codes` 给出关系式编码的常元与隶属情形。最后，由标签索引的构造子形状描述支撑如下证明：同一元数的公式若码相等，则公式相等。

要把语法编码为集合，载体上的两个操作本身就够了，但真正让「解码」成为可能的是单射性：若两段语法得到同一个集合，编码就无法还原。因此本章在一个 `ZFStructure` 结构 `𝒮` 中工作；其等词与隶属关系取值于 `hProp ℓ`，编码所需的数据则取作显式的模块参数。下面每个定义都对任意一个带这类数据的结构成立；累积层级会在后面的章节中给出实例。

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

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Coding {ℓ} (𝒮 : ZFStructure ℓ)
```

这两份数据是一个单射配对和一个单射数字映射。`pr` 把载体 `S` 的两个元素映为它们的序对，`pr-inj` 说这个配对可以重新拆开：等式 `pr a b ≡ pr c d` 给出 `a ≡ c` 与 `b ≡ d` 两条路径组成的对。`encℕ` 把每个自然数送到 `S` 的一个元素，`encℕ-inj` 说不同的数落在不同的元素上。带标签对的构造消耗的正是这些假设；本章不再使用 `𝒮` 的其他任何内容。

```agda
  (pr       : ZFStructure.S 𝒮 → ZFStructure.S 𝒮 → ZFStructure.S 𝒮)
  (pr-inj   : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d))
  (encℕ     : ℕ → ZFStructure.S 𝒮)
  (encℕ-inj : ∀ {j k} → encℕ j ≡ encℕ k → j ≡ k)
  where
```

被编码的对象来自句法层：归纳类型 `Term` 与 `Formula`，由两个词项构造子 (集合常元 `con` 与变元 `var`) 和十个公式构造子组成，从原子式 `_∈̇_` 与 `_≐_` 一直到联结词以及有界与无界量词。结构本身只用到载体 `S`，因为编码不给语法附加任何集合论运算。空类型只作为不可能等式的值域出现，用于证明某些码不可能重合。

```agda
open ZFStructure 𝒮 using ( S )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

import Cubical.Data.Empty as Empty
```

两个小的算术事实支撑着单射性证明。其一，结构上不同的数字永不相等：引理 `znots` 与 `snotz` 分别否证 `0 ≡ suc k` 与 `suc j ≡ 0`，而带不同标签的两条公式被假设共享一个码时，产生的正是这类冲突。其二，`Fin n` 中的变元序号经 `toℕ` 转换为自然数，`inj-toℕ` 记录这一转换是单射的，因此按序号编码变元不会丢失信息。

```agda
open import Cubical.Data.Nat using ( znots; snotz )
open import Cubical.Data.FinData using ( toℕ; inj-toℕ )
```

## 带标签的对

唯一的构造：构造子序号与载荷配成对。单射性直接来自那两个参数，而冲突模式把「两个不同构造子相比较」时反复出现的情况集中处理。

基本构件是 `mkTag k x = pr (encℕ k) x`：标签是 `k` 的数字，载荷是 `x`，由于 `pr` 返回 `S` 的元素，二者都在 `S` 中。一个小例子可见标签如何区分形状：常元的码将是 `mkTag 0 x`，而序号为 `i` 的变元的码将是 `mkTag 1 (encℕ (toℕ i))`。若两个带标签对相等，标签必须一致；`mkTag-inj` 把这一点写清楚，复合 `pr-inj` 与 `encℕ-inj` 而返回 `(j ≡ k) × (x ≡ y)`。它的对偶 `clash` 处理否定情形：给定「标签 `j` 与 `k` 不可能相等」的证明，它从带标签对的等式中抽出标签等式，与该证明矛盾，从而在环境层级的任意类型 `A` 中得出结论。

```agda
mkTag : ℕ → S → S
mkTag k x = pr (encℕ k) x

mkTag-inj : ∀ {j k x y} → mkTag j x ≡ mkTag k y → (j ≡ k) × (x ≡ y)
mkTag-inj p = encℕ-inj (pr-inj p .fst) , pr-inj p .snd

clash : ∀ {j k x y} {A : Type ℓ} → (j ≡ k → Empty.⊥) → mkTag j x ≡ mkTag k y → A
```

`clash` 的主体把这一论证写成一行。`mkTag-inj p .fst` 是从假设的码等式中抽出的等式 `j ≡ k`；把它交给假设 `ne` 得到空类型的一个元素，`Empty.rec` 消去该元素，返回任意类型 `A` 中的值。每当两个构造子形状迫使数字 `0` 与 `suc _` 相等时，`clash` 就把这一算术否证转化为所需的结论。

```agda
clash ne p = Empty.rec (ne (mkTag-inj p .fst))
```

## 码

先看项，前文所说那点简洁在此出现：集合常元无须编码，因为它本来就是集合，只有变元的序号要被注入。不同项的码彼此可以分辨，单射性立得。

语境 `n` 中的词项由上面两条子句编码为 `S` 的元素。常元 `con x` 得标签 `0`、载荷 `x`，即该集合本身：这正是前文所说的省事之处，载荷无须另行编码。变元 `var i` 得标签 `1`、载荷 `toℕ i` 的数字，于是标签与序号分处序对的两侧，不会混淆。单射性证明按两个词项的构造子分情形。在常元对常元的情形只有载荷可能不同，故 `mkTag-inj p .snd` 直接就是 `x ≡ y`，再由 `cong con` 提升为 `con x ≡ con y`。

```agda
⌜_⌝ᵗ : ∀ {n} → Term S n → S
⌜ con x ⌝ᵗ = mkTag 0 x
⌜ var i ⌝ᵗ = mkTag 1 (encℕ (toℕ i))

⌜⌝ᵗ-inj : ∀ {n} (t u : Term S n) → ⌜ t ⌝ᵗ ≡ ⌜ u ⌝ᵗ → t ≡ u
⌜⌝ᵗ-inj (con x) (con y) p = cong con (mkTag-inj p .snd)
```

其余分支补完论证。混合情形中，码的相等将迫使数字 `0` 与 `1` 相等；由于 `1` 是后继，`znots` 或 `snotz` 恰好否证这一点，`clash` 再把否证转化为词项等式。变元对变元的情形，载荷等式说 `encℕ (toℕ i) ≡ encℕ (toℕ j)`；`encℕ-inj` 给出 `toℕ i ≡ toℕ j`，`inj-toℕ` 把它提升为 `i ≡ j`，再由 `cong var` 得 `var i ≡ var j`。每个分支都以词项等式收尾，故对每个固定的 `n`，码函数在 `Term S n` 上单射。注意这里的 `n` 是可用的变元槽位数，而不是某个具体词项实际使用的变元个数。

```agda
⌜⌝ᵗ-inj (con x) (var j) p = clash znots p
⌜⌝ᵗ-inj (var i) (con y) p = clash snotz p
⌜⌝ᵗ-inj (var i) (var j) p = cong var (inj-toℕ (encℕ-inj (mkTag-inj p .snd)))
```

然后是公式：十个构造子，十个标签。二元构造子把两个子码配成对，一元的直接取子码；「假」取一个虚设的载荷，因为标签已经决定了它。

公式沿用同样的带标签对方案，五个二元构造子分得标签 `0` 到 `4`。隶属原子式 `t ∈̇ u` 以标签 `0` 配上两个词项码组成的对来编码，相等式同样在标签 `1`；每个联结词把两条直接子公式的码配成对。与词项对比：那里的载荷是裸集合或数字，而这里的载荷本身可以是由码搭建的复合物，公式的整个结构就这样嵌套在载荷之中。递归发生在宿主的归纳类型 `Term` 与 `Formula` 上，从不在集合自身上进行。

```agda
⌜_⌝ : ∀ {n} → Formula S n → S
⌜ t ∈̇ u ⌝   = mkTag 0  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ t ≐ u ⌝   = mkTag 1  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ φ ∧̇ ψ ⌝   = mkTag 2  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ∨̇ ψ ⌝   = mkTag 3  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
```

蕴涵与其他联结词一样取标签 `4`。「假」`⊥̇` 是唯一没有部分的构造子：标签 `5` 本身已决定它，故载荷取虚设的数字 `encℕ 0`，只为让每个码都保持带标签对的统一形状。无界量词 `∃̇` 与 `∀̇` 是一元的，其码是标签 `6` 或 `7` 直接配上子公式的码。

```agda
⌜ φ ⇒̇ ψ ⌝   = mkTag 4  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ ⊥̇ ⌝       = mkTag 5 (encℕ 0)
⌜ ∃̇ φ ⌝     = mkTag 6 ⌜ φ ⌝
⌜ ∀̇ φ ⌝     = mkTag 7 ⌜ φ ⌝
⌜ ∀̇∈ t φ ⌝  = mkTag 8 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)
```

有界量词以标签 `8` 与 `9` 收尾。各自把界定词项的码与主体的码配成对。元数体现了约束：界定词项与整条公式处于同一语境 `n`，而主体的元数是 `suc n`，为被约束变元多出一个槽位。至此每个公式构造子都有互不相同的标签，而标签加载荷决定公式，这一点将在下一节证明。

```agda
⌜ ∃̇∈ t φ ⌝  = mkTag 9 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)
```

## 编码关系

模块接着记录编码的关系式表述的首批情形。`CodesT s t` 把集合与词项关联，`Codes s φ` 把集合与公式关联。本文件中，前者包含常元情形，后者包含隶属情形。

`CodesT` 的构造子 `c-con` 把码 `mkTag 0 x` 与常元 `con x` 关联起来。`Codes` 的构造子 `c-∈` 接受两个词项码的推导，把标签 `0` 下由二者组成的载荷与隶属公式关联起来。这些声明只覆盖此处列出的情形；下文的公式码单射性证明直接从 `⌜_⌝` 出发。

```agda
data CodesT {n : ℕ} : S → Term S n → Type ℓ where
  c-con : (x : S)     → CodesT (mkTag 0 x) (con x)

data Codes : {n : ℕ} → S → Formula S n → Type ℓ where
  c-∈  : ∀ {n s s'} {t u : Term S n}
       → CodesT s t → CodesT s' u → Codes (mkTag 0 (pr s s')) (t ∈̇ u)
```

## 码决定公式

同一元数、同一码的两条公式相等。证明不直接比较十个构造子的每一种配对，而是把公式码分成数字标签与载荷。一个由标签索引的类型族描述相应的构造子形状，配对的单射性则给出标签与载荷的相等。证明随后只沿载荷分量递归。

本节是一个按标签分离的证明。第一个材料 `tagOf` 把公式的构造子序号作为自然数读出，编号与 `⌜_⌝` 构造码时用的完全相同：隶属 `0`，相等 `1`，合取 `2`，析取 `3`。于是 `⌜_⌝` 把标签构造进集合，`tagOf` 又把标签读出来；本节之所以成立，正是因为这两套编号彼此一致。

```agda
tagOf : ∀ {n} → Formula S n → ℕ
tagOf (t ∈̇ u)  = 0
tagOf (t ≐ u)  = 1
tagOf (a ∧̇ b)  = 2
tagOf (a ∨̇ b)  = 3
```

其余子句把 `4` 到 `9` 分配给蕴涵、「假」、两个无界量词与两个有界量词。于是每条公式的标签都在 `0` 到 `9` 之间，且没有两个构造子共享标签，这正是标签能够识别构造子形状的原因。

```agda
tagOf (a ⇒̇ b)  = 4
tagOf ⊥̇        = 5
tagOf (∃̇ a)    = 6
tagOf (∀̇ a)    = 7
tagOf (∀̇∈ t a) = 8
```

第二个材料 `payOf` 以同样方式抽出载荷：隶属与相等是两个词项码的对，合取是两条子公式码的对。每条子句都是 `⌜_⌝` 对应子句的载荷分量，因此用 `tagOf` 与 `payOf` 读一个码，恰好还原出 `⌜_⌝` 放进去的数据。

```agda
tagOf (∃̇∈ t a) = 9

payOf : ∀ {n} → Formula S n → S
payOf (t ∈̇ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (t ≐ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (a ∧̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
```

析取与蕴涵把两个子码配成对，无界量词返回单个子码。「假」是抽取必须按约定与构造一致的情形：由于 `⌜ ⊥̇ ⌝` 以虚设数字 `encℕ 0` 为载荷，`payOf ⊥̇` 也取同一个值，而不是省去这条子句。

```agda
payOf (a ∨̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ⇒̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf ⊥̇        = encℕ 0
payOf (∃̇ a)    = ⌜ a ⌝
payOf (∀̇ a)    = ⌜ a ⌝
```

有界量词补完 `payOf`，各自把界定词项的码与主体的码配成对。接着 `shape` 记录两个方向之间的桥梁：对每条公式 `φ`，码 `⌜ φ ⌝` 等于 `mkTag (tagOf φ) (payOf φ)`。由于 `tagOf` 与 `payOf` 是从 `⌜_⌝` 的子句转录而来，对 `φ` 作匹配便把两边归约为同一个带标签对，各情形都由 `refl` 成立。

```agda
payOf (∀̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝
payOf (∃̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝

shape : ∀ {n} (φ : Formula S n) → ⌜ φ ⌝ ≡ mkTag (tagOf φ) (payOf φ)
shape (t ∈̇ u)  = refl
shape (t ≐ u)  = refl
```

这里展示的子句为析取、蕴涵、「假」与无界存在量词给出同样的论证：每种情形的等式都是定义性的，因为 `⌜_⌝`、`tagOf` 与 `payOf` 出自对公式的同一套递归。下一块完成其余构造子，然后转向反方向。

```agda
shape (a ∧̇ b)  = refl
shape (a ∨̇ b)  = refl
shape (a ⇒̇ b)  = refl
shape ⊥̇        = refl
shape (∃̇ a)    = refl
```

最后几条 `shape` 子句了结有界情形，构造到此转了一个方向：给定标签，描述带该标签的公式长什么样。类型族 `Match` 承担这个任务。对标签 `k`，`Match k φ` 是「`φ` 能由序号为 `k` 的构造子产生」的方式所成的类型：每个子公式槽位一层依值序对，末端是一条路径 `φ ≡` 加上构造子作用于这些槽位的结果。对标签 `0` 与 `1`，槽位是两个词项，分别以构造子 `_∈̇_` 与 `_≐_` 收尾。

```agda
shape (∀̇ a)    = refl
shape (∀̇∈ t a) = refl
shape (∃̇∈ t a) = refl

Match : ∀ {n} → ℕ → Formula S n → Type ℓ
Match {n} 0  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ∈̇ u)))
```

标签 `2` 到 `4` 为三个二元联结词重复同一模式，各自要求两条元数同为 `n` 的公式。标签 `5` 是退化情形：「假」没有槽位，故 `Match 5 φ` 就是单条路径 `φ ≡ ⊥̇`，根本没有序对。这表明该族随构造子形状而变化，并不强加统一的元数。

```agda
Match {n} 1  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ≐ u)))
Match {n} 2  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∧̇ b)))
Match {n} 3  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∨̇ b)))
Match {n} 4  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ⇒̇ b)))
Match     5 φ = φ ≡ ⊥̇
```

量词标签带有元数变化。标签 `6` 与 `7` 的唯一槽位是元数 `suc n` 的公式；标签 `8` 与 `9` 的两个槽位分别是元数 `n` 的词项与元数 `suc n` 的主体，对应构造子 `∀̇∈` 与 `∃̇∈`。其余标签没有任何公式可描述，故该族以空类型 `Empty.⊥*` 收尾；由此 `Match` 对每个自然数标签都有定义。

```agda
Match {n} 6 φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∃̇ a))
Match {n} 7 φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∀̇ a))
Match {n} 8 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∀̇∈ t a))
Match {n} 9 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∃̇∈ t a))
Match     _  _ = Empty.⊥*
```

计算见证的方向是容易的：`matches φ` 通过对 `φ` 的递归构造 `Match (tagOf φ) φ` 的一个元素。二元公式 `a ∧̇ b` 提供两个槽位 `a` 与 `b`，末端的路径是 `refl`，因为 `a ∧̇ b` 按定义等式由其部分重新组装。例如，`t ∈̇ u` 的见证就是三元组 `t , (u , refl)`。

```agda
matches : ∀ {n} (φ : Formula S n) → Match (tagOf φ) φ
matches (t ∈̇ u)  = t , (u , refl)
matches (t ≐ u)  = t , (u , refl)
matches (a ∧̇ b)  = a , (b , refl)
matches (a ∨̇ b)  = a , (b , refl)
```

其余构造子按各自 `Match` 行的形状处理：「假」只贡献 `refl`，每个无界量词把主体与 `refl` 配成对，每个有界量词给出界定词项与主体。覆盖最后一个构造子之后，`matches` 表明每条公式都与自己的标签匹配，于是仅凭标签就能把任何公式缩小到一种构造子形状。

```agda
matches (a ⇒̇ b)  = a , (b , refl)
matches ⊥̇        = refl
matches (∃̇ a)    = a , refl
matches (∀̇ a)    = a , refl
matches (∀̇∈ t a) = t , (a , refl)
```

定理 `⌜⌝-inj` 已近在眼前：对元数相同的公式 `φ` 与 `ψ`，等式 `⌜ φ ⌝ ≡ ⌜ ψ ⌝` 应当强制 `φ ≡ ψ`。证明归约为辅助函数 `go`，它在 `private` 块内给出，使导出的只有定理本身。`go` 的假设恰是标签分离所提供的东西：把 `ψ` 重新呈现为 `φ` 之标签的一次匹配，以及载荷相等 `payOf φ ≡ payOf ψ`。由这些它必须返回 `φ ≡ ψ`。

```agda
matches (∃̇∈ t a) = t , (a , refl)

⌜⌝-inj : ∀ {n} (φ ψ : Formula S n) → ⌜ φ ⌝ ≡ ⌜ ψ ⌝ → φ ≡ ψ

private
  go : ∀ {n} (φ ψ : Formula S n) → Match (tagOf φ) ψ → payOf φ ≡ payOf ψ → φ ≡ ψ
  go (t ∈̇ u) ψ (t' , (u' , q)) p =
```

隶属子句展示了全部机制，值得细读。匹配把 `ψ` 呈现为差一条路径 `q : ψ ≡ (t' ∈̇ u')` 的 `t' ∈̇ u'`，而假设 `p` 只给出 `φ` 与 `ψ` 的载荷相等，并非 `t' ∈̇ u'` 的载荷。把 `p` 与 `cong payOf q` 复合，等式便沿 `q` 转移，得到 `pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ ≡ pr ⌜ t' ⌝ᵗ ⌜ u' ⌝ᵗ`，`pr-inj` 再把它拆成词项码的等式。每条等式经已证的 `⌜⌝ᵗ-inj` 处理，`cong₂ _∈̇_` 在两侧重新装上构造子，末尾的 `sym q` 把右端从 `t' ∈̇ u'` 换回 `ψ`。相等子句把这一切换成 `_≐_` 逐字重演。

```agda
    cong₂ _∈̇_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (t ≐ u) ψ (t' , (u' , q)) p =
    cong₂ _≐_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
```

每个二元联结词都由这一个模式处理，因此把合取子句当作通用配方来陈述是值得的。匹配是三元组 `a' , (b' , q)`，其中 `q : ψ ≡ (a' ∧̇ b')`。转移后的载荷等式形如 `pr _ _ ≡ pr _ _`，`pr-inj` 给出两个子码的等式，`⌜⌝-inj` 递归地把它们提升为子公式的等式，`cong₂ _∧̇_` 重组出 `a ∧̇ b ≡ a' ∧̇ b'`，`sym q` 把右侧指向 `ψ`。这条配方就是其余联结词子句的全部内容。

```agda
  go (a ∧̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∧̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ∨̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∨̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
```

析取与蕴涵子句只是用各自的构造子实例化这条配方，其余不变。「假」是唯一完全不需要载荷操作的情形：匹配就是 `q : ψ ≡ ⊥̇`，于是 `sym q : ⊥̇ ≡ ψ` 已是所需的等式，载荷假设 `p` 未被使用。

```agda
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ⇒̇ b) ψ (a' , (b' , q)) p =
    cong₂ _⇒̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go ⊥̇ ψ q p = sym q
```

无界量词让配方更简单：载荷是单个子码，转移后的等式直接就是 `⌜ a ⌝ ≡ ⌜ a' ⌝`，一次递归调用包上 `cong ∃̇_` 或 `cong ∀̇_`，再以 `sym q` 收尾即可。有界量词 `∀̇∈` 则是两层编码在一个构造子中相遇之处：经 `pr-inj` 拆分后，项分量由 `⌜⌝ᵗ-inj` 解决，公式分量由递归的 `⌜⌝-inj` 解决，`cong₂ ∀̇∈` 把两者重组，最后照例以 `sym q` 收束。

```agda
  go (∃̇ a) ψ (a' , q) p = cong ∃̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇ a) ψ (a' , q) p = cong ∀̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∀̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
```

有界存在量词与有界全称平行，十个情形到此齐备。顶层随后组装定理。给定 `e : ⌜ φ ⌝ ≡ ⌜ ψ ⌝`，`go` 需要一个以 `φ` 之标签索引的 `ψ` 的匹配，而 `matches ψ` 位于 `ψ` 的标签处。作为数二者可能不同，因此匹配要被转移：`tp .fst` 是一条路径 `tagOf φ ≡ tagOf ψ`，沿其对称作 `subst` 便把 `matches ψ` 重定索引到类型 `Match (tagOf φ) ψ`，这正是 `go` 所期望的。

```agda
  go (∃̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∃̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q

⌜⌝-inj φ ψ e = go φ ψ
  (subst (λ k → Match k ψ) (sym (tp .fst)) (matches ψ)) (tp .snd)
```

局部定义 `tp` 造出这一转移所需的一对等式。把 `sym (shape φ)`、假设 `e` 与 `shape ψ` 串起来，码的相等被改写为带标签对之间的等式 `mkTag (tagOf φ) (payOf φ) ≡ mkTag (tagOf ψ) (payOf ψ)`，`mkTag-inj` 再把它拆成标签等式与载荷等式。标签等式驱动 `subst`，载荷等式成为 `go` 的第二个参数，定理就此完成：无需十乘十地比较构造子，只需标签的算术加上沿载荷的递归。

```agda
  where
  tp = mkTag-inj (sym (shape φ) ∙ e ∙ shape ψ)
```

## 小结

词项与公式如今都有 `S` 中的码：`⌜_⌝` 把构造子标签附到各部分的码上，常元则以其底层集合作为载荷。本文件记录关系式编码的常元情形与隶属情形，随后证明在固定元数下一个码至多决定一条公式。整个构造只以单射配对和自然数的单射为参数。