Working experience on a new approach to the foundations of mathematics that lies in the intersection of Logic,
Computer Science and Mathematics.
Syllabus:
Homotopy Type Theory (HoTT) is a new approach to the foundations of
mathematics that revealed surprising connections between Martin-Löf's
Intensional Type Theory (ITT) and classical homotopy theory.
First we give an introduction to ITT and a detailed analysis of
Martin-Löf's axiom of path-induction, the elimination axiom for
equality, or path types, which was so difficult to grasp before
Voevodsky's homotopical interpretation of types as spaces, or better as
infinity groupoids. Through this interpretation ITT satisfies a certain
"principle of naturality" that makes its development unexpectedly
smooth. This naturality is preserved in the extension of ITT with
Voevodsky's axiom of univalence, a principle of special strength and
generality, the consequences of which are extensively studied. In the
last part of the course we present important theorems on path spaces of
higher inductive types like the higher circle and the higher spheres.
No prior knowledge of homotopy theory, mathematical logic or category
theory is required, just a working knowledge of basic algebra and topology.
Martin-Löf Type Theory, Univalence Axiom, Higher Inductive
Types, Synthetic Homotopy Theory
Teaching Material:
Homotopy Type Theory: Univalent Foundations of Mathematics, The
Univalent Foundations Program, Institute for Advanced Study, Princeton,
2013. https://homotopytypetheory.org/book/
| Author | Title | Publisher | Year | ISBN | Note |
| The Univalent Foundations Program | Homotopy Type Theory: Univalent Foundations for Mathematics. | Institute for Advanced Study | 2013 | Available on-line: https://homotopytypetheory.org/book/ |
Oral examination only.
