泛等公理

泛等公理是同伦类型论的核心要素之一, 是一个类型论公理, 可以表述如下: 宇宙中的相等类型与相应类型间的所有等价构成的类型相等价. 也就是说, 对类型 $A,B$, 有$$\mathrm{Id}(A,B)\simeq (A\simeq B),$$其中 $\mathrm{Id}$ 是宇宙 $\mathcal{U}$ 中的相等类型, 而等式右边可仅由 $A,B$ 而不借助 $\mathcal{U}$ 定义. 换言之, 这一公理要求宇宙具有好的性质, 以使得其中的相等类型是我们所希望的.

实际上, 上述公式并不准确, 因为类型论中的 J 公理本身能给出一个操作:

$${\mathrm{coe}}_{\simeq }:\mathrm{Id}(A,B)\to (A\simeq B).$$

泛等公理更准确的描述是 “${\mathrm{coe}}_{\simeq }$ 是一个等价”.

1定义

泛等公理最常见的用法是将一个等价转化为一个相等, 且证明这个转换本身是等价. 如下公式打包了这些操作:

$$\mathrm{Id}(A,B)\simeq (A\simeq B)$$

但直接引入这个公式作为公理有如下缺点:

•	常见的操作 (如等价到相等的转换) 的使用比起该公理本身更加频繁, 且

•	该公理本身会额外给出一个 $\mathrm{Id}(A,B)\to A\simeq B$ 的操作, 但我们已经有 ${\mathrm{coe}}_{\simeq }$ 了! 我们可能需要处理泛等公理给出的这个操作和 ${\mathrm{coe}}_{\simeq }$ 之间的相等关系, 这会带来额外的麻烦.

因此, 将该公式肢解后去掉多余的部分, 我们有如下三个公理作为该公式的替代品:

$$\begin{array}{rl}\mathrm{ua}& :(A\simeq B)\to \mathrm{Id}(A,B)\\ {\mathrm{ua}}_{\beta }& :\prod _{e:A\simeq B}\mathrm{Id}({\mathrm{coe}}_{\simeq }(\mathrm{ua}e),e)\\ {\mathrm{ua}}_{\eta }& :\prod _{p:\mathrm{Id}(A,B)}\mathrm{Id}(\mathrm{ua}({\mathrm{coe}}_{\simeq }p),p)\end{array}$$

首先, 这三个公理更加接近泛等公理的准确叙述: 它给出了证明 $\mathrm{isEquiv}({\mathrm{coe}}_{\simeq })$ 所需的组件.

其次, 这三个公理给出了更直观的 “化简” 规则: 若将 $\mathrm{ua}$ 操作类比为一种构造规则的话, 那么 ${\mathrm{coe}}_{\simeq }:\mathrm{Id}(A,B)\to A\simeq B$ 就是它的消去规则 (而由于这个函数本身也是由 J 规则实现的, 所以也可以认为 J 规则是它的消去规则), 然后 ${\mathrm{ua}}_{\beta }$ 就是它的计算规则、${\mathrm{ua}}_{\eta }$ 是唯一性规则.

配合 J 规则, 我们能通过这三个公理证明上面的公式.

2推论

泛等公理有很多非常深刻的推论.

函数外延性

主条目: 函数外延性

定义 2.1. 函数外延性指如下命题: 对于函数 $f,g:A\to B$, $$\mathrm{funExt}:\left(\prod _{a:A}{\mathrm{Id}}_B(f(a),g(a))\right)\to {\mathrm{Id}}_{A\to B}(f,g)$$

将 $\mathrm{Id}$ 写成等号的话 2.1 会更直观一些: $$\mathrm{funExt}:\prod _{a:A}(f(a)=g(a))\to f=g$$

引理 2.2. 泛等公理蕴涵函数的外延性. 换言之, 同伦类型论中函数的外延性总是成立.

首先, 在函数类型中已经指出 2.1 并不总是成立. 但它的反向函数却总是成立: 如果 $f=g$, 那么一定有 ${\Pi }_{a:A}(f(a)=g(a))$, 这是因为类型论中, 相等的表达式可以互相代换, 因此 $f=g$ 的话可知$$\left({\Pi }_{a:A}f(a)=g(a)\right)=\left({\Pi }_{a:A}f(a)=f(a)\right)$$而后者显然成立.

另外, 相等类型有一个重要的性质: $$A\simeq {\Sigma }_{a:A}{\Sigma }_{b:A}a=b$$这是因为 ${\Sigma }_{a:A}{\Sigma }_{b:A}a=b$ 这个类型中 ${\Sigma }_{b:A}a=b$ 这个部分没有任何信息, 它只是把 $a$ 的存在重复了一遍. 根据这两件事, 可以证明 2.2.

证明. 根据相等类型的性质和泛等公理, 可知 $B={\Sigma }_{a:B}{\Sigma }_{b:B}a=b$, 因此$$({\Sigma }_{f:A\to B}{\Sigma }_{g:A\to B}f=g)=(A\to B)=(A\to {\Sigma }_{a:B}{\Sigma }_{b:B}a=b)$$至此证明已经基本结束, 只需一些比较繁琐的手法将 ${\Pi }_{a:A}f(x)=g(x)$ 转换成 ${\Pi }_{a:A}{\Sigma }_{a:B}{\Sigma }_{b:B}a=b$ 的特例后, 用上面的连等即可得到 $f=g$.

$\square$

命题的外延性

参见: 命题宇宙

定义 2.3. 如下命题叫做命题外延性: 对于命题 $A,B$, 有$$(A\to B)\times (B\to A)\to \mathrm{Id}(A,B)$$

引理 2.4. 泛等公理蕴涵命题的外延性. 换言之, 同伦类型论中命题的外延性总是成立.

证明. 命题的外延性假设如下函数存在: $$\begin{array}{r}f:A\to B\\ g:B\to A\end{array}$$要通过泛等公理证明 $\mathrm{Id}(A,B)$ 的话只需证明 $A\simeq B$ 即可. 根据命题本身的性质可知对于任意 $a:A$, 有 $g(f(a)):A$ 和 $a$ 命题等价、反之亦然.

$\square$

结构等价原则

(...)

K 公理

主条目: K 公理

引理 2.5. 令 $2$ 为拥有两个互不相等实例的类型, 泛等公理蕴涵如下等价关系: $$\mathrm{Id}(\mathrm{Id}(2,2),2)$$

证明. 类型 $\mathrm{Id}(2,2)$ 拥有两个实例, 一个由泛等公理加上 “交换 $2$ 的两个元素” 这一等价给出, 另一个是恒同函数.

$\square$

定理 2.6. 泛等公理提供了 K 公理的反例.

证明. 根据 K 公理, 有 $\mathrm{Id}(\mathrm{Id}(2,2),1)$, 其中 $1$ 是单位类型. 显然 $1\ne 2$.

$\square$

这也可以作为一种 “J 公理不能推出 K 公理” 的矫枉过正的证明, 因为泛等公理和 J 公理是相容的.

3相关概念

•	泛等范畴
•	宇宙 (类型论)
•	编码-解码法

4参考文献

•	The Univalent Foundations Program (2013). “Homotopy type theory: Univalent foundations of mathematics”.

术语翻译

泛等公理 • 英文 univalence axiom • 法文 axiome d’univalence • 拉丁文 axioma de univalentia • 日文 一価性公理