Abstract: Homotopy type theory is a foundation for mathematics that is well-suited to do homotopy theory. Unlike ZFC, we no longer have access to the law of excluded middle or the axiom of choice. Many mathematicians find it daunting and off-putting to work without these axioms, but great opportunity is created amidst the challenge.

In this talk we will investigate how we can do homotopy theory in homotopy type theory. We will construct the fundamental group of the circle by using the tools provided by Martin-Löf type theory, Voevodsky’s univalence axiom, and higher inductive types. In particular, we will look at the underlying language of type theory and its identity types, how fiber bundles are expressed as type families, and the essential role played by the univalence axiom.