A (combinatorial) species is a presheaf or higher categorical presheaf on the groupoid core(FinSet).

A species is a symmetric sequence by another name. Meaning: they are categorically equivalent notions.



The category of species, Species:=PSh(core(FinSet))Species := PSh(core(FinSet)), is the category of presheaves on the groupoid :=core(FinSet)\mathbb{P} := core(FinSet) of finite sets and bijections, the core of FinSet:

^:=PSh(core(FinSet)). \hat \mathbb{P} := PSh(core(FinSet)) \,.

For more, see structure type.


A 2-species (usually called a stuff type) is a 2-presheaf on core(FinSet), i.e. a pseudofunctor

core(FinSet)Grpd core(FinSet) \to Grpd

to the 2-category Grpd.


Generally, an \infty-species or homotopical species is an (∞,1)-presheaf on core(FinSet)core(FinSet), i.e. an (∞,1)-functor

core(FinSet) opGrpd core(FinSet)^{op} \to \infty Grpd

to the (∞,1)-category ∞Grpd.

The (∞,1)-category of \infty-species is the (∞,1)-category of (∞,1)-presheaves

Species:=PSh (,1)(core(FinSet)), \infty Species := PSh_{(\infty,1)}(core(FinSet)) \,,

For more on this see also below the discussion In homotopy type theory.

Operations on species

There are in fact 5 important monoidal structures on the category of species. For a discussion of all five, you’ll currently have to read about Schur functors, where these operations are discussed in the context of FinVectFin\Vect-valued species, i.e. FinVectFin\Vect-valued presheaves on the groupoid of finite sets. But here are two:


The sum A+BA + B of two species AA, BB is their coproduct ABA \coprod B. Since colimits of presheaves are computed objectwise, we have

(A+B) nA nB n. (A + B)_n \simeq A_n \coprod B_n \,.


The category core(FinSet)core(FinSet) becomes a monoidal category under disjoint union of finite sets. This monoidal structure (core(FinSet),)(core(FinSet), \coprod) induces canonically the Day convolution monoidal structure on Species:=PSh(core(FinSet))Species := PSh(core(FinSet)).

For AA and BB two combinatorial species, their product is given by the coend

(AB) n nFinSetA k×B l×Hom core(FinSet)(n,k+l) k+l=n (k+l)!k!+l!(A k×B l). (A \otimes B)_n \simeq \int^{n \in FinSet} A_k \times B_l \times Hom_{core(FinSet)}(n,k+l) \simeq \coprod_{k+l = n} \prod_{\frac{(k+l)!}{k! + l!}} (A_k \times B_l) \,.

In Homotopy Type Theory

The following discusses formalization of the concept of species in homotopy type theory.

Let FinSet be the type of finite sets (see at hSet). Notice that in homotopy type theory this automatically comes out as the groupoid of finite sets (see also at universe in type theory), so we may (and do) suppress writing “core” here.


A species is a type X:TypeX \colon Type equipped with a function into FinSetFinSet. Hence the type of all species is the dependent sum

Species X:Type(XFinSet) Species \coloneqq \sum_{X : Type} (X \to FinSet)

of all function types XFinSetX \to FinSet as XX ranges over the type of types.


FinSetFinSet 0 FinSet \longrightarrow {\|FinSet\|_{0}} \simeq \mathbb{N}

for the unit of the 0-truncation modality on FinSet, going into the type of natural numbers.

Given a species f:XFinSetf \colon X \to FinSet as in def. 1, its “decategorification” is the composite

fcard:XfFinSetFinSet 0 f \circ card \colon X \stackrel{f}{\longrightarrow} FinSet \to {\|FinSet\|_{0}} \simeq \mathbb{N}

The generating function of a species f:XFinSetf \colon X \to FinSet, def. 1, is

|X|(z) n=0 |fib fcard(n)|z n= n=0 |fib f(Fin(n))|z nn!, {|X|}(z) \coloneqq \sum_{n=0}^{\infty} {\big| fib_{f \circ card}(n) \big|}\, z^{n} = \sum_{n=0}^{\infty} {\big| fib_{f}(Fin(n)) \big|}\, \frac{z^{n}}{n!} \,,

where fib()fib(-) denotes the homotopy fiber and Fin(n)Fin(n) denotes a 0-type with exactly nn elements.


If Φ:FinSetType\Phi : FinSet \to Type is a family of types, then we obtain the species

pr 1:( A:FinSetΦ(A))FinSet pr_{1} : \bigg(\sum_{A : FinSet} \Phi(A)\bigg) \to FinSet

with generating function

|Φ|(z)= n=0 |Φ(Fin(n))|z nn! {|\Phi|}(z) = \sum_{n=0}^{\infty} {|\Phi(Fin(n))|} \frac{z^{n}}{n!}

If Φ\Phi is a stuff, structure, or property on finite sets, then we immediately know something about its generating function, considered as an exponential generating function:

  • If Φ(A)\Phi(A) is contractible for all AA, then Φ(Fin(n))=1\Phi(Fin(n)) = 1, so its generating function is the exponential function e ze^{z}.

  • If Φ(A)\Phi(A) is a family of mere propositions, then every coefficient is either 00 or 11, according to whether AA can be equipped with a Φ\Phi-structure or not.

  • If Φ(A)\Phi(A) is a family of sets (i.e., a structure type), then every coefficient is an element of the type of natural numbers \mathbb{N}.

  • If Φ(A)\Phi(A) has a higher homotopy level (i.e., is a stuff type), then the coefficients are in [0,)[0, \infty).


Since any species f:XTypef : X \to Type is equal to

pr 1:( x:Xfib f(x))Type pr_{1} : \bigg(\sum_{x:X}fib_{f}(x)\bigg) \to Type

every species is equal to one obtained from a stuff type.

Operations on species

The five monoidal structures mentioned above under Operations on species can be represented in HoTT, along with a couple other useful operations. We give four of the five monoidal structures here. For more operations, see (Dougherty15). We assume throughout this subsection that f:XFinsetf : X \to \Finset and g:YFinsetg : Y \to Finset are two species, and Φ,Ψ:FinSetType\Phi, \Psi : FinSet \to Type are two stuff types.


The recursion principle for the coproduct gives the species

(f+g) : X+YFinset (f+g) : rec X+Y(FinSet,f,g)=z{f(x) ifzinlx g(y) ifzinry. \array{ (f + g) &:& X + Y \to Finset \\ (f + g) &:& rec_{X + Y}(FinSet, f, g) = z \mapsto \left\{\array{ f(x) & \text{if}\; z \equiv inl x \\ g(y) & \text {if}\; z \equiv inr y .}\right. }

If XX and YY are obtained from Φ\Phi and Ψ\Psi, respectively, then the coproduct is equal to

A:FinSet(Φ(A)+Ψ(A)) \sum_{A : FinSet} (\Phi(A) + \Psi(A))

The generating function for the coproduct is

|X+Y|(z)=|X|(z)+|Y|(z) {|X + Y|}(z) = {|X|}(z) + {|Y|}(z)

Hadamard product

The Hadamard product of species is

X,Y : X× FinSetYFinSet X,Y : (x,y,p)f(x) \array{ \langle X, Y \rangle &:& X \times_{FinSet} Y \to FinSet \\ \langle X, Y \rangle &:& (x, y, p) \mapsto f(x) }

which for stuff types is equal to

A:FinSet(Φ(A)×Ψ(A)) \array{ \sum_{A : FinSet} (\Phi(A) \times \Psi(A)) }

The generating functions are related by

|X,Y|(z)= n=0 n!X nY nz n {|\langle X, Y \rangle|}(z) = \sum_{n=0}^{\infty} n! X_{n} Y_{n} z^{n}

where X nX_{n} and Y nY_{n} are the nnth coefficients of the functions |X|(z){|X|}(z) and |Y|(z){|Y|}(z), respectively.

The name “Hadamard product” is used in (Aguiar-Mahajan10) and (Bergeron-Labelle-Leroux08). In (Baez-Dolan01) it is called the “inner product” of stuff types, because equipping the category of stuff types with this operation makes it a categorified version of the Hilbert space of a quantum harmonic oscillator.

Cauchy product


The Cauchy product of species is given by sending two species f,gf,g as in def. 1 to the species given by

(fg) : X×YFinSet (fg) : (x,y)f(x)+g(y) \array{ (f \cdot g) &:& X \times Y \to FinSet \\ (f \cdot g) &:& (x, y) \mapsto f(x) + g(y) }

The Cauchy product, def. 4, is eqivalently the phased tensor product on the slice over the symmetric monoidal groupoid (FinSet,)(FinSet, \coprod).


For stuff types Φ\Phi, Ψ\Psi, their Cauchy product, def. 4, is equal to

A,U,V:FinSet p:U+V=A(Φ(U)×Ψ(V)) \sum_{A, U, V : FinSet} \sum_{p : U + V = A} (\Phi(U) \times \Psi(V))

In this form the Cauchy product is discussed in (Aguiar-Mahajan 10, def. 8.5, Aguiar-Mahajan 12, section 2.2). Monoids and comonoid in the resulting monoidal category of species are discussed in (Aguiar-Mahajan 10, section 8.2) and Hopf monoids in this category in (Aguiar-Mahajan 12, section 2.2).

This means that ΦΨ\Phi\Psi stuff on a finite set is the stuff of “being chopped in two, with Φ\Phi stuff on one part and Ψ\Psi stuff on the other”.

The generating function is

|XY|(z)=|X|(z)|Y|(z). {|X \cdot Y|}(z) = {|X|}(z) \cdot {|Y|}(z) \,.


The composition of two species is

(f˜g) : ( x:X(Fin(card(f(x))Y))FinSet (f˜g) : (x,P,p) i=1 card(f(x))g(P(i)) \array{ (f \tilde{\circ} g) &:& \bigg(\sum_{x:X}(Fin(card(f(x)) \to Y)\bigg) \to FinSet \\ (f \tilde{\circ} g) &:& (x, P, p) \mapsto \bigoplus_{i=1}^{card(f(x))}g(P(i)) }

where i=1 ng(P(i))\bigoplus_{i=1}^{n}g(P(i)) is the nn-ary direct sum of the finite sets g(P(i))g(P(i)). For stuff types, this amounts to

(A,C:FinSet) (B:Fin(card(C))FinSet)((B card(C)A)×Φ(C)× k:Fin(card(C))Ψ(B(k))) \sum_{(A, C : FinSet)}\sum_{(B : Fin(card(C)) \to FinSet)} \bigg( (B\vdash_{card(C)}A) \times \Phi(C) \times \prod_{k : Fin(card(C))} \Psi(B(k)) \bigg)

That is, Φ˜Ψ\Phi \tilde{\circ} \Psi stuff on a finite set is a partition of the set into card(C)card(C) subsets, with Φ\Phi stuff on the partition and Ψ\Psi stuff on each of the subsets.

The generating function of the composition is

|X˜Y|(z)=|X|(|Y|(z)) {|X \tilde{\circ} Y|}(z) = {|X|}({|Y|}(z))

This species is also called the plethysm product.



Under groupoid cardinality

||:Grpd tame {|-|} : \infty Grpd_{tame} \to \mathbb{R}

every (tame) ∞-groupoid is mapped to a real number

X|X|:= [x]π 0(X) i=1 (π i(X,x) (1) i). X \mapsto {|X|} := \sum_{[x] \in \pi_0(X)}\prod_{i = 1}^{\infty} (\pi_i(X,x)^{(-1)^{i}}) \,.

A species X\mathbf{X} assigns an ∞-groupoid X n\mathbf{X}_n to each natural number nn \in \mathbb{Z}. Therefore under groupoid cardinality we may naturally think of a tame species as mapping to a power series

X|X|:= n=0 1n!|X n|z n[[z]]. \mathbf{X} \mapsto {|\mathbf{X}|} := \sum_{n = 0}^{\infty} \frac{1}{n!} {|\mathbf{X}_n|} z^n \in \mathbb{R}[ [ z ] ] \,.

This cardinality operation maps the above addition and multiplication of combinatorial species to addition and multiplication of power series.

That coproduct of species maps to sum of their cardinalities is trivial. That Day convolution of species maps under cardinality to the product of their cardinality series depends a little bit more subtly on the combinatorial prefactors:

|AB|=|A||B|= n=0 1n! k+l=nn!k!l!|A k||B l|. {| A \otimes B |} = {|A|} \cdot {|B|} = \sum_{n=0}^\infty \frac{1}{n!} \sum_{k+l = n} \frac{n!}{k! l!} {|A_k|} \cdot {|B_l|} \,.


  • If in the definition of combinatorial species the domain core(FinSet) is replaced with FinVect and also the presheaves are take with values in FinVect then one obtains the notion of Schur functor.

  • Instead of core(FinSet)core(FinSet), we may choose as domain BA\mathbf{B} A for a small category AA, with objects a i iI\langle a_i \rangle_{i \in I}, for II in core(FinSet)core(FinSet), i.e., finite families of objects of AA. Also, instead of SetSet valued presheaves, we may consider those valued in presheaves on a small category BB. This joint generalisation yields what are called generalised species. These generalised species can be collected in a cartesian closed 2-category (FGHW).


The notion of species goes back to

An expositional discussion can be found at

  • Todd Trimble, Exponential Generating Function and Introduction to Species (blog) (scroll down a bit).

See also wikipedia: combinatorial species and

An application in computer science:

  • Brent Yorgey, Random testing and beyond! with combinatorial species, slides pdf; Species and functors and types, oh my, article, pdf

Formalization in homotopy type theory:

An application in statistical mechanics:

  • W. Faris, Combinatorial species and cluster expansions, Mosc. Math. J. 10:4 (2010), 713–727 pdf, MR2791054

Discussion in relation to 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)

Discussion of generalised species:

  • M. Fiore, N. Gambino, M. Hyland, G. Winskel, The cartesian closed bicategory of generalised species of structures, (pdf)

Revised on July 25, 2016 03:35:05 by Urs Schreiber (