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)

Spring 2017