Nicola Gambino (University of Palermo), Homotopy-initial W-types


  • March 1, 2012, 14:00 - 15:00


It is well-known that within the extensional version of Martin-Lof type theory the deduction rules for W-types are equivalent to the existence of initial algebras for polynomial functors. The aim of the talk is to examine what happens to this characterization in the intensional version of Martin-Lof type theory. I will also show how some inductive types can be represented as W-types assuming a propositional version of the principle of function extensionality. The talk is based on joint work with Steve Awodey and Kristina Sojakova.