数学里的构造主义与直觉主义（二） (3-2)

Equivalence 的定义在这里恕不展开了，只能说任给A，B：∪，可以定义 type of equivalences A ≃ B. 用不严格的符号说，前述的 map p↦p⁎实际上给出了 identity type 到 type of equivalences 的一个 map. Voevodsky 引入的 univalence 公理说，这个 map 是一个 equivalence.

引入 univalence 公理相当于把终极的外延性 (extensionality) 引入了 type theory。说到底，extensionality 是关于什么时候能判定两个结构在某种意义下 “相同” 的公理，对于集合来说，这是很简单的。但是在通常的数学中，有些熟悉例子，两个很一致的东西（即关键的性质可以像前面说的那样 “搬来搬去” (transport)），不能说他们相等。比如任意两个n维线性空间，我们只能说他们 “同构” 而不能说他们相等，因为有太多种方式把他们等同起来（选取基以后任意的n × n可逆矩阵都给出同构）；对于两个范畴，甚至只能说他们 “等价” 而不能说他们同构（因为在集合层面并不是一一对应）。这些褶皱，都能用 univalence axiom 一一抚平。

更体现 univalence axiom 威力的地方在于，有了 univalence axiom, 能很好地对任意的自然数n定义n-groupoid（n-type）——定义 n-groupoid 或者(∞，1)-groupoid其实是很有意义的，也很困难（比如通常的 algebraic stacks 也就是n＝2的情形而已）。Grothendieck 在 Esquisse d'un Programme ( Sketch of a Programme) 的第七节 Pursuing Stacks 描绘了用 homotopic algebra 来定义 n-stack的可能性。Univalence axiom 可以看做对 Grothendieck 描绘的蓝图的一个回应。

§5. 注释

1. 用“瑞典人” 来描述 Martin-Löf 的主要原因是他太神，没法用 “数学家” 这样的词简单概括，引用 Wikipedia 第一句做个注解：Per Erik Rutger Martin-Löf (born May 8, 1942) is a Swedish logician, philosopher, and mathematical statistician.（逻辑学家，哲学家和数理统计学家）

2. Type theory 其实最早是罗素提出来的。这里介绍的是 Martin-Löf type theory. Martin-Löf 发展的 type theory 其实有好几个版本, 参见 Intuitionistic type theory#Martin-Löf_Type_Theories. 我认为 identity type 是最大的创新之一。

3. 计算机证明黎曼猜想和自然数的定义那个故事是编的，但是很有必要定义一种数学基础使得所有的命题都可以 “搬来搬去”，则是一种共识。“It should be impossible to formulate a statement which is not invariant with respect to equivalences.” ——T. Coquand

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。