Miniseries "An introduction to homotopy type theory and univalent foundations"

Miniseries abstract: 
The field of homotopy type theory/univalent foundations (HoTT/UF) presents a new connection between topology and logic. It provides a foundational framework for mathematics where equivalent objects are identified. Moreover, in HoTT the basic objects carry homotopical information making it possible to do homotopy theory in a synthetic way. Using appropriate software, the proofs in HoTT/UF can be verified on a computer.

 

In this mini series, we'll give an introduction to the fundamental ideas of HoTT. The first talk by Jonathan Weinberger gives an introduction to the language of HoTT with a few hints on how this allows for doing synthetic homotopy theory. In the second talk, Léonard Guetta discusses the higher groupoidal structures of path/identity types and relations to Grothendieck's Homotopy Hypothesis. The final talk is given by Paige Randall North (University of Pennsylvania) and provides a detailed discussion of the Univalence Principle, going back to Vladimir Voevodsky, which states that equivalent mathematical structures are indistinguishable.