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.