Till innehåll på sidan

Chris Kapulkin: Type theory and locally cartesian closed quasicategories

Tid: On 2015-05-27 kl 10.00 - 11.45

Plats: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university

Medverkande: Chris Kapulkin, University of Western Ontario

Exportera till kalender

Let T be a dependent type theory admitting the rules for Pi-, Sigma-, and Id- types, and let C(T) be its syntactic category, that is, the category whose objects are contexts and whose morphisms are (sequences of) terms. This category is naturally equipped with a class of syntactically defined weak equivalences and as such presents some quasicategory. It is then natural to ask what can we say about this quasicategory. After explaining the necessary background, I will show a proof that the quasicategories arising this way are locally cartesian closed. This answers the question posed by Andre Joyal in his talk at the Oberwolfach mini-workshop on HoTT in 2011.