Title:

   Data types with symmetries and polynomial functors over groupoids

Speaker:

   Joachim Kock

Abstract: 

   Polynomial functors (over Set or other locally cartesian
   closed categories) are useful in the theory of data types,
   where they are often called containers.  They are also useful
   in algebra, combinatorics, topology, and higher category
   theory, and in this broader perspective the polynomial aspect
   is often prominent and justifies the terminology.  For
   example, Tambara's theorem states that the category of finite
   polynomial functors is the Lawvere theory for commutative
   semirings.
  
   In this talk I will explain how an upgrade of the theory from
   sets to groupoids (or other locally cartesian closed
   2-categories) is useful to deal with data types with
   symmetries, and provides a common generalisation of and a
   clean unifying framework for quotient containers (in the
   sense of Abbott et al.), species and analytic functors (Joyal
   1985), as well as the stuff types of Baez and Dolan.  The
   multi-variate setting also includes relations and spans,
   multispans, and stuff operators.  An attractive feature of
   this theory is that with the correct homotopical approach ---
   homotopy slices, homotopy pullbacks, homotopy colimits,
   etc. --- the groupoid case looks exactly like the set case.
  
   After some standard examples, I will illustrate the notion of
   data-types-with-symmetries with examples from perturbative
   quantum field theory, where the symmetries of complicated
   tree structures of graphs play a crucial role, and can be
   handled elegantly using polynomial functors over groupoids.
   (These examples, although beyond species, are purely
   combinatorial and can be appreciated without background in
   quantum field theory.)
  
   Locally cartesian closed 2-categories provide semantics for a
   2-truncated version of Martin-Lšf intensional type theory.
   For a fullfledged type theory, locally cartesian closed
   infinity-categories seem to be needed.  The theory of these
   is being developed by David Gepner and the author as a
   setting for homotopical species, and several of the results
   exposed in this talk are just truncations of infinity-results
   obtained in joint work with Gepner.  Details will appear
   elsewhere.