As it was explained in Steve Awodey's talks on January 25th and February 8th, there are many deep connections between Intensional Martin-Lof Type Theory and homotopy theory. By interpreting type theory in Quillen model categories---or more generally, in categories equipped with a (natural) weak factorization system---we 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 Curry-Howard 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 Sigma-types. 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