In Homotopy Type Theory, few constructions have proved as troublesome as the smash product. While its definition is just as direct as in classical mathematics, one quickly realises that in order to define and reason about functions over iterations of it, one has to verify an exponentially growing number of coherences. This has led to crucial results concerning smash products remaining open. One particularly important such result is the fact that smash products form a (1-coherent) symmetric monoidal product on the universe of pointed types. This fact was used, without a complete proof, by e.g. Brunerie in his PhD thesis to construct the cup product on integral cohomology and is, more generally, a fundamental result in traditional algebraic topology. In this paper, we salvage the situation by introducing a simple informal heuristic for reasoning about functions defined over iterated smash products. We then use the heuristic to verify e.g. the hexagon and pentagon identities, thereby obtaining a proof of symmetric monoidality. We also provide a formal statement of the heuristic in terms of an induction principle concerning the construction of homotopies of functions defined over iterated smash products. The key results presented here have been formalised in the proof assistant Cubical Agda.

翻译：在同伦类型论中，很少有构造像 smash 积这样难以处理。虽然其定义与经典数学中一样直接，但人们很快意识到，为了定义并推理关于其迭代的函数，必须验证指数级增长的相干性。这导致关于 smash 积的关键结果至今仍未解决。其中一个特别重要的结果就是：smash 积在带点类型宇宙上构成（1-相干）对称幺半群乘积。该结果曾被 Brunerie 在其博士论文中用于构造整上同调中的 cup 积（但未给出完整证明），并且更广泛而言，它是传统代数拓扑学中的一个基本结果。本文通过引入一个简单的非正式启发式方法，用于推理定义在迭代 smash 积上的函数，从而解决了该问题。然后我们利用这一启发式方法验证了六边形和五边形恒等式等，进而得到了对称幺半群性质的证明。我们还基于关于构造迭代 smash 积上函数同伦的归纳原理，给出了该启发式方法的正式陈述。本文提出的关键结果已在证明辅助工具 Cubical Agda 中形式化。