There are two rather different approaches to classical plane geometry: Euclid's synthetic approach and Descartes analytic approach. In Descartes approach circles and lines are defined in terms of simpler notions as a set of points, while in Euclid's approach circles and lines are fundamental objects satisfying certain axioms and allowing certain constructions (like intersecting lines to get a point). In Euclid's approach, you can ask whether a point lies on a line, but you can't say that a line consists of a collection of points. Homotopy Type Theory was inspired by computer science, but it gives a synthetic approach to homotopy theory. That is, we think of spaces as basic notions which satisfy certain axioms and allow certain constructions, rather than defining them in terms of simpler notions (like certain topological spaces or certain simplicial sets). I will discuss some calculations of small homotopy groups using this synthetic approach. The rough idea is that CW complexes are \infty-groupoids with a given presentation in terms of generators and relations, and computing their homotopy groups is roughly like solving the word problem for a group. The usual way we solve the word problem for nice ordinary groups is to write down a free and transitive group action on something well understood. I will explain how to compute several examples of homotopy groups by writing down free and transitive actions of higher groups. This talk will be a mix of explaining results of Buchholtz, Brunerie, van Doorn, Rijke, Licata, Lumsdaine, and Shulman, and some new ideas from joint work with my student Nachiket Karnick and joint in part with our REU advisee Jacob Prinz. No previous knowledge of Homotopy Type Theory will be assumed (and I will mostly avoid using the language of type theory at all), and my hope is that this is a relaxing fun talk mostly about a different way to think about very old math beautiful mathematics of Pontryagin and others.
