等价 (类型论)

等价在类型论中指一些满足特定条件的函数, 该性质一般记作 , 命题宇宙保证一个函数的等价证明唯一, 具体定义方式很多, 下面会列举一些.

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

定义 0.1. 函数 在如下情况下是拟等价:

存在 , 使得能够给出 .

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

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

1定义

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

定义 1.1 (可缩纤维等价). 对于 , 是说 的 (所有) 纤维可缩.

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

定义 1.2 (双可逆等价). 对于 , 是指如下数据:

函数 , 且有 的实例,

函数 , 且有 的实例.

定义 1.3 (半伴随等价). 对于 , 是指如下数据:

函数 , 且有

,

同伦 .

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

定义 1.4. 类型 之间的等价是指如下类型: 该类型记作 .

2性质

例 2.1. 每一个类型到自身都有一个由恒同映射给出的等价, 即有

事实上, 任何两个相等的类型 (即有一个元素 ) 都可以用 J 公理证明等价, 即有函数 .

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

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