作为集合的语法

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

阅读指南 · 依赖地图

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

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

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

{-# 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 说不同的数落在不同的元素上。带标签对的构造消耗的正是这些假设；本章不再使用 𝒮 的其他任何内容。

  (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，因为编码不给语法附加任何集合论运算。空类型只作为不可能等式的值域出现，用于证明某些码不可能重合。

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ℕ 记录这一转换是单射的，因此按序号编码变元不会丢失信息。

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 中得出结论。

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 就把这一算术否证转化为所需的结论。

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。

⌜_⌝ᵗ : ∀ {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 是可用的变元槽位数，而不是某个具体词项实际使用的变元个数。

⌜⌝ᵗ-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 上，从不在集合自身上进行。

⌜_⌝ : ∀ {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 直接配上子公式的码。

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

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

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

编码关系

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

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

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 又把标签读出来；本节之所以成立，正是因为这两套编号彼此一致。

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 之间，且没有两个构造子共享标签，这正是标签能够识别构造子形状的原因。

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

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

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 ⊥̇ 也取同一个值，而不是省去这条子句。

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 成立。

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 出自对公式的同一套递归。下一块完成其余构造子，然后转向反方向。

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，槽位是两个词项，分别以构造子 _∈̇_ 与 _≐_ 收尾。

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 φ 就是单条路径 φ ≡ ⊥̇，根本没有序对。这表明该族随构造子形状而变化，并不强加统一的元数。

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 对每个自然数标签都有定义。

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)。

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 表明每条公式都与自己的标签匹配，于是仅凭标签就能把任何公式缩小到一种构造子形状。

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 ψ。由这些它必须返回 φ ≡ ψ。

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' 换回 ψ。相等子句把这一切换成 _≐_ 逐字重演。

    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 把右侧指向 ψ。这条配方就是其余联结词子句的全部内容。

  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 未被使用。

              (⌜⌝-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 收束。

  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 所期望的。

  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 的第二个参数，定理就此完成：无需十乘十地比较构造子，只需标签的算术加上沿载荷的递归。

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

小结

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