公式码的字母表

关于可构造集合 W 的陈述往往会提到 W 的成员：比如说，要断言 W 中某个 x 满足一条性质，公式就要带着 x 作为参数。在集合论内部，这样的参数以一阶语言的常元符号出现。然而，外围的语法编码要求常元是层级 V ℓ 中的集合，而不是对任意集合成员的抽象指称。因此需要一座桥：一种字母表可索引 W 成员的语言，连同把每个索引送到其集合指称的嵌入。

本章对固定的 W 搭建这座桥。字母表是 W 底层集合的成员索引类型；嵌入把每个索引送到它所指称的集合，并附上该集合属于 W 的证书。沿嵌入改标每个常元后，字母表上的每个词项与每条公式都成为以集合为常元的语法，从而适用已有的取值于 V 的编码，得到词项码 ct 与公式码 cd。由于该编码不查看元数，沿元数相等路径传输公式不会改变其码，这正是 cd-subst 所记录的事实。

本章的一切都在唯一一个类型论宇宙层级 ℓ 上进行，它只固定一次并贯穿全章。该层级上的集合层级 V ℓ 是最终编码的目标，而一阶语言则是参数所处的舞台。方案是统一的：给定可构造集合 W，把其成员读作常元符号，用抽象索引为它们命名，再把每个名字传输到它在 V ℓ 中指称的集合。这一方案不依赖于所选的 W，因此对任意的 W 通用。

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

open import Base.Prelude

module L.Coding.CodeAlphabet {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

对象语言的语法对字母表是泛的。常元类型为 K、元数为 n 的公式类型 Formula K n 从不查看常元本身是什么，只把它们安排进逻辑结构中。因此，字母表上的任何函数都能扩充为语法的改标：把每个常元沿该函数映射，即可改写每一处出现，而联结词、量词与变量保持不变。这里所用的函数将是把成员索引嵌入 V ℓ 的映射，改标后的公式以集合为常元，恰好是层级上取值于集合的语法编码所要求的输入格式。剩下的只是选好字母表与嵌入，使这些常元确实是 W 的成员。

open import FOL.Syntax using ( Formula; Term )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import V.Coding {ℓ} using ( module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ )

open import Cubical.Foundations.Prelude using ( J; substRefl )

两个区分组织了整个构造。其一，层级的集合的成员由 ⟪ a ⟫ 中的抽象索引 q 呈现，嵌入 ⟪ a ⟫↪ 把该索引送到它所指称的集合；索引是名字，值 ⟪ a ⟫↪ q 是它在 V ℓ 中的指称，两种角色始终分开。其二，W 不是任意集合，而是可构造结构载体 S 的元素，因而带有层级中的底层集合 fst W 与可构造性证书；正是这一点使我们能把它的成员读作关于可构造集合的语言的参数。字母表将取为 ⟪ fst W ⟫ 本身，下一节把这些部件装配成码 ct 与 cd。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

open hPropStructure 𝒮ʟ using ( S )

嵌入常元并编码语法

本节把可构造集合 W 取为载体 S 的一个元素，考察如何把 W 上的语法编码为集合。构造由三步复合而成：提取可用常元符号的类型 Ab，把每个符号嵌入层级 V ℓ 并附上它确实属于 W 的证书，然后对换标后的词项与公式施以取值于集合的编码。末尾的引理处理一个因公式按元数索引而产生的记账问题。

元素 W : S 把层级中的一个集合与结构数据打包在一起；fst W 是其底层集合。于是 Ab 就是 ⟪ fst W ⟫，即该集合成员的索引类型，而 ι 是嵌入 ⟪ fst W ⟫↪，把每个索引送到它在 V ℓ 中所指称的成员。因此 Ab 的元素恰好就是一个可用常元符号，ι 则算出它作为集合的指称。

module Alphabet (W : S) where
  Ab : Type ℓ
  Ab = ⟪ fst W ⟫

  ι : Ab → V ℓ
  ι = ⟪ fst W ⟫↪

隶属证书 ι∈ 说明：对每个常元符号 q，集合 ι q 确实是 fst W 的成员；它由库中隶属关系与带分类的隶属关系 ∈ₛ 之间的等价直接读出。字母表就位后，cd 与 ct 几乎是被逼出来的：mapFo ι 与 mapTm ι 把每处常元 con q 替换为 con (ι q) 来改写公式或词项，随后层级编码的括号 ⌜_⌝ 与 ⌜_⌝ᵗ 把所得结果打包为集合。改标后公式的逻辑骨架原样保留，这正是能够复用该编码的原因。

  ι∈ : (q : Ab) → ⟨ ι q ∈ fst W ⟩
  ι∈ q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)

  cd : ∀ {n} → Formula Ab n → V ℓ
  cd ψ = VCode.⌜ mapFo ι ψ ⌝

  ct : ∀ {n} → Term Ab n → V ℓ

类型 Formula Ab n 的公式带有元数 n，而在依值类型论中该索引是类型的一部分。若某个证明稍后需要 n 与 n' 相等，它会沿路径 e : n ≡ n' 对公式作传输；传输后的公式在语法上是另一个居民，即便底层的公式未变。引理 cd-subst 表明这对编码毫无影响：作用于传输后公式的 cd 等于作用于原公式的 cd。证明对 e 使用 J，自反情形成立是因为沿 refl 的传输是恒等，而 substRefl 把这一化简显式化，剩下由 cong cd 把两次作用等同起来。

  ct t = VCode.⌜ mapTm ι t ⌝ᵗ

  cd-subst : ∀ {n n'} (e : n ≡ n') (ψ : Formula Ab n) → cd (subst (Formula Ab) e ψ) ≡ cd ψ
  cd-subst {n} e ψ = J (λ n' e' → cd (subst (Formula Ab) e' ψ) ≡ cd ψ)
    (cong cd (substRefl {B = Formula Ab} ψ)) e

小结

Alphabet W 把可构造集合 W 的成员看作一阶语言的常元符号，将每个成员嵌入外围层级并附上证书 ι∈，再通过 ct 与 cd 给出词项与公式所得的集合码。由于编码从不查看元数，cd-subst 保证了沿元数相等的路径传输公式不会改变其码。