Introdurre gli studenti all'Homotopy Type Theory, un nuovo approccio ai fondamenti della matematica che fornisce un punto d'incontro fra logica, computer science e matematica.
Al termine dell'insegnamento lo studente dovrà essere in grado di produrre argomentazioni e dimostrazioni rigorose e di leggere articoli e testi (anche avanzati) relativi alla Homotopy Type Theory.
Homotopy Type Theory (HoTT) costituisce un nuovo approccio ai fondamenti della matematica, che ha mostrato sorprendenti connessioni fra la Teoria dei Tipi Intensionale (ITT) di Martin-Löf e la teoria classica dell'omotopia.
Innanzitutto daremo un'introduzione ad ITT e un'analisi dettagliata dell'assioma di path-induction di Martin-Löf (l'assioma di eliminazione dell'uguaglianza) che si era mostrato di difficile comprensione prima dell'interpretazione omotopica di Voevodsky dei tipi come spazi, o meglio, come infinity groupoids. Attraverso questa interpretazione, ITT soddisfa un certo principio di naturalezza che rende il suo sviluppo inaspettatamente elegante. Questa naturalezza è preservata dall'estensione di ITT tramite il cosiddetto axiom of univalence di Voevodsky, un principio di particolare forza e generalità, le cui conseguenze verranno studiate dettagliatamente. Nell'ultima parte del corso presenteremo importanti teoremi sui path spaces di higher inductive types, quali ad esempio high circle e higher spheres.
Non è richiesta alcuna conoscenza preliminare di teoria dell'omotopia, teoria delle categorie o logica matematica, ma soltanto abilità operative di base in algebra e topologia.
Parole chiave: Martin-Löf Type Theory, Univalence Axiom, Higher Inductive Types, Synthetic Homotopy Theory
Al di fuori del monte ore dell'insegnamento, che comprende sia lezioni frontali che esercitazioni in aula, sono assegnati esercizi da svolgere a casa che vengono raccolti e corretti dal docente oppure discussi durante le ore di esercitazione.
| Autore | Titolo | Casa editrice | Anno | 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/ |
L'esame consiste in una sola prova orale a quesiti aperti e voti in trentesimi. Le modalità d’esame non sono differenziate fra frequentanti e non frequentanti.
L'esame ha lo scopo di verificare la piena maturità circa le tecniche dimostrative e la capacità di leggere e comprendere argomenti avanzati della Homotopy Type Theory.
