立方类型论

立方类型论是一种同伦类型论的典范 “实现”. 有如下两种方式看待立方类型论:

•	语义视角: 将依值类型论中的所有对象全部升级为方形集, 这是一种类似单纯集的预层, 但使用方形代替单形.

•	语法视角: 通过重新定义 Martin-Löf 类型论中的相等类型以将同伦类型论中的公理转化为新的相等类型上的定理.

1动机

同伦类型论最经典的模型是基于单纯集的, 也就是说将依值类型解释为单纯集, 然后将泛等公理在单纯集中证明出来. 但是在当时, 这个模型的构造需要假设排中律. 具体来说, 需要假定一个单纯形要么是退化的, 要么不是. 不然有许多必须的性质就无法证明. 如果希望将某个模型使用计算机算法实现成编程语言的话, 就不能使用公理, 不能为了解决同伦类型论的泛等公理而引入选择公理或者排中律. 而使用方形的模型没有这些困难, 由此启发了立方类型论的设计. (后来对相关的构造和证明进行改进, 去除了排中律与选择公理的使用, 并且也有工作提出了单形类型论的概念.)

在类型论中, 方形的表示非常方便: 如果某方形上的值类型都是 $X$ 那么它可以表示为如下函数:

$$\mathbb{I}\to \mathbb{I}\to \cdots \to \mathbb{I}\to X$$

使用逻辑的语言的话, 可以写作

$$x:\mathbb{I},y:\mathbb{I},\cdots ⊢X(x,y,\cdots )$$

将 $x,y$ 这样的变量替换为 $0,1$ 的过程就是退化映射, 而在语境里加入新的变量就是面映射.

2内容

道路类型

立方类型论的基本思想是引入一个类比标准区间拓扑空间的底层构造 $\mathbb{I}$, 用这个类型来定义道路空间的类型, 并且用这个类型代替相等类型. 比如类型 $X$ 上的道路空间就是 $\mathbb{I}\to X$, 而 $x,y:X$ 之间的道路 ${\mathrm{Id}}_X(x,y)$ 就是函数 $p:\mathbb{I}\to X$ 使得 $p(0)=x,p(1)=y$. 这本质上是相等类型变成了某种特殊的函数类型, 因此相等类型可以像函数一样通过 $\lambda$ 符号被构造、被传递参数来应用.

相等类型的构造规则, 也就是自反性可以直接定义为常函数.

用这种方式可以轻易地证明函数外延性.

证明.

证明. 令 $f,g:A\to B$, 定义

$$\begin{array}{rl}\mathrm{funExt}& :({\Pi }_{a:A}\mathrm{Id}(fa,ga))\to \mathrm{Id}(f,g)\\ \mathrm{funExt}& (p)=\lambda i.\lambda x.p(x)(i)\end{array}$$

其中

$$\begin{array}{rl}\lambda i.\lambda x.p(x)(i)& :\mathrm{Id}(f,g)\\ \lambda x.p(x)(i)& :A\to B\\ p(x)& :\mathrm{Id}(fx,gx)\end{array}$$

$\square$

但这样定义的话还需要处理 J 公理, 也就是相等类型的消去规则. 立方类型论引入了转换规则和复合来解决这个问题.

Kan 结构

立方类型论给每个类型的形成规则加入了如下操作:

$$\frac{\Gamma ⊢A:\mathbb{I}\to \mathcal{U}\Gamma ⊢r,r^{\prime }:\mathbb{I}}{{\mathrm{coe}}_A^{r⇝r^{\prime }}:A(r)\to A(r^{\prime })}$$

该操作对于每个类型的形成规则都必须定义, 此处只给出函数类型的例子:

$$\begin{array}{rl}{\mathrm{coe}}_{\lambda i.A\to B}^{r⇝r^{\prime }}& :(A[r/i]\to B[r/i])\to (A[r^{\prime }/i]\to B[r^{\prime }/i])\\ & :=\lambda f.\lambda a.{\mathrm{coe}}_{\lambda i.B}^{r⇝r^{\prime }}(f({\mathrm{coe}}_{\lambda i.A}^{r^{\prime }⇝r}(a)))\end{array}$$

其中

$$\begin{array}{rl}f& :A[r/i]\to B[r/i]\\ a& :A[r^{\prime }/i]\\ {\mathrm{coe}}_{\lambda i.A}^{r^{\prime }⇝r}(a)& :A[r/i]\end{array}$$

除此之外, 若 $r=r^{\prime }$ 那么转换操作直接返回参数. 换言之,

$${\mathrm{coe}}_X^{r⇝r}=\lambda x.x$$

复合

相等类型的 $\mathrm{coe}$ 操作并不能像函数类型那样直接通过类型论现有的规则处理. 考虑如下表达式:

$$\frac{p:\mathrm{Id}(a,b)}{{\mathrm{coe}}_{\lambda i.\mathrm{Id}(pi,c)}^{0⇝r}:\mathrm{Id}(p0,c)\to \mathrm{Id}(pr,c)}$$

根据 $p$ 的类型化简得到

$${\mathrm{coe}}_{\lambda i.\mathrm{Id}(pi,c)}^{0⇝r}:\mathrm{Id}(a,c)\to \mathrm{Id}(pr,c)$$

类型 $\mathrm{Id}(pr,c)$ 虽说看起来像是一条 $pr$ 到 $c$ 的道路, 但如果把 $pr$ 看作以 $r$ 为方向的道路的话, 这个表达式整体就可以看作一个方块了:

$$bcacpr$$

而 $\mathrm{coe}$ 是每个形成规则都必须给出的操作, 此时没有任何类型规则可以构造出上面的方形. 立方类型论引入了方形的复合操作来解决这个问题.

(..)

正则性

参见: Andrew Swan 问题

根据以上定义, 可将 J 公理定义为:

(..)

但 J 公理的计算规则并不成立: 对于根据自反性得到的相等证明, 对它使用 J 公理会触发化简. 在立方类型论中, 没有任何一条规则可以给出这样的化简, J 公理的计算规则只能被作为一个定理证明出来, 而不是一个类型论内置的规则. 内置形式的计算规则在立方类型论中叫做正则性, 在 [Angiuli 2019] 的第 3.4 节中给出了一个反例.

宇宙

宇宙作为定义泛等公理不可或缺的类型, 必然也要支持复合. 待复合的宇宙本身也是一种类型, 它必须要有构造规则和消去规则.

V 类型

在以上框架下, 直接将泛等公理作为一种新的类型加入类型论即可.

(..)

3开放问题

以下问题在立方类型论中尚未解决:

•	尚未存在高性能的编程语言实现.
•	Swan 问题.

4参考文献

•	Carlo Angiuli (2019). “Computational semantics of Cartesian cubical type theory”.

术语翻译

立方类型论 • 英文 cubical type theory

转换规则 • 英文 coercion rules

复合 • 英文 homogeneous composition

正则性 • 英文 regularity