Erik Palmgren: On presheaf models of type theory
Time: Wed 2017-10-11 10.00 - 11.45
Location: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University
Participating: Erik Palmgren (SU)
Abstract. A presheaf model may be regarded as a generalisation of a Kripke model, where the frame is allowed to be a general category instead of just a partial order. In this talk we review some basic facts on such models, especially with reference to semantic structures for dependent types. We show in particular how the notion of iterated presheaves naturally give rise to contextual categories.