A ‘stuff type’ is a type of stuff that can placed on finite sets, e.g. ‘being a 2-colored finite set’, or ‘being the first of two finite sets’. To make this precise, we define a stuff type to be a functor
from some groupoid to the groupoid of finite sets and bijections, which is the core of the category FinSet. Equivalently, we can think of a stuff type as a 2-functor (of a suitably weakened sort, namely a pseudofunctor)
The idea is to use the Grothendieck construction and define
taking advantage of the fact that we may assume without loss of generality that is a fibration.
We can think of as a suitably weakened sort of presheaf of groupoids on . But since a groupoid is equivalent to its opposite, we can also think of a stuff type as a functor
If a stuff type
A stuff type can also be thought of as a categorified generating function. Whereas a generating function assigns a number to each natural number (or finite set), a stuff type assigns a groupoid. Namely, the stuff type
assigns to the finite set the groupoid . We can write as a power series where the coefficient of is the groupoid . In these terms, the structure type ‘being a finite set’ is
where is disjoint union, is the weak quotient, is the permutation group , and is the one-element set (since there’s only one way to be finite).
The structure type ‘being a totally ordered even set’ is
since there are ways to order a set with elements and ways for an odd set to be even.
One advantage of stuff types over the more familiar structure types (i.e., species) is that they allow one to categorify the theory of Feynman diagrams:
John Baez and James Dolan, From finite sets to Feynman diagrams, in Mathematics Unlimited - 2001 and Beyond, vol. 1, eds. Björn Engquist and Wilfried Schmid, Springer, Berlin, 2001, pp. 29-50. (arXiv)
Jeffrey Morton, Categorified algebra and quantum mechanics, Theory and Applications of Categories, 16 (2006), 785–854. (arXiv)