Posted in

Organiser(s):

Barthel, Ozornova, Ray, Teichner
Date:

Mon, 14/03/2022 - 15:00 - 16:00 For zoom details contact: Barthel, Ozornova, Ray, Teichner.

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.

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.

© MPI f. Mathematik, Bonn | Impressum & Datenschutz |