等价 (类型论)

等价在类型论中指一些满足特定条件的函数, 该性质一般记作 $\mathrm{isEquiv}:(A\to B)\to \mathrm{Prop}$, 命题宇宙保证一个函数的等价证明唯一, 具体定义方式很多, 下面会列举一些.

这个定义需要满足如下性质: $\mathrm{isEquiv}f$ 在逻辑上等价于 (即两者能够互相推导) 拟等价, 定义如下:

定义 0.1. 函数 $f:A\to B$ 在如下情况下是拟等价:

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

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

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

1定义

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

定义 1.1 (可缩纤维等价). 对于 $f:A\to B$, $\mathrm{isEquiv}(f)$ 是说 $f$ 的 (所有) 纤维可缩.

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

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

定义 1.2 (双可逆等价). 对于 $f:A\to B$, $\mathrm{isEquiv}(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)$ 的实例.

定义 1.3 (半伴随等价). 对于 $f:A\to B$, $\mathrm{isEquiv}(f)$ 是指如下数据:

•	函数 $g:B\to A$, 且有

•	$\eta :{\prod }_{x:A}\mathrm{Id}(g(fx),x)$ 和 $\epsilon :{\prod }_{y:B}\mathrm{Id}(f(gy),y)$,

•	同伦 $\tau :{\prod }_{x:A}{\mathrm{Id}}_{\mathrm{Id}(f(g(fx)),fx)}({\mathrm{ap}}_f(\eta x),\epsilon (fx))$.

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

定义 1.4. 类型 $A,B$ 之间的等价是指如下类型: $$\sum _{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

拟等价 • 英文 quasi-equivalence

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

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

半伴随等价 • 英文 half-adjoint equivalence