同伦类型论路径空间中计算路径的应用

在类型论中将等式视为一种类型，产生了一种有趣的类型论结构，称为“恒等类型”。其思想是：给定类型 $A$ 的项 $a,b$，可以构造类型 $Id_{A}(a,b)$，其元素即为 $a$ 与 $b$ 作为类型 $A$ 中相等元素的证明。该类型的一个项 $p : Id_{A}(a,b)$ 构成了确立 $a$ 确实等于 $b$ 的依据（或证明）。基于此，等式的证明可被视为一系列替换与重写，也称为“计算路径”。一个有趣的事实是，可以利用由路径中冗余性分析得出的一组归约规则来重写计算路径。这些规则由 De Oliveira 于 1994 年在一个称为 $LND_{EQ}-TRS$ 的项重写系统中给出。此处我们利用计算路径及该项重写系统来处理路径空间。在同伦类型论中，定义路径空间的主要技术是 code-encode-decode 方法。我们的目标是提出一种基于计算路径理论的替代方法。我们认为这种新方法比 code-encode-decode 方法更简单直接。随后我们利用该方法获得了同伦类型论的两个重要结果：自然数路径空间的构造与圆的基群的计算。