数学里的构造主义与直觉主义（二）

这样的问题。而在 type theory（intensional type theory, 下同）中，没有办法 “给出” 一个不 “属于” 任何类型的α，再去讨论它和别的类型有没有从属关系，只能一次性地给出判定α：A——注意这里的用词，α：A是一个判定 (judgement)，而不是一个取值有可能真也有可能假的命题，一个判定从摆上纸面的那一刻就自动成立。在集合论中，如果α ∈ A，B是一个满足A ⊂ B的集合，则我们也有α ∈ B. 类似的话在 type theory 中毫无意义。——实际上，type theory 的这种讨论方式，反倒更接近现代数学实践，因为没有人会真的拿两个不相干的东西α，A再问 “α ∈ A是否成立”，而通常是 “设X是拓扑空间，x ∈ X是X中的一个点”，从这个角度上说，这种做法更接近于给出判定X：Top，x：X.

更有趣的一点是，类型论的法则自动地包含了基本的逻辑！一个命题，在类型论中可以写成一个类型P，其证明则是构造那个类型中的一项 (term) x：P. 命题P ⇒ Q则变成了一个新的 type P → Q，其 “证明” 则是在类型论的意义下构造P到Q的一个函数。对照之下，数理逻辑独立于集合论而存在。

集合论中最基本的 “命题”，α ∈ A 在 type theory 中已经不能讨论。另一类命题，即对于x，y∈A是否有x＝y，则在 type theory 中有深远的推广。前面说了，任意一个命题，都有自己的类型，x＝y 这样的，也不例外——它对应的类型，叫 identity type, 记做x＝ᴀ y. 相比之下，集合论中的命题，无非是两个元素的一个比较，相等，则x，y只是同一对象的两个符号而已，可以互相置换（substitution, 等量代换是中学数学中最基本的操作）；不相等，则他们之间在集合论的意义下没有任何联系。x＝ᴀ y 是个 type 这件事情，不仅仅是个记号，意味着 type theory 的任何构造，都可以对它进行。

§4. 尾声：从 Extensionality 到 Univalence

两个集合什么时候相等呢？在 ZFC 集合论中，这是由一条叫做外延性 (extensionality) 的公理保证的：∀A，B(∀x，x ∈ A ⇔ x ∈ B) ⇒ (A＝B). 也就是说，如果两个集合包含的元素一模一样，我们就说两个集合相等。

这个公理完全不能用在 type theory 中——根本没有∀x这个说法，要给出x，必须以x：A这样的方式，这时候x：B就成了彻底的伪命题，没法讨论。

但是，在类型论中讨论两个类型的 equality, 还是有一定意义：实际上，任意两个 type A，B 都是一个更大的 type, 即 universe ∪ 中的项，所以给出两个类型其实是给定了A，B：∪， 我们当然可以定义 identity type A＝ᴜ B，但是，怎么描述这个类型呢？

Voevodsky 在 2009 年给出了一个诱人的答案，即 univalence axiom.

从A＝ᴜ B这个类型到(A → B)这个类型，有个 map. 对于任意一个p：A＝ᴜ B，我们都能得到一个p⁎：A → B，这个p⁎有个特殊的性质，它（together with other data）实际上构成了A到B的一个 equivalence. ——熟悉范畴论的读者应该不会觉得奇怪。

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

4. 让计算机理解集合论并没有文中说的那么困难，参见 Mizar system —— A proof assistant based on first-order logic, in a natural deduction style, and Tarski–Grothendieck set theory. (Tarski-Grothendieck set theory 是 ZFC 的一个 non-conservertive extension, 添加了 Tarski 公理：对任意一个集合x存在一个 Grothendieck universeU使得x∈U.)

5. 可能有读者会问 type theory 里这套 Programming 和 Mathematics 的对应和所谓的 Curry-Howard Isomorphism 有什么区别和联系, 实际上上述对应相当于把 Curry-Howard isomorphism 扩展到了 dependent type theory. 相当于 Curry–Howard isomorphism 加上了谓词逻辑的的强化版。

6. 集合论的 extensionality 公理的推论之一是，对于两个集合之间的函数f，g：X → Y，f＝g ⇔ ∀x ∈ X，f(x)＝g(x)：因为作为X × Y的子集，f，g的图像Γf，Γg在函数值完全相当的时候完全重合，所以作为集合相等。

7. 用不严谨的话讲，加入了 univalence axiom 的 type theory, 叫 homotopy type theory. 我故意在正文里避开了这个词。

8. Jacob Lurie 以集合论为基础来定义(∞，1)-groupoid，做了很重要的工作，但他的工作与 homotopy type theory 无关。窃认为 Jacob Lurie 工作的困难程度可以反过来说明 homotopy type theory 的重要性。

§6. 参考

1. 关于构造主义的一个比较耐读的参考 (40 pp.): Constructive Mathematics in Theory and Programming Practice, Douglas BRIDGES and Steve REEVES

2. Constructive Mathematics (Stanford Encyclopedia of Philosophy)

3. 有一定数学背景，且对 Homotopy type theory 有兴趣的读者很有必要看看这三个 slides：

• cse.chalmers.se/~coquan...

• cse.chalmers.se/~coquan...

• cse.chalmers.se/~coquan...

（题图：Wikipedia File：Logic.svg）

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。