A constructive model of synthetic homotopy theory in classical homotopy theory

In 2022, Axel Ljungström and Anders Mörtberg calculated π_4S^3 using the computer proof assistant Cubical Agda. They first implemented a constructive proof due to Guillaume Brunerie that π_4S^3 is Z/nZ for some integer n and then asked Cubical Agda to run that algorithm to calculate the value of n (which turned out to be -2). This anecdote motivates the search for constructive models of synthetic homotopy theory (HoTT).

Proofs in Cubical Agda can be converted to proofs in set theory via a model which interprets the types and terms of Cubical Agda into a particular category of cubical sets equipped with a Quillen model structure. While this model structure gives this category of cubical sets "a homotopy theory" it is known not to be the homotopy theory of spaces. This talk will describe a recent preprint with Steve Awodey, Evan Cavallo, Thierry Coquand, and Christian Sattler that gives a constructive model of HoTT in a different category of cubical sets equipped with a new "equivalent" model structure that presents the classical homotopy theory of spaces.