- Feb 9. The topos of trees and guarded recursion. First 17 slides of these slides. (Rasmus)
- Feb 15. Seely: Locally cartesian closed categories and type theory and Awodey, Category Theory, chapter 8.7 and 9.7. (Rasmus)
- Feb 22. Simon Huber: Cubical interpretation of type theory (PhD thesis) chapter 1. Alternative source: Martin Hofmann: Syntax and semantics of dependent types (Marie)
- Mar 1.Huber chapter 1 continued (Marie) and a bit of universes in locally cartesian closed categories (Rasmus)
- Mar 8. Robert Atkey and Conor McBride: Productive coprogramming with guarded recursion (Christian)
- Mar 15. Bizjak et al: Guarded dependent type theory with coinductive types (Patrick)
- Mar 22 and 29. Ales Bizjak and Rasmus Møgelberg: Paper in progress (Rasmus)
- Apr 5. Martin Hofmann and Thomas Streicher: The groupoid interpretation of type theory (Bassel)
- Apr 19. Awodey and Warren: Homotopy theoretic models of identity types (Bassel)
- April 26 and May 3. HoTT book Chp 2 (Marie)
- May 10. HoTT book Chp 3 (Christian)
- May 24. HoTT book Chp 4 (Danil)
- Some day in the future. Marc Bezem, Thierry Coquand and Simon Huber: A model of type theory in cubical sets
- ...