This is the seminar on models of type theory. We will meet once a week to discuss papers following the below (tentative) schedule. We meet Wednesdays at 10-12 in 4A22 except March 1 and 8.

  • 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
  • ...