同伦类型论 是一种 类型论 , 建立于 同伦论 和 高阶范畴论 的概念之上. 它将类型视为 ∞ -群胚 (或 拓扑空间 ), 该 ∞ -群胚的 对象 (或拓扑空间的点) 是类型的元素, 其间的 1 -态射 (或拓扑空间里的道路) 的空间可以解释为元素之间相等关系的所有证明构成的空间, 而 2 -态射 (或道路之间的同伦) 是这些证明之间的等价关系, 如此等等.

同伦类型论可以视为 公理化 同伦论 , 它把代数拓扑中的一些构造抽象出来作为公理, 并仅使用这些公理进行推导.

同伦类型论也是 数学的基础 的观点之一. 这种观点认为, 类型是比 集合 更基础的对象, 故同伦类型论可以取代 集合论 而成为数学的基础. 关于这种观点, 可以参考 类型论 .

同伦类型论也可以应用于机器辅助证明. 相较于基于集合论或传统类型论的方法, 它能更简洁地形式化数学证明.

1 动机

类型论视角

在 类型论 中, 通常用 Curry–Howard 对应 将命题与其证明的关系编码为类型与其元素的关系. 譬如两个命题 A 与 B 的 合取 A ∧ B 可以编码为两个类型的 积 A × B . 在同伦类型论中, 对此有更精细的刻画. 同伦类型论中, 命题对应的是所有元素都相等的类型. 例如, 真命题是 可缩 的类型, 而假命题是空类型. 这符合数学直觉, 即一个命题得到证明后便成立, 而不会 “有多种不同的成立方式”. 这个定义消除了很多类型论中有悖于一般数学或者 直觉主义 数学的结论, 如 Curry–Howard 对应下的 选择公理 是重言式, 等等.

但考察各种类型是否是命题的时候, 会遇到一个困难: 相等类型本身不一定是命题. 在 Martin-Löf 类型论 中, 给定一个类型 A 与其两个元素 a , b , 可以定义 相等类型 Id A ​ ( a , b ) , 简写为 Id ( a , b ) . 要构造这个类型的元素, 只能通过 自反 性质: refl a ​ : Id ( a , a ) . 另一方面, 要利用一个已经构造好的元素, 需要通过 J 公理 : 若有一族类型 C ( x , y , p ) , 取决于三个变量 x : A , y : A , p : Id ( x , y ) , 为了构造 c ( x , y , p ) : C ( x , y , p ) , 只需要考虑 x = y 的情况, 即构造 c 0 ​ ( x ) : C ( x , x , refl x ​ ) . 此时 c ( x , y , p ) = J ( c 0 ​ , x , y , p ) . 给定 J 公理, 我们无法证明 Id ( a , b ) 是命题. 这是同伦类型论中最基本的结论, 可以通过模型论给出证明. 若一个类型 A 上的相等类型 Id A ​ ( a , b ) 是命题, 那么这个类型的性质表现得正如一般数学中的 集合 . 特别的, 可以证明命题都是集合.

尽管无法证明所有的类型都是集合, 同样无法证明其否定, 更无法给出反例 (注意在没有排中律的情况下这两者一般是不同的). 因此在 Martin-Löf 类型论中并没有相等类型表现得非平凡的具体例子. 同伦类型论中增添了两种新事物, 泛等公理 与 高阶归纳类型 . 前者在回答了一系列数学哲学、本体论相关的问题的同时, 也解决了一些在 Martin-Löf 类型论中如函数与命题的外延性不可证明的问题 (见 函数类型 ) ; 后者为许多数学中常见的构造 (如代数结构的 商 ) 提供了基础.

•	泛等公理 粗略来看, 说的是 “同构的类型相等”. 从拓扑角度来说, 这对应同伦等价, 因此下文将用 “等价” 称之.
•	高阶归纳类型 是 归纳类型 结合了 CW 复形 的升级. 给定一个集合以及其上的等价关系, 其商类型 (可以证明是集合) 是一种高阶归纳类型.

同伦论视角

拓扑学 研究 拓扑空间 的性质, 但存在许多病态的拓扑空间使得许多理应满足的性质实际上并不成立: 不是所有的空间都有 万有覆叠 ; 拓扑空间间的映射空间 Map ( X , Y ) 上定义了并不自然的紧开拓扑, 还未必满足 指数律 , 等等. 使得人们不得不花费精力于在每一种理论中筛去那些不好的空间 (例如只考虑 紧生成 弱 Hausdorff 空间 ), 使主流理论招来了批判 [ Grothendieck 1997 ].

人们正因如此寻求一种 公理化 (或综合) 代数拓扑学, 不再把理论建立于集合论和一般拓扑的框架之上, 而视一些基本构造和它们应满足的性质为公理, 并只从这些公理出发建立整个代数拓扑理论. 例如在同伦类型论中, 空间中两个点之间的道路不再由映射 [ 0 , 1 ] → X 所定义 (此映射的出发域基于实数), 而是一个抽象的类型 “相等类型” 中的元素; 圆周不再是基于实数的 Euclid 空间 的子空间, 而是由一个点和此点到自己的道路构成的类型等等.

不过需要指出现在的同伦类型论发展尚未成熟, 能做的计算暂时远少于主流代数拓扑, 且无法利用 微分拓扑 等相关理论辅助计算.

(还可以写一些抽象同伦论相关...)

2 历史

(...) [ Univalent Foundations Program 2013 ]

3 类型论及性质

本节主要以类型论视角介绍. 下一节介绍在同伦论视角的一些成果.

泛等公理

主条目: 泛等公理

泛等公理的一种常见表述是 等价 (类型论) 和 “类型上的的 相等类型 ” 这两个类型等价: Id ( A , B ) ≃ ( A ≃ B ) 而这里 “等价” 有多种可能的定义, 只要满足一些原则即可 (可以理解为 “命题形式的同构”).

降级公理

主条目: 降级公理

非直谓 命题宇宙 是非常有用的形式化工具, 而降级公理极大地增加了可以被非直谓地使用的类型的数量.

高阶归纳类型的例子

主条目: 高阶归纳类型

最简单的高阶归纳类型是 逻辑截断类型 , 在通常的数学语言中, 即商去一个恒成立的等价关系, 使商类型中所有元素都相等. 它的用途在于确保某个类型是命题, 譬如命题的析取 A ∨ B 在一般的 Curry–Howard 定义下是 无交并类型 , 不一定是命题. 因此在同伦类型论的定义下是其截断 ∣ A + B ∣ .

对于一个类型 A , 构造其截断类型 ∣ A ∣ 的元素的方式是给出 A 的一个元素. 换言之, 有函数 A → ∣ A ∣ , 记作 ∥ a ∥ . 与此同时, 给定 x , y : ∣ A ∣ , 都可构造 Id ∣ A ∣ ​ ( x , y ) 的元素 trunc ( x , y ) .

与一般数学的商集类似, 我们在 “使用” ∣ A ∣ 的元素 (即定义以 ∣ A ∣ 为定义域的函数) 时, 需要给出以 A 为定义域的函数, 然后证明该函数在定义域上是常数.

利用高阶归纳类型还可以构造一些拓扑空间的类比, 详见下节.

4 同伦论性质

参见: 代数拓扑–同伦类型论类比

同伦类型论和 代数拓扑 中 同伦论 (或者更一般的抽象同伦论) 有许多相似的构造. 一方面这为人们提供了同伦类型论中各种构造的直观; 另一方面, 代数拓扑中的构造可以在同伦类型论的框架下以一种 公理化 的方式, 不提及点集拓扑与实数而定义, 这省去了需要筛去病态拓扑空间的麻烦.

首先考虑相等类型 Id ( x , y ) , 它的类比是以 x , y 为两个端点的 道路空间 : refl a ​ 可以看作在某个点不动的平凡道路; 利用 J 公理, 给定一条从 x 到 y 与一条从 y 到 z 的道路, 可以将其拼接形成一条 x 到 z 的道路. 即函数 concat : Id ( x , y ) × Id ( y , z ) → Id ( x , z ) . 与传统的同伦论相同, 将其记作 p ⋅ q . 同样, 我们可以将道路逆转, 记作 p − 1 .

进一步, 由于相等类型也是类型, 因此同样可以考察其上的相等类型: 在拓扑中这即是两条道路之间的同伦. 这样正如 基本 ∞ -群胚 , 任何类型的相等类型具有 ∞ -群胚 结构. 譬如, 可以给出 Id (( p ⋅ q ) ⋅ r , p ⋅ ( q ⋅ r )) , 即在高阶同伦意义下的结合律. 再进一步, 可以得到结合律的五边形恒等式: ( p ⋅ q ) ⋅ ( r ⋅ s ) p ⋅ ( q ⋅ ( r ⋅ s )) (( p ⋅ q ) ⋅ r ) ⋅ s p ⋅ (( q ⋅ r ) ⋅ s ) ( p ⋅ ( q ⋅ r )) ⋅ s

其中, 每个箭头都代表一条道路的道路 (即 Id Id A ​ ( a , b ) ​ ( p , q ) 的一个元素). 而整个五边形上面的两条道路拼接与下面三条道路拼接得到的道路的道路 (2-道路) 之间有一条 3-道路.

特别地, 给定一个类型 A 与其中的某个元素 a , 可以定义 环路空间 Ω A = Id A ​ ( a , a ) , 这个类型的 0 -截断 (对应于取连通分支) 在道路的拼合下构成的群就是基本群.

以上是一般类型上的同伦结构, 而类型上的操作则给出了更具体的构造带有同伦结构的空间的方法. 最简单的构造是无交并 A ⊎ B , 它对应空间的无交并. 类型的积 A × B 即对应空间的积. 它正确模拟了拓扑学中乘积空间, 例如拓扑学中积空间的道路空间同伦等价于道路空间的积. 这在同伦类型论中也可以证明: Id A × B ​ (( a 1 ​ , b 1 ​ ) , ( a 2 ​ , b 2 ​ )) ≅ Id A ​ ( a 1 ​ , a 2 ​ ) × Id B ​ ( b 1 ​ , b 2 ​ ) .

作为一种 依值类型论 , 类型可以包含其他类型的值作为变量. 如 Id N ​ ( m + n , n + m ) 这个类型, 作为命题的解释即 “自然数 m , n 的加法交换”. 它取决于两个自然数变量 m , n : N . 在代数拓扑中, 依值类型 B ( a ) 的类比是纤维化. 基空间 A 即变量 a 的类型. 对于每个具体的 a 0 ​ : A , B ( a 0 ​ ) 即其上的纤维, 全空间在类型论中写作 ∑ x : A ​ B ( x ) . 而纤维化满足的同伦提升性质类比为如下命题 (可以在同伦类型论中证明): 对底空间的道路 p : x = y , 存在映射 p ∗ ​ : B ( x ) → B ( y ) , 并对任意存在一族在全空间中的道路 u = p ∗ ​ ( u ) ( u : B ( x ) ).

高阶归纳类型可以想象为 CW 复形 , 它的定义就是在类比 “把不同维数的胞腔粘成一个空间” 的过程. 一个高阶归纳类型的例子是 圆 S 1 . 它有构造函数 base : S 1 与 loop : Id S 1 ​ ( base , base ) , 相应的几何意义即是 S 1 的 0 维和 1 维胞腔. S 1 有许多 代数拓扑 中熟悉的性质: 如可以定义并求出其 基本群 π 1 ​ ( S 1 ) = Z [ Univalent Foundations Program 2013 , §8.1]. 高维的 CW 复形 (如 球面 ) 也可以类似地定义. 还有不少同伦论中的构造也可以在同伦类型论中通过高阶归纳类型定义: 可以定义 纬悬 Σ A , 并且证明 ( Σ A → B ) ≅ ( A → Ω B ) , 且圆的纬悬等价于球面.

同伦类型论中计算非常依赖泛等公理. 可以利用传统同伦论的方法计算, 不过它还有一套独特的方法, 称为 编码-解码法 . 上文所说 π 1 ​ ( S 1 ) = Z 是一个例子. 更非平凡的例子是计算 π 4 ​ ( S 3 ) , 在 [ Brunerie 2016 ] 中有完整的计算与证明.

5 实现

同伦类型论作为一种类型论, 有多种实现. 各种实现都有着各自的设计目标, 实现的侧重点也有所不同, 不过它们都有一个共通的目标, 就是把类型论实现为编程语言的类型系统, 以达到在计算机中形式化 (可计算的) 数学的目的.

•	Arend 编程语言的类型论, 以尽可能接近原本的同伦类型论而设计, 仅为对 Martin-Löf 类型论 的简单扩展.
•	立方类型论 侧重于模型的构造性, 它是一个具有 典范性 的类型论, 在 Martin-Löf 类型论 的基础上进行了极大量的修改.
•	高阶观测类型论 试图通过在 观测类型论 的基础上扩展以支持同伦类型论, 但目前还处于实验阶段.

6 参考文献

•	The Univalent Foundations Program (2013). “Homotopy type theory: Univalent foundations of mathematics”.
•	Guillaume Brunerie (2016). “On the homotopy groups of spheres in homotopy type theory”. arXiv: 1606.05916 . ( doi ) ( web )
•	Alexandre Grothendieck (1997). “Esquisse d’un Programme”. 7–48( doi ) 类型论 基本概念 类型 • 语境 • 替换操作 • λ 编码 • Curry–Howard 对应 • 模式匹配 一般类型论 简单类型 λ 演算 • 函数类型 、 积类型 、 无交并类型 • 归纳类型 、 逆归纳类型 ( 互拟 ) • 自然数类型 • 纯类型论 、 F 系统 、 U 系统 • 线性类型论 • 子类型 依值类型论 Martin-Löf 类型论 • 宇宙 、 命题宇宙 、 集合 • 相等类型 • W 类型 、 M 类型 • 观测类型论 • 量化类型论 • 构造演算 同伦类型论 圆周 、 区间 、 纬悬 • 逻辑截断类型 、 截断类型 • n -类型 • 高阶归纳类型 • 立方类型论 • 高阶观测类型论 属性 正规性 、 典范性 • 一致性 • 参数性 • 合流性 • 非直谓性 • 类型不变性 语义与模型 范畴语义 、 概括范畴 、 C 系统 、 含族范畴 • 语汇理论 • 偏等关系语义 • 具现 [​ 查看模板 ]