Thomas Thorbjørnsen (Western University): An Informal Introduction to Homotopy Type Theory

Abstract: Homotopy Type Theory is an alternate foundation of mathematics that is well-suited to do homotopy theory in a more general settings than topological spaces. Unlike ZFC, this theory is constructive, i.e. does not admit the law of excluded middle, nor the axiom of choice. Many mathematicians find it daunting to not work with these principles, but more flexibility and new opportunities are created amidst the challenge. One of the most interesting properties is that this gives us a way to syntactically reason internally in infinity-topoi. We will first look at how we can work internally in this language, and different ways to interpret these results. We will secondly investigate some homotopy relevant mathematics that we can develop inside homotopy type theory. In particular we will look at homotopy groups of types and spectral sequences defined along arbitrary maps.