Published on *Max Planck Institute for Mathematics* (https://www.mpim-bonn.mpg.de)

Posted in

- Seminar [1]

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.

**Links:**

[1] https://www.mpim-bonn.mpg.de/taxonomy/term/41

[2] https://www.mpim-bonn.mpg.de/node/11271/program?page=last

[3] https://www.mpim-bonn.mpg.de/node/11271/abstracts