Posted in

Speaker:

Félix Loubaton
Affiliation:

MPIM
Date:

Thu, 13/06/2024 - 15:00 - 16:00
Location:

MPIM Lecture Hall
Parent event:

MPI-Oberseminar In this talk I'll try to give an overview of (homotopic) type theory, a theory which produces a very important link between computer science and homotopy theory and which is at the heart of modern proof assistants.

We'll start with concrete examples from computer science, which will allow us to introduce Martin-Löf's dependent type theory. We'll then talk about Voevodsky's univalence axiom and finally the interepration of this theory in simplicial sets by Voevodsky, Lumsdaine and Warren.

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