Tags:Categorical semantics, Dependent type theory and Polynomial functors

Abstract:

This talk is an overview of my PhD thesis (supervised by Steve Awodey), which develops the theory of natural models of dependent type theory, an essentially algebraic notion which is equivalent to Dybjer's categories with families. In particular, we explore a connection with polynomial functors, and we discuss how to freely extend a natural model by type theoretic structure.