Introduction to Homotopy Type Theory

3 Vorträge von Dr. Roberta Bonacina (Tübingen) im Rahmen des Carl Friedrich von Weizsäcker-Kolloquiums
Homotopy type theory is a vibrant research field in contemporary  Mathematics. It aims at providing a foundation of Mathematics  extending Martin-Löf type theory with the central notion of  univalence, which induces a connection between types and homotopy  spaces.
We will begin the short course defining the simple theory of types,  and showing how it can be extended to Martin-Löf type theory and then  to Homotopy type theory. We will stress the propositions-as-types  interpretation between the type theories and intuitionistic logic, and  study in detail the notion of equality. Then we will show how  classical logic can be done in this intuitionistic setting, allowing  to introduce the law of excluded middle and the axiom of choice as  axioms. Finally, we will analyse the different definitions of  equivalence, which are fundamental to introduce univalence.

Sie sind herzlich eingeladen, via ZOOM an diesem Kolloquium teilzunehmen. Den Link zur Registrierung und weitere Informationen finden Sie auf der Seite des Zentrums
uni-tuebingen.de/de/198526