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

这样的问题。而在 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. ——熟悉范畴论的读者应该不会觉得奇怪。

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