Studying at the University of Verona
Here you can find information on the organisational aspects of the Programme, lecture timetables, learning activities and useful contact details for your time at the University, from enrolment to graduation.
Study Plan
This information is intended exclusively for students already enrolled in this course.If you are a new student interested in enrolling, you can find information about the course of study on the course page:
Laurea magistrale in Mathematics - Enrollment from 2025/2026The Study Plan includes all modules, teaching and learning activities that each student will need to undertake during their time at the University.
Please select your Study Plan based on your enrollment year.
1° Year
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
| Modules | Credits | TAF | SSD |
|---|
3 course to be chosen among the followingOne course to be chosen among the followingLegend | Type of training activity (TTA)
TAF (Type of Educational Activity) All courses and activities are classified into different types of educational activities, indicated by a letter.
Advanced course in foundations of mathematics (2016/2017)
Teaching code
4S001104
Academic staff
Coordinator
Credits
6
Language
English
Scientific Disciplinary Sector (SSD)
MAT/01 - MATHEMATICAL LOGIC
Period
II sem. dal Mar 1, 2017 al 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.
Program
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 | Publishing house | Year | ISBN | Notes |
|---|---|---|---|---|---|
| The Univalent Foundations Program | Homotopy Type Theory: Univalent Foundations for Mathematics. | Institute for Advanced Study | 2013 | Available on-line: https://homotopytypetheory.org/book/ |
Examination Methods
Oral examination only.
