同伦类型论

引论

第1章 类型论

第1.1节 类型论和集合论的对比

同伦类型论是数学的一种基础性语言, 即Zermelo-Fraenkel集合论的一种替代品. 然而, 其表现与集合论存在诸多重要的相异之处, 而这需要一些适应. 仔细解释这些不同之处需要我们比本书的其余部分更加形式化. 正如在引论中所言, 我们的目的在于非形式化地写下类型论; 但是对于习惯于集合论的数学家而言, 最初更多的精确性有助于避免一些常见的误解和错误.

我们注意到一个集合论式的基础拥有两个层次: 一阶逻辑的演绎系统, 以及在这个系统内所刻画的某个特定理论 (例如ZFC) 的公理. 因此, 集合论不仅是关于集合的, 更是关于集合 (第二层次的对象) 和命题 (第一层次的对象) 的交互作用的.

与之相对的是, 类型论是其自身的演绎系统: 它不需要在其中刻画任何的超越结构, 例如一阶逻辑. 集合论拥有两个基本概念, 集合和命题, 而类型论只有一个基本概念: 类型. 命题 (可以对其进行证明, 证伪, 假设, 否定等行为的陈述¹) 被等同于特定的类型, 通过表格1所展示的对应关系. 因此, 证明一个定理这样的数学活动被等同于构造一个对象这样的数学活动的一种特殊情况, 这个对象即代表一个命题的类型的一个居民.

¹令人困惑的是, 习惯上 (可以追溯至Euclid) 术语命题 (proposition)和定理 (theorem)近乎同义. 我们将自限于逻辑学家使用术语的方式, 命题是可以进行证明活动(susceptible to proof)的陈述, 而定理 (或者引理或者推论) 是已经被证明的陈述. 因此, $0=1$及其否定$\neg (0=1)$都是命题, 但只有后者才是定理.

这将我们导向了另外一个类型论和集合论的不同之处, 但是为了解释这个不同, 我们必须说点关于一般演绎系统的事情. 非形式化地说, 一个演绎系统是用以推导被称为判断的东西的一集规则. 如果我们将演绎系统当成是形式游戏, 那么判断就是游戏中我们根据游戏规则抵达的位置. 我们也可以将演绎系统想成是某种代数理论, 在这种情况下判断是元素 (就像是一个群的元素) 而演绎规则是运算 (类似于群的乘法). 从逻辑角度来看, 判断可以被认为是外部陈述, 活在元理论之中, 与理论本身的内部陈述相对.

在一阶逻辑 (集合论基于此) 的演绎系统之中, 只存在一种判断: 一个给定的命题拥有一个证明. 也就是说, 每个命题$A$都产生了一个判断$A$拥有一个证明, 而且所有的判断都具有这种形式. 从$A$和$B$可以推出$A\wedge B$这样的一阶逻辑规则实际上是一种证明构造规则, 其是在说给定判断$A$拥有一个证明和$B$拥有一个证明, 我们可以推出$A\wedge B$拥有一个证明. 注意到判断$A$拥有一个证明存在于和命题$A$不同的层次, 其是理论的内部陈述.

类型论的基本判断, 同$A$拥有一个证明类似, 写作$a:A$, 读作项$a$具有类型$A$, 或者更不严谨地说, $a$是$A$的一个元素 (或者, 在同伦类型论中, $a$是$A$的一个点). 当$A$是一个代表命题的类型时, 那么$a$可以被称为$A$的可证明性的见证者, 或者说$A$的真性的证据 (或者甚至说是$A$的一个证明, 但是我们将会尽力避免使用这个令人困惑的术语). 在这种情况下, 判断$a:A$在类型论中是可推导的 (对于某个$a$) 恰当类似的判断$A$拥有一个证明在一阶逻辑中是可推导的 (抛开假定的公理和数学的编码上的差异, 这我们将在整本书中进行讨论).

从另一方面来说, 如果类型$A$以更近于集合而非命题的方式对待 (尽管我们将看到, 区别有时是模糊的), 那么$a:A$就类似于集合论式的陈述$a\in A$. 然而, 这里存在一个本质性的不同, 在于$a:A$是判断而$a\in A$是命题. 具体来说, 当位于类型论的内部进行处理的时候, 我们不能作出例如如果$a:A$, 那么就不会有$b:B$这样的陈述, 也不能证伪判断$a:A$.

一种思考该点的好方法是, 在集合论中, 成员资格 (membership)是一种关系, 可能也可能不在两个预先存在的对象$a$和$A$之间成立, 而在类型论中, 我们不能单独讨论一个元素$a$: 每个元素, 究其本质而言, 都是某个类型的元素, 并且这个类型 (一般而言) 是唯一确定的. 因此, 当我们非形式化地说令$x$是一个自然数时, 在集合论中这是令$x$是某个东西并假定$x\in \mathbb{N}$的缩写, 而在类型论中, 令$x:\mathbb{N}$是一个原子陈述: 我们不能引入一个变量但不刻画其类型.

第一眼看上去, 这似乎是令人不快的限制, 但是或许也可以说这更接近于令$x$是一个自然数在数学上的直觉含义. 在实践中, 似乎每当我们实际上需要$a\in A$是一个命题而非判断时, 总是存在一个包覆$A$的集合$B$, 此时我们知道$a$是$B$的一个元素并且$A$是$B$的一个子集. 这种情况在类型论中也是容易表示的, 取$a$是类型$B$的一个元素, 而$A$是$B$上的一个谓词; 见第3.5节.

类型论和集合论之间的最后一点不同在于对于相等的处理. 数学中为人熟知的相等概念是一种命题: 例如, 我们可以证伪一个相等性或者将一个相等性当作前提. 既然在类型论中, 命题也是类型, 这意味着一个相等性也是一个类型: 对于元素$a,b:A$ (即$a:A$且$b:A$) 而言, 我们有类型$a{=}_{A}b$. (当然, 在同伦类型论中, 这种相等命题的表现可能相当不同寻常: 见第1.12节和第2章, 以及全书的剩余部分.) 当$a{=}_{A}b$存在居民 (is inhabited) 时, 我们称$a$和$b$是(命题)相等的.

然而, 在类型论中, 也有相等判断的需要, 其存在平行于判断$x:A$的层次. 这被称为判断相等或者定义相等, 我们将其记为$a\equiv b:A$或者就简记作$a\equiv b$. 将这种相等想成是根据定义相等比较好. 例如, 如果我们根据等式$f(x)=x^2$定义了一个函数$f:\mathbb{N}\to \mathbb{N}$, 那么根据定义(by definition)表达式$f(3)$等于$3^2$. 在理论内部, 否定或者假定一个定义相等性是没有意义的; 我们不能说如果根据定义$x$等于$y$, 那么根据定义$z$不等于$w$. 两个表达式根据定义相等或者不相等这种判断只和展开定义有关; 具体来说, 这是算法上可判定的 (尽管此算法必然是元理论性质的, 而非位于理论内部).

随着类型论变得愈发复杂, 判断相等也可能变得愈发微妙起来, 但以上的直觉是良好的起点. 从另外一种角度看, 如果我们将演绎系统当作代数理论, 那么判断相等不过就只是这个理论之中的相等, 类似于一个群的元素之间的相等. 唯一可能造成混乱的地方在于演绎系统的内部同样也存在着从内部表现为相等的概念对象, 即类型$a=b$.

我们想要相等的判断概念的原因在于它可以控制其他形式的判断, $a:A$. 例如, 设给定了一个$3^2=9$的证明, 即对于某个$p$推导出了$p:(3^2=9)$, 那么相同的见证者$p$也应该可以算作$f(3)=9$的证明, 因为根据定义$f(3)$就是$3^2$. 表示这种想法的最好方式在于通过一个规则言称, 给定判断$a:A$和$A\equiv B$, 我们可以推导出判断$a:B$.

因此, 对于我们来说, 类型论会是基于以下两种形式的判断的演绎系统:

判断	意义
$a:A$	$a$是具有类型$A$的一个对象
$a\equiv b:A$	$a$和$b$是定义上相等的具有类型$A$的对象

当引入一个定义相等时, 即定义某个东西与另一个相等时, 我们将使用符号$:\equiv$. 因此, 上述对于函数$f$的定义将会写成$f(x):\equiv x^2$.

因为判断不能放在一起以构造更复杂的陈述, 符号$:$和$\equiv$的绑定比其他任何符号都更松散. 因此, 例如$p:x=y$, 应该被理解为$p:(x=y)$, 这是有意义的, 因为$x=y$是一个类型, 但是不能被理解为$(p:x)=y$, 这是无意义的, 因为$p:x$是一个判断, 其不能等于任何东西. 类似地, $A\equiv x=y$只能被理解为$A\equiv (x=y)$, 尽管在这样极端的情况下, 我们应该加上括号以辅助阅读理解. 而且, 之后我们还将采用通常的相等链式记号, 例如写下$a=b=c=d$以表达$a=b$, $b=c$, $c=d$, 因而$a=d$. 并且, 我们也将包括判断相等于这样的链中. 上下文总是能够使得我们的意图清晰.

这里或许也是提及另外一种常见数学记号$f:A\to B$的适合地方了, 其表达了$f$是从$A$到$B$的一个函数的事实, 可以被视为一个类型判断, 因为我们使用$A\to B$作为从$A$到$B$的函数的类型 (这是类型论的标准实践; 见第1.4节).

判断可以依赖于具有形式$x:A$的假设, 其中$x$是一个变量而$A$是一个类型. 例如, 我们可以在$m,n:\mathbb{N}$的假设下构造一个对象$m+n:\mathbb{N}$. 另外一个例子是假设$A$是一个类型, $x,y:A$, 以及$p:x{=}_{A}y$, 那么我们可以构造一个元素$p^{-1}:y{=}_{A}x$. 所有这样的假设构成的合集被称为上下文 (context); 从拓扑的角度来看, 其可以被想成是一个参数空间. 实际上, 从技术上来说上下文必须是假设的有序列表, 因为后面的假设可以依赖于之前的假设: 假设$x:A$只能在假定任意的变量在$A$中出现之后作出. [译注: 这里译者也没看明白原文的含义.]

如果一个假设$x:A$中的类型$A$代表一个命题, 那么这个假设是类型论版本的前提(hypothesis): 我们假定命题$A$成立. 当类型被视为命题时, 我们可以省略证明的名字. 因此, 在上面的第二个例子里, 我们也可以说假定$x{=}_{A}y$, 我们可以证明$y{=}_{A}x$. 然而, 鉴于我们正在做证明相关的数学, 所以我们也将经常回头指明证明为对象. 例如, 在上面的例子里, 我们想要建立这样的想法, 即$p^{-1}$连带着传递性和自反性的证明就表现得如同一个群胚; 见第2章.

注意到在词汇假设(assumption)的含义下, 我们可以假定一个命题相等性 (通过假设一个变量$p:x=y$), 但是我们不能假定一个判断相等性$x\equiv y$, 因为这不是一个可以拥有元素的类型. 然而, 我们可以做些其他的事情, 看起来就像是假定了一个判断相等性: 如果我们有一个牵涉变量$x:A$的类型或者元素, 那么我们可以将$x$替换为任意具体的元素$a:A$以得到一个更加特定的类型或者元素. 有时我们使用语言现在假设$x\equiv a$以指这种替换过程, 即便这并非前文所引入的技术含义上的假设.

根据相同的理由, 我们也不能证明一个判断相等性, 因为这并非我们可以展示见证人的类型. 然而, 我们有时会陈述判断相等性作为定理的一部分, 例如存在$f:A\to B$满足$f(x)\equiv y$. 这应该被视为分别作出了两个判断: 首先我们作出了对于某个元素$f$有$f:A\to B$这一判断, 然后我们作出了$f(x)\equiv y$这一额外判断.

本章的剩余部分, 我们将试图给出类型论的非形式化呈现, 这对于本书的目的而言是足够了; 在附录A中我们给出了一个更加形式化的版本. 除了一些特别显然的规则 (例如判断相等的东西总是可以相互替换这一事实), 类型论的规则可以按照类型形成子(type former)组织. 每个类型形成子都由一种构造类型的方式 (可能利用之前已经构造了的类型), 以及关于该类型的元素的构造和行为的规则构成. 大多数情况下, 这些规则遵循着显而易见的模式, 但是现在我们还不会精确刻画这个想法; 然而读者可以见第1.5节的开头和第5章.

本章所呈现的类型论的一个重要方面在于其仅由规则构成, 没有任何公理. 在对基于判断的演绎系统的描述里, 规则允许我们从一集其他的判断中推导 (conclude) 出一个判断, 而公理是我们最初就拥有的判断. 如果我们将演绎系统想成是形式游戏, 那么规则就是游戏的规则, 而公理是起始位置. 如果我们将演绎系统想成是代数理论, 那么规则是理论的运算而公理是对于理论的某个特定自由模型而言的生成元.

在集合论中, 仅有的规则就是一阶逻辑的规则 (例如允许我们从$A$有一个证明和$B$有一个证明推导出$A\wedge B$有一个证明的规则): 关于集合的行为的所有信息都被包含在公理之中了. 与之相对的是, 在类型论中, 通常是规则涵盖了所有的信息, 而公理是没有必要的. 例如, 在第1.5节中我们将看到存在一条规则允许我们从$a:A$和$b:B$推导出判断$(a,b):A\times B$, 而在集合论中类似的陈述将会是配对公理(的一个实例).

只使用规则刻画类型论的优点在于规则是过程性的. 具体来说, 这种性质使得类型论的良好计算性质成为可能 (但并不自动保证), 例如canonicity. 然而, 尽管这种风格对于传统类型论有效, 我们还不全然理解以这种方式刻画对于同伦类型论而言必要的一切. 具体地说, 在第2.9节和第2.10节以及第6章中, 我们将引入额外的公理来增强本章所呈现的类型论规则, 特别是泛等公理(univalence axiom). 然而, 本章我们将自限于基于规则的传统类型论.

第1.2节 函数类型

给定类型$A$和$B$, 我们可以构造以$A$为定义域而$B$为陪域的函数的类型$A\to B$. 有时我们也称函数为映射. 和集合论不同的是, 函数并不被定义为函数关系; 反而它们是类型论中的原始概念. 我们通过描述可以对于函数做些什么, 如何构造函数, 以及函数所导出的相等性来解释函数类型.

给定一个函数$f:A\to B$和定义域的一个元素$a:A$, 我们可以应用函数以得到陪域$B$的一个元素, 记作$f(a)$, 称为$f$在$a$处的值. 在类型论中省略括号是普遍的, 例如可以将$f(a)$简记为$fa$, 有时我们也将这么做.

但是我们该如何构造$A\to B$的元素呢? 存在两种等价的方式: 要么通过直接的定义, 要么使用$\lambda$抽象. 通过定义引入函数意味着我们在定义函数时赋予了其名字, 比如说$f$, 我们可以说我们通过等式$$f(x):\equiv \mathrm{\Phi }$$定义了一个函数$f:A\to B$, 其中$x$是一个变量而$\mathrm{\Phi }$是一个可以使用$x$的表达式. 为了使得这个定义具有意义, 我们需要验证假定$x:A$时可以推出$\mathrm{\Phi }:B$. [译注: 在某种意义上而言, 这里的假定不是假定.]

现在我们可以通过替换$\mathrm{\Phi }$里的变量$x$为$a$来计算$f(a)$. 作为一个例子, 考虑由$f(x):\equiv x+x$定义的函数$f:\mathbb{N}\to \mathbb{N}$. (我们将于第1.9节定义$\mathbb{N}$和$+$.) 那么, $f(2)$判断相等于$2+2$.

如果我们不希望为函数引入名字, 我们可以使用$\lambda$抽象. 给定一个类型$B$的表达式$\mathrm{\Phi }$, 其可以和上面一样使用$x:A$, 我们记$\lambda (x:A).\mathrm{\Phi }$以指和之前的表达式所定义的相同的函数. 因此, 我们有$$(\lambda (x:A).\mathrm{\Phi }):A\to B\text{.}$$对于前一节的例子, 我们有类型判断$$(\lambda (x:\mathbb{N}).x+x):\mathbb{N}\to \mathbb{N}\text{.}$$作为另外一个例子, 对于任意的类型$A$和$B$以及任意的元素$y:B$, 我们有一个常函数$(\lambda (x:A).y):A\to B$.

我们一般会省略$\lambda$抽象里变量$x$的类型而记$\lambda x.\mathrm{\Phi }$, 因为定型判断$x:A$可从函数$\lambda x.\mathrm{\Phi }$具有类型$A\to B$这一判断推出. 根据惯例, 变量绑定$\lambda x.$的作用域是表达式的整个剩余部分, 除非被括号隔断. 因此, $\lambda x.x+x$应该被理解为$\lambda x.(x+x)$而不是$(\lambda x.x)+x$, 当然后者不论如何都是病态类型 (ill-typed) 的.

另一种等价的记号是$$(x\mapsto \mathrm{\Phi }):A\to B\text{.}$$有时我们也可以在表达式$\mathrm{\Phi }$中用空白$-$代替变量以指称隐式的$\lambda$抽象. 例如, $g(x,-)$是另一种书写$\lambda y.g(x,y)$的方式.

现在$\lambda$抽象是函数, 于是我们可以将其应用于参数$a:A$. 然后我们会有以下计算规则², 其是定义相等性:$$(\lambda x.\mathrm{\Phi })(a)\equiv {\mathrm{\Phi }}^{\prime }$$其中${\mathrm{\Phi }}^{\prime }$是将所有$x$的出现替换为$a$了的$\mathrm{\Phi }$. [译注: 其实是所有$x$的自由出现, 而且需要避免意外的变量捕获.] 继续上面的例子, 我们有$$(\lambda x.x+x)(2)\equiv 2+2\text{.}$$注意到由任意的函数$f:A\to B$, 我们可以构造一个$\lambda$抽象$\lambda x.f(x)$. 因为根据定义这是将$f$应用于其参数的函数, 我们将其视为定义相等于$f$³:$$f\equiv (\lambda x.f(x))\text{.}$$这种相等性是函数类型的唯一性原则, 因为$f$由其值唯一确定. [译注: 当然是在所有可能的元素上的值, 集合论学家会认为这是外延公理的推论.]

²这种相等性的运用经常被称为$\beta$变换或者$\beta$规约.

³这种相等性的运用经常被称为$\eta$变换或者$\eta$规约.

通过带有显式参数的定义引入的函数也可以被规约为使用$\lambda$抽象的简单定义: 例如, 我们可以将通过$$f(x):\equiv \mathrm{\Phi }$$定义的函数$f:A\to B$读作$$f:\equiv \lambda x.\mathrm{\Phi }\text{.}$$

当进行牵涉变量的计算时, 我们必须在替换变量以同样牵涉变量的表达式时小心谨慎, 因为我们想要保持表达式的绑定结构. 我们所说的绑定结构指的是由绑定子 (例如$\lambda ,\mathrm{\Pi },\mathrm{\Sigma }$, 很快我们就要遇到) 生成的在变量引入处与变量使用处之间的无形连接. 作为一个例子, 考虑由$$f(x):\equiv \lambda y.x+y$$定义的函数$f:\mathbb{N}\to (\mathbb{N}\to \mathbb{N})$. 现在如果我们已经在某处假定了$y:\mathbb{N}$, 那么$f(y)$是什么呢? 只是朴素地 (naively) 将表达式$\lambda y.x+y$中的所有$x$替换为$y$是错误的, 因为这意味着$y$会被捕获. 在替换之前, 被替换进去的$y$指的是我们的假定, 但是现在它指的是$\lambda$抽象的参数. 因此, 朴素的替换将会破坏绑定结构, 允许我们执行语义上unsound的计算.

但是这个例子中的$f(y)$应该是什么呢? 我们注意到绑定 (或者哑) 变量, 例如表达式$\lambda y.x+y$中的$y$, 只具有局部的意义, 可以被一致地替换为其他变量, 仍然保持绑定结构. 诚然, $\lambda y.x+y$被声明为判断相等⁴于$\lambda z.x+z$. 然后, 我们知道$f(y)$判断相等于$\lambda z.y+z$. (不止是$z$, 任意不同于$y$的变量都可以使用, 产生相等的结果.)

⁴这种相等性的运用经常被称为$\alpha$变换.

当然, 这些对于数学家而言都应该是熟悉的: 如果$f(x):\equiv {\int }_1^2\frac{1}{x-t}dt$, 那么$f(t)$不是${\int }_1^2\frac{1}{t-t}dt$而是${\int }_1^2\frac{1}{t-s}ds$, 这与之前的现象本质上是相同的. $\lambda$抽象绑定哑变量的方式与积分完全一致.

我们已经看到该如何定义单变量的函数了. 定义多变量函数的一种方式是使用笛卡尔积, 笛卡尔积将在之后引入: 参数的类型为$A$和$B$而结果的类型为$C$的函数将被赋予类型$A\times B\to C$. 然而, 还存在另外一种避免使用积类型的选择, 其被称为currying (以数学家Haskell Curry的名字命名).

currying的想法是表示具有两个输入$a:A$和$b:B$的函数以一个函数, 其接受一个输入$a:A$, 然后返回另一个函数, 其将接受第二个输入$b:B$并返回结果. 也就是说, 我们将两个变量的函数想成是属于一个迭代的函数类型, $f:A\to (B\to C)$. 我们也可以省略括号, 将其写成$f:A\to B\to C$, 默认约定向右结合. 那么, 给定$a:A$和$b:B$, 我们可以应用$f$于$a$, 然后应用结果于$b$, 得到$f(a)(b):C$. 为了避免括号大量增殖, 我们允许我们自己将$f(a)(b)$写成$f(a,b)$, 甚至其实这里并没有积的参与. 当整个省略函数参数周围的括号时, 我们记$fab$或者$(fa)b$, 默认约定向左结合, 这就使得$f$以正确的顺序应用于其参数.

我们对于显式参数定义的记号也可以扩展到此类情况: 我们可以通过等式$$f(x,y):\equiv \mathrm{\Phi }$$以定义一个命名函数$f:A\to B\to C$, 其中假定$x:A$和$y:B$时有$\mathrm{\Phi }:C$. 使用$\lambda$抽象, 这对应于$$f:\equiv \lambda x.\lambda y.\mathrm{\Phi }$$其也可以写作$$f:\equiv x\mapsto y\mapsto \mathrm{\Phi }$$我们也可以隐式地通过多个空白以作出多个变量的抽象, 例如$g(-,-)$的意思是$\lambda x.\lambda y.g(x,y)$. currying三个或者更多参数的函数是对于我们之前所描述的方法的直截了当的扩展.

第1.3节 宇宙和族

到目前为止, 我们只是在非形式化地使用表达式$A$是一个类型. 现在我们要将其变得更加精确, 通过引入宇宙 (universe). 一个宇宙是一个其元素是类型的类型. 就和在朴素集合论中一样, 或许我们希望拥有一个所有类型的宇宙${\mathcal{U}}_{\infty }$, 其包含自身, 即${\mathcal{U}}_{\infty }:{\mathcal{U}}_{\infty }$. 然而, 就和在集合论中一样, 这是unsound的, 即我们可以从中推导出每个类型, 包括表示命题False的空类型 (见第1.7节), 都拥有居民. 例如, 通过将集合表示为树, 我们可以直接编码Russell悖论 [Coq92a].

为了避免悖论, 我们引入一个宇宙的层次结构$${\mathcal{U}}_0:{\mathcal{U}}_1:{\mathcal{U}}_2:\cdots$$其中每个宇宙${\mathcal{U}}_i$都是下一个宇宙${\mathcal{U}}_{i+1}$的元素. 而且, 我们假定我们的宇宙是累积性的, 即第$i$个宇宙的所有元素也都是第$i+1$个宇宙的元素, 例如若$A:{\mathcal{U}}_i$则也有$A:{\mathcal{U}}_{i+1}$. 这是方便的, 但也会导致元素不再具有唯一的类型这一令人不太愉快的后果, 在其他方面也会有点tricky, 但是在这里还不至于让我们烦心; 见本章末的注记.

当我们说$A$是一个类型时, 我们的意思是其居于某个宇宙${\mathcal{U}}_i$之中. 我们通常想要避免显式提及层级$i$, 并假定层级可以按照一致的方式被赋予; 因此, 我们或许可以记$A:\mathcal{U}$而省略层级. 以这种方式, 我们甚至可以写下$\mathcal{U}:\mathcal{U}$, 其应该读作${\mathcal{U}}_i:{\mathcal{U}}_{i+1}$, 它有意地将层级留作隐式. 这种写下宇宙的风格常被称为典型的歧义 (typical ambiguity). 它很方便, 但是也有点危险, 因为其允许我们写下表面上看起来合理的证明, 但是实际上却重演了自指的悖论. 如果对于某个论证的正确性保有任何的疑问, 那么验证这个证明的方法在于尝试为其中出现的每个宇宙一致地赋予层级. 当假定了某个宇宙$\mathcal{U}$时, 我们可以称属于$\mathcal{U}$的类型为小类型 (small types).

为了模拟在给定类型$A$上变动的一个类型合集, 我们使用函数$B:A\to \mathcal{U}$, 其陪域是一个宇宙. 这些函数被称为类型族 (或者有时也被称为依赖类型); 它们对应于集合论中使用的集合族.

类型族的一个例子是有限集合的族$\mathsf{Fin}:\mathbb{N}\to \mathcal{U}$, 其中$\mathsf{Fin}(n)$是一个恰具有$n$个元素的类型. (现在我们还不能定义族$\mathsf{Fin}$, 因为我们还没有引入定义域$\mathbb{N}$, 但是很快就可以了; 见练习1.9.) 我们可以将$\mathsf{Fin}(n)$的元素记为$0_n,1_n,\dots ,{(n-1)}_n$, 这里的下标是为了强调在$n$不同于$m$时, $\mathsf{Fin}(n)$和$\mathsf{Fin}(m)$的元素是不同的, 并且它们也都不同于一般的自然数 (我们将在第1.9节引入).

一种更平凡(但是也非常重要)的类型族的例子是在某个类型$B:\mathcal{U}$处的常类型族, 其当然是常函数$(\lambda (x:A).B):A\to \mathcal{U}$.

作为一个non-example, 在我们的版本的类型论中, 并没有类型族$\lambda (i:\mathbb{N}).{\mathcal{U}}_i$. 诚然如此, 并没有足够大的宇宙作为其陪域. 而且, 甚至我们也不会将宇宙${\mathcal{U}}_i$的下标$i$和类型论的自然数$\mathbb{N}$等同起来 (后者在第1.9节引入).

第1.4节 依赖函数类型 ($\mathrm{\Pi }$类型)

在类型论中, 我们经常使用一种更加一般的函数类型的版本, 其可以称为$\mathrm{\Pi }$类型或者依赖函数类型. 我们使用名字$\mathrm{\Pi }$类型的原因在于这种类型也可以被视为给定类型上的笛卡尔积.

给定类型$A:\mathcal{U}$和族$B:A\to \mathcal{U}$, 我们可以构造依赖函数的类型$\prod _{(x:A)}B(x):\mathcal{U}$. 这种类型的记号可以有诸多变体, 例如$$\prod _{(x:A)}B(x)\prod _{(x:A)}B(x)\prod (x:A),B(x)\text{.}$$如果$B$是一个常族, 那么依赖积类型就变成了通常的函数类型:$$\prod _{(x:A)}B\equiv (A\to B)\text{.}$$的确, 所有$\mathrm{\Pi }$类型的构造其实是通常函数类型上的相应构造的一种推广.

我们可以通过隐式定义来引入依赖函数: 为了定义$f:\prod _{(x:A)}B(x)$, 其中$f$是要被定义的函数的名字,

第1.5节 积类型

第1.6节 依赖序对类型 ($\mathrm{\Sigma }$类型)

第1.7节 余积类型

第1.8节 布尔的类型

第1.9节 自然数

第1.10节 模式匹配和递归

第1.11节 命题作为类型

第1.12节 相等类型

注记

练习

第2章 同伦类型论

第2.1节 类型是高阶群胚

第2.2节 函数是函子

第2.3节 类型族是纤维

第2.4节 同伦和等价

第3章 集合和逻辑

第4章 等价

第5章 归纳

第6章 高阶归纳类型

第7章 同伦$n$类型