Introduction to synthetic homotopy theory
Introduction to synthetic homotopy theory
-
Guillaume Brunerie, IAS
Homotopy type theory is a young field at the interface between听mathematics, logic, and computer science. It studies a variety of听connections between algebraic topology (more precisely, homotopy听theory) and dependent type theory (a class of formal systems听extensively studied in logic and computer science).听听In this talk I will focus on the aspect of homotopy type theory called听"synthetic homotopy theory", whose aim is to use the language of听dependent type theory in order to study homotopy theory. I will听introduce the main concepts and show various examples of theorems from听homotopy theory that we can prove in this setting.