Advanced course in foundations of mathematics (2016/2017)

Course code
Name of lecturers
Peter Michael Schuster, Iosif Petrakis
Peter Michael Schuster
Number of ECTS credits allocated
Academic sector
Language of instruction
II sem. dal Mar 1, 2017 al Jun 9, 2017.

Lesson timetable

II sem.
Day Time Type Place Note
Wednesday 2:30 PM - 5:30 PM lesson Lecture Hall M from Mar 1, 2017  to Apr 30, 2017
Thursday 11:30 AM - 2:30 PM lesson Lecture Hall B from Mar 16, 2017  to Jun 9, 2017

Learning outcomes

Working experience on a new approach to the foundations of mathematics that lies in the intersection of Logic,
Computer Science and Mathematics.



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,

Reference books
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:

Assessment methods and criteria

Oral examination only.

Student opinions - 2015/2016

Statistics about transparency requirements (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

Data from AA 2016/2017 are not available yet