Symmetric Monoidal Smash Products in Homotopy Type Theory
Axel Ljungström
TL;DR
The paper resolves a long-standing challenge in HoTT by proving that the smash product is a $1$-coherent symmetric monoidal structure on the universe of pointed types, using an informal yet effective heuristic to manage iterated coherence conditions. It introduces a higher inductive construction for double smash products, develops a practical induction principle for homotopies, and demonstrates hexagon and pentagon coherence via this approach, with all results formalised in Cubical Agda. The work also connects to Brunerie’s cup product construction, confirming its graded-commutativity and associativity through the established monoidal framework. Finally, it outlines a formal statement of the heuristic and discusses potential extensions to related algebraic-topology structures, such as Whitehead products and polyhedral-like constructions, within synthetic homotopy theory.
Abstract
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.