同伦类型论中的对称幺半群smash积

在同伦类型论中，很少有构造像smash积这样被证明是棘手的。尽管其定义与经典数学中一样直接，但人们很快意识到，为了定义和推理其迭代上的函数，必须验证呈指数级增长数量的协调性条件。这导致关于smash积的关键结果一直悬而未决。其中一个特别重要的结果是，smash积在指向类型的宇宙上形成一个（1-协调的）对称幺半群积。例如，Brunerie在其博士论文中使用了这一事实（但未给出完整证明）来构造整系数上同调上的杯积，更一般地，这是传统代数拓扑中的一个基本结果。在本文中，我们通过引入一种简单的非正式启发式方法来推理定义在迭代smash积上的函数，从而挽救了这一局面。然后，我们使用该启发式方法验证了例如六边形和五边形恒等式，从而获得了对称幺半性的证明。我们还就该启发式方法给出了一个形式化陈述，其形式为一个归纳原理，该原理涉及定义在迭代smash积上的函数的同伦构造。本文提出的关键结果已在证明助手Cubical Agda中形式化。