Till innehåll på sidan

Erik Palmgren: On presheaf models of type theory, II

Tid: On 2017-10-18 kl 10.00

Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University

Medverkande: Erik Palmgren

Exportera till kalender

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.

(This is a continuation of last week’s seminar on the same topic.)