基于 Agda 的单值数学基础导论

我们介绍 Voevodsky 的单值基础（univalent foundations）与单值数学（univalent mathematics），并解释如何借助基于 Martin-Löf 类型论的计算机系统 Agda 来发展它们。Agda 允许我们编写数学定义、构造、定理与证明，例如数论、分析、群论、拓扑、范畴论或编程语言理论中的内容，并对其逻辑与数学正确性进行检验。Agda 默认是一个构造性数学系统，这等于说它也可被视为一种用于操作数学对象的编程语言。但对于需要它们的数学片段，我们可以假定选择公理或排中律，代价是失去系统隐式的编程语言特性。为了在 Agda 中完全构造性地发展单值数学，我们需要使用其新的立方（cubical）风格，我们希望这些笔记能为有兴趣学习立方类型论与立方 Agda 作为下一步的研究者提供基础。与大多数相关论述相比，我们使用显式的宇宙层级（universe levels）。