Polynomial functors: a general framework for induction and substitution

The starting point for this tutorial will be the Seely
correspondence between (extensional) dependent type theory and
locally cartesian closed categories, such as the category of
sets.  Under this correspondence, polynomial functors provide
semantics for generic data types, and their initial algebras
provide semantics for W-types (wellfounded trees).  While trees
in this approach are defined inductively, it is also possible to
define trees combinatorially, directly as certain multivariate
polynomial endofunctors.  This leads to an alternative
characterisation of initial algebras, namely as operations for
the free monad on a polynomial endofunctor.  The monad itself
has important structure not seen at the level of initial
algebras, namely the monad multiplication, which always encodes
a notion of subtitution.  I will finish with some outlook
regarding the role of polynomial monads (which are essentially
operads) to encode and manipulate combinatorial and algebraic
structures, and the need for groupoids and higher groupoids to
really unleash the power of this formalism -- also in
intensional type theory.