Michael Warren (Pittsburgh) Model categories and intensional identity types Abstract: Quillen model categories provide a flexible axiomatic framework in which to develop the homotopy theory of various categories. In this talk we will show that model categories also provide a framework in which to develop the semantics of Martin-Löf's intensional type theory. In particular, the internal language of any model category, in which fibrant objects are closed types and fibrations are dependent types, contains a form of intensional identity type arising from the path objects present in the model structure. We explore this connection further by considering several variations on this theme as well as looking at dependent products and sums in the setting of Quillen model categories. If time permits the connection between cocategory objects and model structures will also be discussed.