Nicola Gambino (University of Palermo), Homotopy-initial W-types
Schedule
- March 1, 2012, 14:00 - 15:00
Abstract
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.
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.