泛等公理
泛等公理是同伦类型论的核心思想之一, 是一个类型论公理, 常见的表述大概是 “等价和类型相等” 这两个类型等价, 写作其中 是相等类型, 代表两边存在一个等价. 等价这个概念的定义有多种选择, 只要满足一些原则即可.
实际上, 上述公式并不准确, 因为类型论中的 J 公理本身能给出一个操作:
泛等公理更准确的描述是 “ 是一个等价”.
1定义
泛等公理最常见的用法是将一个等价转化为一个相等, 且证明这个转换本身是等价. 如下公式打包了这些操作:
但直接引入这个公式作为公理有如下缺点:
• | 常见的操作 (如等价到相等的转换) 的使用比起该公理本身更加频繁, 且 |
• | 该公理本身会额外给出一个 的操作, 但我们已经有 了! 我们可能需要处理泛等公理给出的这个操作和 之间的相等关系, 这会带来额外的麻烦. |
因此, 将该公式肢解后去掉多余的部分, 我们有如下三个公理作为该公式的替代品:
首先, 这三个公理更加接近泛等公理的准确叙述: 它给出了证明 所需的组件.
其次, 这三个公理给出了更直观的 “化简” 规则: 若将 操作类比为一种构造规则的话, 那么 就是它的消去规则 (而由于这个函数本身也是由 J 规则实现的, 所以也可以认为 J 规则是它的消去规则), 然后 就是它的计算规则、 是唯一性规则.
配合 J 规则, 我们能通过这三个公理证明上面的公式.
2推论
泛等公理有很多非常深刻的推论.
函数外延性
主条目: 函数外延性
定义 2.1. 函数外延性指如下命题: 对于函数 ,
将 写成等号的话 2.1 会更直观一些:
引理 2.2. 泛等公理蕴涵函数的外延性. 换言之, 同伦类型论中函数的外延性总是成立.
另外, 相等类型有一个重要的性质: 这是因为 这个类型中 这个部分没有任何信息, 它只是把 的存在重复了一遍. 根据这两件事, 可以证明 2.2.
命题的外延性
参见: 命题宇宙
定义 2.3. 如下命题叫做命题外延性: 对于命题 , 有
引理 2.4. 泛等公理蕴涵命题的外延性. 换言之, 同伦类型论中命题的外延性总是成立.
结构等价原则
(...)
K 公理
主条目: K 公理
引理 2.5. 令 为拥有两个互不相等实例的类型, 泛等公理蕴涵如下等价关系:
定理 2.6. 泛等公理提供了 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 • 日文 一価性公理