This is the seminar on models of type theory. We meet Thursdays 10-12 in room 4A20.
  • Sept 21, 28 and Oct 5: Huber thesis chapter 2 and 3 (Bassel)
  • Oct 12, Nov 9, 16 and 23: Huber thesis chapter 6 (Niccolo)
  • Nov 30: Huber thesis chapter 7 (Christian)
  • Dec 7: Guarded cubical type theory (Bassel).

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