turkmath.org

Homotopy Type Theory is a new approach to the foundations of mathematics, in which the basic objects of mathematics are not sets but homotopy types. It is natively isomorphism-invariant and well-adapted to computer formalization, and can be interpreted in higher toposes to give a synthetic language for internal constructions and proofs. It can also be explained intuitively to students, giving them access to higher structures while avoiding the complicated machinery of combinatorial homotopy theory; and it can be used as a programming language, to compute certain invariants of higher structures by simply running code derived from their definitions. However, until recently it was not known how to achive both of these latter two properties simultaneously with a single formal system. In this talk I will introduce Homotopy Type Theory and its applications to higher structures from perspective of Higher Observational Type Theory; this is a new formal system for Homotopy Type Theory that, we hope, is both intuitively natural and computationally adequate. This is joint work in progress with Thorsten Altenkirch and Ambrus Kaposi.