The Univalence Axiom in Dependent Type Theory
Lecturer:
Marc Bezem
(University of Bergen).
About the lecturer | Course Summary | Slides | Assignment
About the lecturer:
Marc Bezem holds a PhD in mathematical logic from Utrecht University
(1986, supervisors Troelstra and van Dalen).
After his graduation he worked as a postdoc
at CWI (Amsterdam, 1986-1990), before assuming a permanent position
at the Faculty of Philosophy of Utrecht University. In the year 2000 he
was appointed professor of computer science at the University of Bergen,
Norway. His research interests can be characterized as computational logic,
the interdisciplinary field of computer science, logic and mathematics.
He currently studies the new homotopy interpretation of type theory
that has led to the univalence axiom.
Course summary: We give an informal introduction to type theory, sketching the development from higher-order logic to dependent type theory. Thereafter we present the recently found homotopy interpretation of equality and universe, leading to the novel axiom of univalence.
We will try to cover as much as possible of the material in the first two chapters of the book Homotopy Type Theory: Univalent Foundations of Mathematics, which is freely available online.
Suggested reading: To get in the right mood, before the course begins it would be useful to read the Introduction and Section 1.1. from the book mentioned above.
Slides to the lecture can be found here.
Assignment: You can find the problem set here. Please send the solutions to the address provided on the problem sheet by Friday, January 13.