I'm happy that my proposal for an introductory course on Homotopy Type Theory / Univalent Foundations at the European Summer School in Logic, Language and Information 2026 in Prague was accepted!
A great opportunity to make use of @egbertrijke's recently published book, @MartinEscardo's lecture notes (in Agda!) and @danielgratzer and @carloangiuli's book draft!
Links for the curious:
- Egbert's book: https://doi.org/10.1017/9781108933568 & https://arxiv.org/abs/2212.11082
- Martín's notes: https://cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html
- Daniel and Carlo's book draft: https://www.danielgratzer.com/papers/type-theory-book.pdf
