同伦类型论

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

同伦类型论可以视为公理化同伦论, 它把同伦论中的一些构造抽象出来作为公理, 并仅使用这些公理进行推导, 从而更自然地处理同伦论, 特别是高阶范畴论中的某些概念.

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

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

1想法

类型论视角

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

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

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

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

同伦论视角

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

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

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

2历史

(...) [Univalent Foundations Program 2013]

3类型论及性质

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

泛等公理

主条目: 泛等公理

泛等公理表明, 宇宙中的相等类型与相应类型间的所有等价构成的类型相等价. 也就是说, 对类型 $A,B$, 有$$\mathrm{Id}(A,B)\simeq (A\simeq B),$$其中 $\mathrm{Id}$ 是宇宙 $\mathcal{U}$ 中的相等类型, 而等式右边可仅由 $A,B$ 而不借助 $\mathcal{U}$ 定义. 换言之, 这一公理要求宇宙具有好的性质, 以使得其中的相等类型是我们所希望的.

降级公理

主条目: 降级公理

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

高阶归纳类型的例子

主条目: 高阶归纳类型

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

对于一个类型 $A$, 构造其截断类型 $|A|$ 的元素的方式是给出 $A$ 的一个元素. 换言之, 有函数 $A\to |A|$, 记作 $\Vert a\Vert$. 与此同时, 给定 $x,y:|A|$, 都可构造 ${\mathrm{Id}}_{|A|}(x,y)$ 的元素 $\mathrm{trunc}(x,y)$.

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

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

4同伦论性质

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

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

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

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

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

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

以上是一般类型上的同伦结构, 而类型上的操作则给出了更具体的构造带有同伦结构的空间的方法. 最简单的构造是无交并 $A\uplus B$, 它对应空间的无交并. 类型的积 $A\times B$ 即对应空间的积. 它正确模拟了拓扑学中乘积空间, 例如拓扑学中积空间的道路空间同伦等价于道路空间的积. 这在同伦类型论中也可以证明:$${\mathrm{Id}}_{A\times B}((a_1,b_1),(a_2,b_2))\cong {\mathrm{Id}}_A(a_1,a_2)\times {\mathrm{Id}}_B(b_1,b_2).$$

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

高阶归纳类型可以想象为 CW 复形, 它的定义就是在类比 “把不同维数的胞腔粘成一个空间” 的过程. 一个高阶归纳类型的例子是圆 $S^1$. 它有构造函数 $\mathrm{base}:S^1$ 与 $\mathrm{loop}:{\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})$, 相应的几何意义即是 $S^1$ 的 $0$ 维和 $1$ 维胞腔. $S^1$ 有许多代数拓扑中熟悉的性质: 如可以定义并求出其基本群 ${\pi }_1(S^1)=\mathbb{Z}$, 可参见编码–解码法或者 [Univalent Foundations Program 2013, §8.1]. 高维的 CW 复形 (如球面) 也可以类似地定义. 还有不少同伦论中的构造也可以在同伦类型论中通过高阶归纳类型定义: 可以定义纬悬 $\Sigma A$, 并且证明$$(\Sigma A\to B)\cong (A\to \Omega B),$$且圆的纬悬等价于球面.

同伦类型论中计算非常依赖泛等公理. 可以利用传统同伦论的方法计算, 不过它还有一套独特的方法, 称为编码-解码法. 上文所说 ${\pi }_1({\mathbb{S}}^1)=\mathbb{Z}$ 是一个例子. 更非平凡的例子是计算 ${\pi }_4({\mathbb{S}}^3)$, 参见 Brunerie 数.

5范畴语义

同伦类型论可在任何 $(\infty ,1)$-意象中实现. 也就是说, 给定 $(\infty ,1)$-意象 $\mathcal{C}$, 将其对象视为类型, 则同伦类型论中的各种操作均可对应于该 $(\infty ,1)$-意象中的构造, 得到的系统满足同伦类型论的所有公理. 简言之, 任何 $(\infty ,1)$-意象都能作为同伦类型论的一个模型. 这称为同伦类型论的范畴语义. 见 [Shulman 2019]、[Riehl 2024].

6实现

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

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

7参考文献

•	The Univalent Foundations Program (2013). “Homotopy type theory: Univalent foundations of mathematics”.

•	Alexandre Grothendieck (1997). “Esquisse d’un Programme”. 出自 Geometric Galois Actions, vol. 1. London Mathematical Society Lecture Note Series. Cambridge University Press. 7–48. (doi)

关于 $(\infty ,1)$-意象中的范畴语义:

•	Michael Shulman (2019). “All $(\infty ,1)$-toposes have strict univalent universes”. arXiv: 1904.07004.

•	Emily Riehl (2024). “On the $\infty$-topos semantics of homotopy type theory”. Bull. Lond. Math. Soc. 56 (2), 461–517. arXiv: 2212.06937. (doi)

术语翻译

同伦类型论 • 英文 homotopy type theory (HoTT) • 德文 Homotopietypentheorie • 法文 théorie homotopique des types • 拉丁文 theoria homotopica typorum • 古希腊文 ὁμοτοπικὴ θεωρία τύπων