Guillaume Brunerie (IAS)|
Invariant homotopy theory in homotopy type theory
Abstract: This talk will be about homotopy type theory and in particular the branch of it known as invariant homotopy theory, or synthetic homotopy theory.
The main idea is that homotopy type theory is a formal language which can be used to talk about "spaces-up-to-homotopy-equivalence". The basic objects can be thought of as spaces, but the language has the property that all the structures, properties, constructions and proofs that we can express are invariant under homotopy equivalence.
One advantage is that every construction or proof done in this setting is expected to be automatically valid in every infinity-topos, not just in the infinity-topos of spaces, while still looking elementary. In this sense, we can see homotopy type theory as an internal language for infinity-topoi. Moreover, such proofs are also amenable to computer formalization, as homotopy type theory is strongly related to computer proof assistants.
I will present the basic concepts and show what a few proofs and constructions look like in invariant homotopy theory. In particular, we will see the universal cover of the circle, the Hopf fibration, cohomology, and the Steenrod operations.