Joachim's web pages
[Home]
[Math]
[Cat]

# Data types with symmetries and polynomial functors over groupoids

By Joachim Kock
Proceedings of the 28th Conference on the
Mathematical Foundations of
Programming Semantics, Bath 2012, *Electronic Notes in Theoretical Computer
Science* **286** (2012), 351-365.
ArXiv:1210.0828

#### 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 \cite{Tambara:CommAlg},
\cite{Gambino-Kock:0906.4931}.
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\"of intensional type theory. For a fullfledged type
theory, locally cartesian closed $\infty$-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 $\infty$-results obtained in joint work with
Gepner. Details will appear elsewhere.

Last updated: 2013-08-14 by
Joachim Kock.