Axel Ljungström: Dealing With Smash Products in HoTT

Abstract

Verifying that the smash product forms a symmetric monoidal product in HoTT turns out to be rather complicated. There is no deeper reason for this: it should, in theory, follow by induction. However, the number of coherences which need to be verified grows too quickly for anyone in their right mind to actually complete the proof. Some solutions have been suggested: van Doorn (2018) attacked the problem by an argument using closed monoidal categories while Brunerie (2018) attempted to produce a computer generated proof using Agda meta-programming. Unfortunately, van Doorn left a gap where the path algebra got too involved and Brunerie's generated proof failed to type-check due to it eating up far too much memory.

In this talk, we choose a different line of attack by introducing a heuristic for proving equalities of pointed maps defined over iterated smash products. With this heuristic, we significantly bound the number of coherences appearing in such proofs. In particular, this heuristic lets us prove that smash products are symmetric monoidal in a rather straightforward manner.