Μάθημα : Ειδικά Θέματα Λογικής: Θεωρία Τύπων

Επαγωγικοί τύποι και αναδρομή

• Ο τύπος τών φυσικών αριθμών
• Αναδρομή στούς φυσικούς αριθμούς
• Άλλα παραδείγματα επαγωγικών τύπων

Κατασκευαστική λογική

• Η ερμηνεία Brouwer-Heyting-Kolmogorov
• Φυσική απαγωγή
• Propositions-as-types

Ισότητα

Επαγωγή

Σύμπαντα

Η ιεραρχία τών τύπων ισότητας

Ανώτεροι επαγωγικοί τύποι και univalence

Propositional resizing and topos logic

Μαθηματικά στήν Ομοτοπική Θεωρία Τύπων / Η Ομοτοπική Θεωρία Τύπων ως θεμέλιο τών κατασκευαστικών-στρουκτουραλιστικών μαθηματικών (θεωρία ομοτοπίας, θεωρία κατηγοριών, θεωρία συνόλων)

Εισαγωγή στήν Agda

Δια ζώσης διδασκαλία

Εβδομαδιαίες ασκήσεις

Προετοιμασία και παρουσίαση θέματος τής επιλογής τού φοιτητή, από λίστα θεμάτων ή μετά από συνεννόηση με τόν διδάσκοντα.

Κάποιες προτάσεις για θέματα εργασίας.

 - Ισοδυναμίες (HoTTbook, 4.1–4.8)

 - Univalence implies function extensionality (HoTTbook, 4.9)

 - π₁(S¹) πλήρης υπολογισμός (HoTTbook, 8.1)

 - Θεωρία κατηγοριών στήν ομοτοπική θεωρία τύπων (HoTTbook, 9.1–9.5)

 - Θεωρία συνόλων στήν ομοτοπική θεωρία τύπων (HoTTbook, 10.1–10.5)

 - Universes and predicativity

     https://www2.math.uu.se/~palmgren/universe.pdf

 - Failure of canonicity, cubical type theory, etc.

     https://1lab.dev/1Lab.intro.html

     https://arxiv.org/abs/1911.05844

     https://arxiv.org/abs/1902.06572

 - Μεταμαθηματικά τής θεωρίας τύπων.

     https://iris.unitn.it/handle/11572/348681

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.

Egbert Rijke, Introduction to Homotopy Type Theory (2022).

Νίκος Ρήγας

nicolasr@di.uoa.gr