Abstracts.2018.HoTT

Introduction to Homotopy Type Theory

by Jannis Limperg

Abstract

Univalent Foundations, aka Homotopy Type Theory, extends a dependent type theory with the univalence axiom, which implies functional and propositional extensionality and allows us to equate any two isomorphic types. I will give an introduction to the axiom and related concepts, including h-levels, equivalences, univalence, univalent logic and propositional truncation (if time permits).