Η κατασκευαστική θεωρία τύπων διατυπώθηκε αρχικά με σκοπό τη θεμελίωση των κατασκευαστικών μαθηματικών. Εδώ και λίγα χρόνια, οι τυποθεωρητικές μέθοδοι έχουν αποδειχθεί ιδιαίτερα γόνιμες στη θεωρία της ομοτοπίας, όπου η γεωμετρική ερμηνεία των τυποθεωρητικών εννοιών έχει οδηγήσει σε συνθετικές περιγραφές γεωμετρικών δομών (ομοτοπικών τύπων των χώρων) και συνθετικές αποδείξεις θεωρημάτων της αλγεβρικής τοπολογίας και της ομοτοπικής θεωρίας.
Θα παρουσιάσουμε την ομοτοπική θεωρία τύπων (Homotopy Type Theory/HoTT) με έμφαση στις κεντρικές της έννοιες και κατασκευές (π.χ. μονοδυναμία, ανώτεροι επαγωγικοί τύποι) και θα προσεγγίσουμε σημαντικές έννοιες και αποτελέσματα γεωμετρικού ενδιαφέροντος από την παραδοσιακή ομοτοπική θεωρία των τοπολογικών χώρων, όπως αυτά προκύπτουν με ένα λογικο-συντακτικό τρόπο μέσα από το νέο τυποθεωρητικό πλαίσιο.
Σύνοψη περιεχομένου: Εισαγωγή στη θεωρία τύπων - επαγωγικοί τύποι - propositions as types - ισότητα - ισοδυναμία τύπων - σύμπαντα - μονοδυναμία (univalence) - ανώτεροι επαγωγικοί τύποι - ανάπτυξη ομοτοπικών εννοιών στη θεωρία τύπων (homotopy pullbacks, homotopy pushouts, descent, ομοτοπικές ομάδες) - η ομοτοπική θεωρία χώρων (simplicial homotopy theory) ως μοντέλο της ομοτοπικής θεωρίας τύπων.
Ώρα: Κάθε Πέμπτη 6–9 μμ (υβριδικά) [2 ώρες μαθήματος + συζήτηση]
Τοποθεσία: Αίθουσα διδασκαλίας Ζ Τμήματος Πληροφορικής & Τηλεπικοινωνιών
Πληροφορίες: Για τεχνικές πληροφορίες (π.χ. zoom link) και λεπτομέρειες του προγράμματος διαλέξεων (π.χ. περιγραφές περιεχομένου, ερωτήσεις για τη βιβλιογραφία, παρουσιάσεις από τους συμμετέχοντες, μέθοδοι εξέτασης), παρακαλούμε να επικοινωνήσετε με τον κ. Ρήγα (nicolasr “at” di.uoa.gr).
(1) 14.11.2024 (Ν. Ρήγας): Επαγωγικοί τύποι και αναδρομή. Οι φυσικοί αριθμοί. Παραδείγματα. Τύποι συναρτήσεων. Φυσική απαγωγή. Αντιστοιχία Curry-Howard. Ισότητα και επαγωγή. Μεταφορά (transport). Σύμπαντα. Κύριες αναφορές: [4, 1–3 & 4], [3], [1].
(2) 21.11.2024 (tbd): Η δομή ανώτερου ομαδοειδούς των τύπων. Χαρακτηρισμός της ισότητας στα εξαρτώμενα αθροίσματα. Ισοδυναμίες. Συσταλτοί (contractible) τύποι και συσταλτές απεικονίσεις. Κύριες αναφορές: [4, 4–6 & 7], [5], [1].
(3) 28.11.2024 (tbd): Η ιεραρχία των τύπων και function extensionality. Εισαγωγή στην έννοια της μονοδυναμίας (univalence). Homotopy pullbacks. Κύριες αναφορές: [4, 8–9 & 10–11],[5], [1].
(4) 05.12.2024 (tbd): Homotopy pullbacks (συνέχεια). Το αξίωμα της μονοδυναμίας και βασικές συνέπειες. Κύριες αναφορές: [4, 10–11], [5], [1].
(5) 12.12.2024 (tbd): Ανώτεροι επαγωγικοί τύποι. Ο κύκλος. Homotopy pushouts. Κύριες αναφορές:[4, 12–13], [1].
(6) 19.12.2024 (tbd): Ιδιότητες καθόδου (descent) στην ομοτοπική θεωρία τύπων. Κύριες αναφορές: [4, 14–15], [1].
(7) 09.01.2025 (tbd): Προτασιακή αποκοπή (truncation). Ομοτοπικές ομάδες στη θεωρία τύπων. Εφαρμογές. Κύριες αναφορές: [4, 16–17 & 18–19], [1].
(8)-(9) 16.01.2025 & 23.01.2025 (tbd): Μετάβαση από το συντακτικό της θεωρίας τύπων στις πλαισιακές κατηγορίες (contextual categories). Κύριες αναφορές: [2, 11–12, Παραρτήματα] & [2, 13–14].
(10)-(11) 30.01.2025 & 06.02.2025 (tbd): Simplicial sets ως μοντέλο της ομοτοπικής θεωρίας τύπων. Κύριες αναφορές: [2, 2–3].
Αναφορές
[1] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, https://homotopytypetheory.org/book/ Institute for Advanced Study, 2013.
[2] C. Kapulkin and P. Lefanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky).
[3] P. Martin-Löf, Intuitionistic Type Theory, Studies in Proof Theory Vol. 1, Bibliopolis, Napoli, 1984.
[4] E. Rijke, Introduction to homotopy type theory. https://github.com/EgbertRijke/HoTT-Intro/blob/master/pdfs/2018-hott-intro-course.pdf.
[5] M. Shulman, Homotopy type theory: the logic of space.