Time:  12:00  13:20 
Room: 
Wean Hall 7201

Speaker: 
Chris Kapulkin Department of Mathematics University of Pittsburgh 
Title: 
Π and Σ types in dependent type theory II

Abstract: 
As it was explained in Steve Awodey's talks on January 25th and February 8th, there are many deep connections between Intensional MartinLof Type Theory and homotopy theory. By interpreting type theory in Quillen model categoriesor more generally, in categories equipped with a (natural) weak factorization systemwe obtain a wide class of models for a type theory being an extension of a theory with only one type constructor Id. However, this interpretation does not (yet) take into account one of the key features of type theory that is the type constructors Pi and Sigma which under CurryHoward Isomorphism correspond to universal and existential quantifiers. In this talk, I will propose a set of conditions on a model category that make it into a model of a type theory that is any extension of the theory with Id, Pi, and Sigmatypes. These conditions will be further examine in a number of examples such as: the category of groupoids, the category of simplicial sets, and the category of preorders. A related 