泛等公理

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

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

泛等公理更准确的描述是 “ 是一个等价”.

1定义

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

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

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

该公理本身会额外给出一个 的操作, 但我们已经有 了! 我们可能需要处理泛等公理给出的这个操作和 之间的相等关系, 这会带来额外的麻烦.

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

首先, 这三个公理更加接近泛等公理的准确叙述: 它给出了证明 所需的组件.

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

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

2推论

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

函数外延性

主条目: 函数外延性

定义 2.1. 函数外延性指如下命题: 对于函数 ,

写成等号的话 2.1 会更直观一些:

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

首先, 在函数类型中已经指出 2.1 并不总是成立. 但它的反向函数却总是成立: 如果 , 那么一定有 , 这是因为类型论中, 相等的表达式可以互相代换, 因此 的话可知而后者显然成立.

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

证明. 根据相等类型的性质和泛等公理, 可知 , 因此至此证明已经基本结束, 只需一些比较繁琐的手法将 转换成 的特例后, 用上面的连等即可得到 .

命题的外延性

参见: 命题宇宙

定义 2.3. 如下命题叫做命题外延性: 对于命题 , 有

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

证明. 命题的外延性假设如下函数存在: 要通过泛等公理证明 的话只需证明 即可. 根据命题本身的性质可知对于任意 , 有 命题等价、反之亦然.

结构等价原则

(...)

K 公理

主条目: K 公理

引理 2.5. 为拥有两个互不相等实例的类型, 泛等公理蕴涵如下等价关系:

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

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

证明. 根据 K 公理, 有 , 其中 单位类型. 显然 .

这也可以作为一种 “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日文 一価性公理