Axel Ljungström: Steenrod squares, the HoTT way

Abstract

The Steenrod squares (\(Sq^n\)) form a set of cohomology operations which can, among other things, be useful for distinguishing different spaces whose cohomology rings happen to be the same. In this talk, I will show you how to construct these in homotopy type theory (HoTT) and how one very simple (but, it turns out, surprisingly hard to prove) Fubini-like theorem for unordered joins implies both the so-called Cartan formula and the Adem relations. I will also discuss how the proofs of the suspension axiom and \(Sq^0(x) = x\) can be reduced to a computational problem and thereby give rise to a new Brunerie number. Finally, I might say a word or two about why the higher Steenrod powers are so hard to define in HoTT (coherence problems? You bet!).