等价 (类型论)

等价在类型论中是函数类型实例的性质, 即给出一个 $\mathrm{isEquiv}:(A\to B)\to \mathrm{Prop}$, 命题宇宙保证一个函数只给出一个等价. 这个定义需要满足如下性质: $\mathrm{isEquiv}f$ 在逻辑上等价于 (即两者能够互相推导)

存在 $g:B\to A$, 使得能够给出 $\mathrm{Id}(f(gx),x)$ 与 $\mathrm{Id}(g(fy),y)$.

一般来说, 后者并不是命题. 直觉上来说, 若两类型等价, 那么应该存在一组互逆的转换函数.

可以看出, 在同构 (即逻辑等价) 意义下, 这样的定义是唯一的.

1定义

存在多种方式给出符合条件的定义, 以下是一个例子.

定义 1.1 (可缩纤维等价). 若 $f:A\to B$ 的 (所有) 纤维可缩, 那么 $f$ 是等价.

纤维可缩的意思是存在如下类型的实例:

$$\prod _{b:B}\mathrm{isContr}\left(\sum _{a:A}\mathrm{Id}(fa,b)\right)$$

定义 1.2 (双可逆等价). 若对于 $f:A\to B$, 存在如下数据, 那么 $f$ 是等价:

•	函数 $g_1:B\to A$, 且 ${\prod }_{x:A}\mathrm{Id}(g_1(fx),x)$,

•	函数 $g_2:B\to A$, 且 ${\prod }_{y:B}\mathrm{Id}(f(g_{2}y),y)$.

另可参见 [Univalent Foundations Program 2013] 的 4.8 节.

在有了等价的定义后, 可以借助 $\Sigma$ 类型来定义类型之间的等价:

定义 1.3. 类型 $A,B$ 之间的等价是指如下类型: $${\Sigma }_{f:A\to B}(\mathrm{isEquiv}f)$$该类型记作 $A\simeq B$.

2性质

例 2.1. 每一个类型到自身都有一个由恒同映射给出的等价, 即有$$\mathrm{isEquiv}(\lambda x.x)$$

事实上, 任何两个相等的类型 $A,B$ (即有一个元素 $p:\mathrm{Id}(A,B)$) 都可以用 J 公理证明等价, 即有函数 ${\mathrm{coe}}_{\simeq }:\mathrm{Id}(A,B)\to A\simeq B$.

而泛等公理说的就是上述函数本身也是等价.

3相关概念

•	泛等公理
•	函数外延性

4参考文献

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

术语翻译

等价 • 英文 equivalence

可缩纤维等价 • 英文 contractible fiber equivalence

双可逆等价 • 英文 bi-invertible equivalence