  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.
