species.tex

%  vim: set spell :
\documentclass[fleqn]{article}

\usepackage{acro}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{enumerate}
\usepackage[margin=1in]{geometry}
\usepackage{mathtools}
\usepackage{natbib}
\usepackage{siunitx}
\usepackage{graphicx}
\usepackage{slashbox}
\usepackage{listings}
\usepackage{xspace}
\usepackage[all]{xy}
\usepackage{tikz-cd}

% Typeface
\usepackage{tgpagella}
\usepackage[T1]{fontenc}
\usepackage{mathpazo}
\linespread{1.05}

\include{macros}

\usepackage{color}
\definecolor{my-blue}{RGB}{1,49,94}
\usepackage{hyperref}
\hypersetup{
  colorlinks=true,
  citecolor=my-blue,
  linkcolor=my-blue,
}

\DeclareAcronym{HoTT}{ short = HoTT, long = homotopy type theory }
\defcitealias{UFP2013}{UFP, 2013}

\newcommand{\card}{\mathsf{card}}
\newcommand{\gf}[1]{\abs{#1}\!(z)}
\newcommand{\fin}{\mathsf{Fin}}
\newcommand{\finset}{\mathsf{FinSet}}
\newcommand{\isfinset}{\mathsf{isFinSet}}
\newcommand{\isfinseq}{\mathsf{isFinSeq}}
\newcommand{\abs}[1]{\left\lvert #1 \right\rvert}
\newcommand{\Aut}{\mathrm{Aut}}
\newcommand{\sslash}{/\!\!/}
\newcommand{\inner}[2]{\langle #1, #2 \rangle}
\DeclareMathOperator{\SINH}{SINH}
\DeclareMathOperator{\COSH}{COSH}

\theoremstyle{theorem}
\newtheorem{thm}{Theorem}

\theoremstyle{definition}
\newtheorem{claim}{Claim}[section]
\newtheorem{defn}{Definition}[section]
\newtheorem{remark}{Remark}[section]
\newtheorem{example}{Example}[section]

\title{Species in HoTT}
\author{John Dougherty}
\begin{document}
\maketitle

\begin{abstract}
Combinatorial species were developed by \citet{Joyal1981} as an abstract
treatment of enumerative combinatorics, especially problems of counting the
number of ways of putting some structure on a finite set.  Many of the results
of species theory are special cases of more general properties of
homotopy types, making \ac{HoTT} a useful tool for dealing with species.  These tools become even more apposite when one generalizes
species to higher groupoids, as \citet{Baez2001} do.
What follows are notes I wrote while learning about species.  They're mainly
summary of the notes Derek Wise took during John Baez's ``Quantization and
Categorification'' seminar in AY2004~\citep{Baez2003,Baez2004a,Baez2004b}, with
some reference to \citet{Bergeron2013}, \citet{Baez2001}, and
\citet{Aguiar2010}.
\end{abstract}


\section{Defining species}

As originally defined by \citet{Joyal1981}, a species is an endofunctor of the
groupoid $\finset$ of finite sets and bijections between them.
\citet{Baez2001} generalized species to stuff types, which are functors $F : X
\to \finset$ for any groupoid $X$.  This formulation admits a natural
generalization to $\infty$-species, or homotopical species, by replacing the
groupoid $X$ with an $\infty$-groupoid---in other words, by working with
homotopy types.  So we can formulate species in \ac{HoTT} as follows.

\begin{defn}
  The canonical finite type with $n$ elements is defined by induction on
  $\mathbb{N}$ by
  \begin{align*}
    \fin(0) &\defeq \emptyt \\
    \fin(\suc(n)) &\defeq \fin(n) + \unit
  \end{align*}
\end{defn}
\begin{defn}
  The type of finite sets is
  \[
    \finset \defeq
    \sm{A : \UU}{n : \mathbb{N}} \merely{A = \fin(n)}
  \]
\end{defn}
\begin{defn}
  A species is a type $X : \UU$ equipped with a function $f : X \to \finset$.
\end{defn}

The definition of $\fin$ won't be unfolded, so you can use your favorite.  Its
role is to provide a standard set with $n$ elements, allowing us to define a
predicate $\isfinset$ such that $\finset \defeq \{A : \UU \mid \isfinset(A)\}$.
Since $\isfinset$ is a family of mere propositions, we'll often ignore it and
abusively write $A$ for both a term of type $\finset$ and its first component,
which is of type $\UU$, eliding reference to the inhabitant of $\isfinset(A)$.

Now, the intended interpretation of a species $f : X \to \finset$ is that for
some finite set $A$, an element of $\hfib{f}{A}$ is a way of equipping $A$ with
``$f$-stuff''.  This gives us a natural way to come up with examples of
species.  For some type family $\Phi : \finset \to \UU$, there is a
corresponding species $\fst : \sm{A : \finset}\Phi(A) \to \finset$.  By Lemma
4.8.2 of the \ac{HoTT} Book \citepalias{UFP2013}, any species is equal to one
of this form.  So we can specify a species up to equality by giving a family
$\Phi : \finset \to \UU$ and taking the first projection to be the map.

All of this is just setup for the main application of species: generating
functions.  Given a species $X$, we want to cook up a formal power series
\[
  \gf{X}
  =
  \sum_{n\geq0} X_{n}\, z^{n}
\]
where $X_{n} : [0, \infty)$.  Intuitively, $X_{n}$ should represent the
``number of ways of putting $X$ stuff on an $n$-element set''.  For a species
$f : X \to \finset$, this description picks out something like the cardinality
of $\hfib{f}{A}$, where $A$ is an $n$-element set.  There are two problems with
this: (i) we need a notion of cardinality, and (ii) we need some way to pick an
$A$ from all of the $n$-element sets.  To solve the first problem we use
groupoid cardinality $\abs{X}$ of $X$.

\begin{defn}
  For any $X : \UU$, if $\merely{X = \fin(n)}$ for some $n : \mathbb{N}$, then
  $\abs{X} = n$.
\end{defn}

\begin{defn}
  The groupoid cardinality $\abs{X}$ of a type $X$ is, if it converges, the sum
  \[
    \abs{X} 
    = \sum_{[x] \in \pi_{0}(X)}\prod_{k\geq1} 
        \abs{\pi_{k}(X, x)}^{(-1)^{k}}
    = \sum_{[x] \in \pi_{0}(X)}
        \frac{1}{\abs{\pi_{1}(X, x)}}\abs{\pi_{2}(X, x)}
        \frac{1}{\abs{\pi_{3}(X, x)}}\abs{\pi_{4}(X, x)}
        \dotsm
  \]
\end{defn}

\noindent
Via the homotopy hypothesis, this is equivalently the Euler characteristic of
a topological space presenting the type $X$.

This solves the problem of finding some notion of cardinality.  To solve
problem (ii), we avoid an arbitrary choice of $A$ by decategorifying and
regarding $f : X \to \finset$ as a fibration over $\mathbb{N}$, rather than
$\finset$.  Specifically, we consider the sequence
\[ \begin{tikzcd}
    X \ar[r, "f"] & 
    \finset \ar[r, "\tproj{0}{\blank}"] \ar[rr, bend right, "\card"] &
    \trunc{0}{\finset} \ar[r, "\mathsf{ext}(\card)"] &
    \mathbb{N}
\end{tikzcd}  \]
where $\card \defeq \fst \circ \snd$, given our definition of $\finset$, and
$\mathsf{ext}$ is the extension along $\tproj{0}{\blank}$, the $0$-truncation
map.  The reason this counts as decategorification is that we're squashing
$\finset$ into a set, meaning that we're identifying all of the equinumerous
sets.  This produces a type $\eqv{\trunc{0}{\finset}}{\mathbb{N}}$.  So,
finally, we have the
\begin{defn}
  The generating function $\gf{X}$ of a species $f : X \to \finset$ is given by
  \[
    \gf{X}
    =
    \sum_{n\geq0}
    \abs{\hfib{\card \circ f}{n}}\,
    z^{n}
    =
    \sum_{n\geq0}
    X_{n}\, z^{n}
  \]
  where this expression defines $X_{n}$.
\end{defn}
\noindent
We'll variously write $\gf{f}$, $\gf{X}$, or $\gf{\Phi}$, as appropriate, for
species $f : X \to \finset$ or $\Phi : \finset \to \UU$.


\section{Computing cardinalities}

There are two kinds of results that simplify the computation of generating
functions.  First, one can compute the cardinality of composite types in terms
of the cardinalities of their components.  Second, the definition of the
generating function can be simplified to eliminate reference to $\card$.  I'm
going to be a bit sloppy about the scope of this section's discussion.
Everything works for essentially finite 1-types, which are going to be the ones
I'm mainly dealing with.

Four properties of the groupoid cardinality follow from the definition above.
In fact, these four axiomatically characterize the groupoid cardinality:

\begin{claim}
  $\abs{\unit} = 1$. 
\end{claim}

\begin{claim}
  If $\merely{\eqv{X}{Y}}$, then $\abs{X} = \abs{Y}$.
\end{claim}

\begin{claim}\label{claim:gc_sum}
  $\abs{X + Y} = \abs{X} + \abs{Y}$
\end{claim}

\begin{claim}\label{claim:gc_fibration}
  If there is a map $f : X \to Y$ and $\lvert{\hfib{f}{y}}\rvert =
  \lvert{\hfib{f}{y'}}\rvert$
  for all $y, y' : Y$, then $\abs{X} = \lvert\hfib{f}{y}\rvert \cdot \abs{Y}$
  for any $y : Y$.
\end{claim}

\noindent
The first three of these are immediate.  The fourth follows from the homotopy
hypothesis.  If $p : A \to B$ is a fibration with fiber $F$ and $B$ is
path-connected, then the Euler characteristic $\chi(E)$ of $E$ is equal to
$\chi(F) \cdot \chi(B)$.  Since any function is equivalent to a fibration, for
any two points $y, y'$ connected by a path we have $\hfib{f}{y} \eqvsym
\hfib{f}{y'}$, translating this result into groupoid-speak and then into
\ac{HoTT}, then summing over the connected components gives
Claim~\ref{claim:gc_fibration}.

Similar properties for $\Sigma$-types and products follow from these axioms.
For $\Sigma$-types we have the
\begin{claim}
  For any type $X$ and family $P : X \to \UU$, if $\abs{P(x)} = \abs{P(x')}$
  for all $x, x' : X$ then
  \[
    \abs{\sm{y:X}P(y)}
    =
    \abs{P(x)} \cdot \abs{X}
  \]
  for any $x : X$.
\end{claim}
\noindent
This is a combination of the sum and fibration claims \ref{claim:gc_sum} and
\ref{claim:gc_fibration}.  If $X$ is $0$-connected, then we automatically get
$\prd{x, x' : X}(\eqv{P(x)}{P(x')})$ by transport.  If, more generally, $X$ is
essentially finite, then the further hypothesis is required.  For products, we
have the following
\begin{claim}
  The cardinality of the product $X \times Y$ is
  \[
    \abs{X \times Y} = \abs{X} \cdot \abs{Y}
  \]
\end{claim}
\noindent
which follows from the definition $X \times Y \defeq \sm{x:X}Y$ and the
property for $\Sigma$-types.

Now consider the definition of the generating function of some $f : X \to
\finset$.  Note first that, because $\card(\fin(n)) \equiv n$, we can write
\[
  \abs{\hfib{\card \circ f}{n}}
  \equiv
  \abs{\hfib{\card \circ f}{\card(\fin(n))}}
  =
  \abs{\sm{w : \hfib{\card}{\card(\fin(n))}}\hfib{f}{\fst{w}}}
  =
  \abs{\sm{w : \sm{A : \UU}\merely{A = \fin(n)}}\hfib{f}{\fst{w}}}
\]
by Exercise 4.4 of the \ac{HoTT} Book.  Since the type of $w$ is 0-connected,
we can replace $\fst(w)$ with $\fin(n)$:
\[
  X_{n} =
  \abs{\sm{w : \sm{A : \UU}\merely{A = \fin(n)}}\hfib{f}{\fin(n)}}
\]
so we can always calculate $X_{n}$ using the fiber of $f$ over $\fin(n)$.

This expression can be simplified further by considering the type $\sm{A :
  \UU}\merely{A = \fin(n)}$.  This is our representative of the type of
$n$-element sets, but it has a number of other descriptions.  In particular, it
is the delooping of the automorphism group of $\fin(n)$.  We have the following
definitions:
\begin{defn}
  The automorphism group of the type $X : \UU$ is $\Aut(X) \defeq (X = X)$.
\end{defn}
\begin{defn}
  The delooping of an automorphism group $\Aut(X)$ is
  \[
    B\Aut(X) \defeq \sm{A : \UU} \merely{A = X}
  \]
\end{defn}
\begin{defn}
  The action groupoid for the action of $\Aut(X)$ on itself is
  \[
    E\Aut(X) \defeq \sm{w : B\Aut(X)} (\fst(w) = X)
  \]
  Giving the canonical fibration
  \[
    \fst : E\Aut(X) \to B\Aut(X)
  \]
\end{defn}
By Theorem 7.3.9 of the \ac{HoTT} book, $B\Aut(C)$ is $0$-connected, so we can
write
\[
  X_{n} = \abs{B\Aut(\fin(n))} \cdot \abs{\hfib{f}{\fin(n)}}
\]
which can be further simplified by computing $B\Aut(\fin(n))$ once and for all.
Note that $E\Aut(X)$ is contractible for all $X$, since it's a type of based
paths, so we have
\[
 1
 = \abs{E\Aut(X)}
 = \abs{B\Aut(X)} \cdot \abs{\Aut(X)}
\]
reducing our problem to computing $\abs{\Aut(\fin(n))}$, the number of
permutations of an $n$-element set.  This is $n!$, so, finally,
\[
  X_{n} = \frac{1}{n!} \abs{\hfib{f}{\fin(n)}}
\]
This suggests the notation $1 \sslash n! \defeq B\Aut(\fin(n))$, which I will
sometimes use in the following.

Plugging this back into the definition of $\gf{X}$, we have
\[
  \gf{X} = \sum_{n\geq0} \abs{\hfib{f}{\fin(n)}}\, \frac{z^{n}}{n!}
\]
So, we could have defined $\gf{X}$ as an exponential generating function,
without first thinking of $X$ as a fibration over $\mathbb{N}$.  Doing it our
way is informative, however.  A common rule of thumb is that one should use
exponential generating functions when working with labeled structures and
ordinary generating functions when working with unlabeled structures.  In
our setup, a labeling of some $A : \finset$ is a path $A = \fin(\card(A))$.  In
other words, we replace the type of finite sets with the type of labeled finite
sets:
\[
  \sm{A : \UU}{n: \mathbb{N}} \merely{A = \fin(n)}
  \qquad\Longrightarrow\qquad
  \sm{A : \UU}{n : \mathbb{N}} (A = \fin(n))
\]
and then proceed as before.  Equivalently, we could write our species as a
fibration $\sm{A:\finset}\Phi(A)$ for some $\Phi : \finset \to \UU$ and then
work with the altered species $\Phi(A) \times (A = \fin(\card(A))$.  So
``labeled $\Phi$-stuff on a finite set'' is the same as ``$\Phi$-stuff on a
finite set and a labeling of the set''.  The cardinality of the $n$th fiber is
then
\[
  \frac{1}{n!}
  \abs{
    \Phi(\fin(n)) \times (\fin(n) = \fin(n))
  }
  =
  \abs{\Phi(\fin(n))}
\]
as the $\abs{\Aut(\fin(n))}$ cancels out the $1/n!$.  The idea, then, is that a
species generating function gives an exponential generating function when one
computes out the dependence on $\card$, and then a labeling turns it into an
ordinary generating function.

Another reason to define $\gf{X}$ as we do is that it allows the labeled and
unlabeled cases to be treated at once.  Working directly with the reduced
generating functions requires one to insert various factorials by hand to make
some equations hold, and similar bookkeeping is needed for working with labeled
and unlabeled structures differently.  Taking the $n$th generating function
coefficient to be the groupoid cardinality of the fiber over $n$ allows us to
define each operation on a species once, and the modifications required for
labels take care of themselves.


\section{Speciation}

One power of the species approach is that it allows one to combine structures
in a natural way.  As an example in the previous section, we took a structure
type $\Phi : \finset \to \UU$ and created a labeled version $\Phi(A) \times (A
= \fin(\card(A)))$, naturally read as ``the species of finite sets equipped
with $\Phi$-stuff and a labeling'', using the propositions-as-types
interpretation.  The other type formers allow for similar combinations.

Throughout this section, we suppose that $f : X \to \finset$ and $g : Y \to
\finset$ are two species, and that $\Phi, \Psi : \finset \to \UU$ are two
families of stuff on $\finset$.


\subsection{Coproduct}

The simplest example is the coproduct.  The recursion principle for the
coproduct gives us a species with type $X + Y \to \finset$.
\begin{defn}
  The coproduct species $(f + g) : X + Y \to \finset$ is given by
  \begin{align*}
    (f + g) &: X + Y \to \finset \\
    (f + g) &\defeq \rec{X+Y}(\finset, f, g)
  \end{align*}
\end{defn}
\noindent
For structure types $\Phi, \Psi : \finset \to \UU$, we have
\[
  \left(\sm{A : \finset}\Phi(A)\right) + \left(\sm{B : \finset}\Psi(B)\right)
  \eqvsym
  \sm{A : \finset}\left(\Phi(A) + \Psi(A)\right)
\]
and so we can think of the species $X + Y$ as ``the species of finite sets
equipped with $X$-stuff or $Y$ stuff'', though ``or'' here is un-truncated.

The generating function $\gf{X + Y}$ can be simply expressed in terms of
$\gf{X}$ and $\gf{Y}$.  We have
\begin{align*}
  (X+Y)_{n}
  &=
  \frac{1}{n!}\abs{\hfib{f+g}{\fin(n)}}
  \\&=
  \frac{1}{n!}\abs{
    \sm{x:X}(f(x) = \fin(n))
    +
    \sm{y:Y}(g(y) = \fin(n))
  }
  \\&=
  \frac{1}{n!}\abs{
    \hfib{f}{n} + \hfib{g}{n}
  }
  \\&=
  X_{n} + Y_{n}
\end{align*}
since $\abs{X + Y} = \abs{X} + \abs{Y}$ for all groupoids $X$ and $Y$.  So, the
generating function $\gf{X+Y}$ is the sum of the generating functions $\gf{X}
+ \gf{Y}$.

\subsection{Hadamard product}
We can tell a similar story with $\times$ instead of $+$.  Where $X + Y$ is
the species of ``$X$ stuff or $Y$ stuff on a finite set'', the product should
give ``$X$ stuff and $Y$ stuff on a finite set''.  But this is ambiguous: there are two ways to put
two kinds of stuff on a finite set.  The problem, essentially, is that while
the recursion principle for the coproduct takes two species and gives a new
one, the recursion principle for the product needs something of type $X \to Y
\to \finset$ to produce a species.  The two kinds of products on species
correspond to different ways of doing this.

One way is to ``superpose'' the
$X$ stuff and $Y$ stuff.  That is, we might take the fiber over $\fin(n)$ to be
\begin{align*}
  \hfib{f}{\fin(n)} \times \hfib{g}{\fin(n)}
  &\equiv
  \left(\sm{x : X}(f(x) = \fin(n))\right)
  \times
  \left(\sm{y : Y}(g(y) = \fin(n))\right)
  \\&\eqvsym
  \sm{x : X}{y : Y}\left(
    (f(x) = g(y))
    \times
    (f(x) = \fin(n))
  \right)
  \\&\eqvsym
  \sm{z : X \times_{\finset} Y} (f(\fst(z)) = \fin(n))
  \\&\equiv
  \hfib{\langle f, g \rangle}{\fin(n)}
\end{align*}
This leads us to
\begin{defn}
  The Hadamard product species $\langle f, g \rangle : X \times_{\finset} Y \to
  \finset$ is given by
  \begin{align*}
    \langle f, g \rangle &: X \times_{\finset} Y \to
    \finset \\
    \langle f, g \rangle &: (x, y, p) \mapsto f(x) 
  \end{align*}
\end{defn}
\noindent
For our structure types, we have
\[
  \left(\sm{A:\finset}\Phi(A)\right)
  \times_{\finset}
  \left(\sm{B:\finset}\Psi(B)\right)
  \eqvsym
  \sm{A:\finset}(\Phi(A) \times \Psi(A))
\]
which is naturally understood as ``a finite set equipped with $\Phi$ stuff on
top of $\Psi$ stuff'', as we wanted.

The generating function for the Hadamard product is
\begin{align*}
  (X \times_{\finset} Y)_{n}
  &=
  \frac{1}{n!}\abs{\hfib{\langle f, g \rangle}{\fin(n)}}
  =
  \frac{1}{n!}\abs{\hfib{f}{\fin(n)}} \cdot \abs{\hfib{g}{\fin(n)}}
  =
  n! X_{n} \cdot Y_{n}
\end{align*}
This formula motivates another name for this species: the inner product.  When
the ring of formal power series is treated as Fock space, the Hadamard product
of two formal power series gives the inner product on Fock space.  The
relationship between the generating functions themselves is messy.

\subsection{Cauchy product}
A more natural relationship between generating functions would be some species
$X \cdot Y$ such that
\[
  \gf{X \cdot Y}
  =
  \gf{X} \cdot \gf{Y}
  =
  \left(\sum_{n\geq0} X_{n} z^{n}\right)
  \left(\sum_{m\geq0} Y_{m} z^{m}\right)
  =
  \sum_{n\geq0}
  \left(
    \sum_{k=0}^{n} X_{k}Y_{n-k}
  \right) z^{n} 
\]
For this to obtain, we should have
\begin{align*}
  \abs{\hfib{f \cdot g}{\fin(n)}}
  &=
  \sum_{k=0}^{n}
  \binom{n}{k}
    \abs{\hfib{f}{\fin(k)}}
    \cdot
    \abs{\hfib{g}{\fin(n-k)}}
\end{align*}
Decategorifying this expression gives the
\begin{defn}
  The Cauchy product species $(f \cdot g) : X \cdot Y \to \finset$ is
  \begin{align*}
    (f \cdot g) &: X \times Y \to \finset \\
    (f \cdot g) &: (x, y) \mapsto f(x) + g(y)
  \end{align*}
\end{defn}
\noindent
And for our structure types,
\[
  \left(\sm{A : \finset}\Phi(A)\right) 
  \cdot
  \left(\sm{B : \finset}\Psi(B)\right)
  \eqvsym
  \sm{A : \finset}\sm{U, V : \finset}{p : U + V = A} \left(
    \Phi(U) \times \Psi(V)
  \right)
\]
So, we can interpret the Cauchy product species as ``a finite set chopped in
two with $\Phi$ stuff on one part and $\Psi$ stuff on the other''.

The coefficients of the generating function are
\begin{align*}
  (X \cdot Y)_{n}
  &\equiv
  \frac{1}{n!}
  \abs{\sm{x:X}{y:Y}(f(x) + g(y) = \fin(n))}
  \\&=
  \frac{1}{n!}
  \abs{\sm{r, s : \mathbb{N}}
    \left(\sm{w : 1\sslash r!}\hfib{f}{\fin(r)}\right)
    \times 
    \left(\sm{w : 1\sslash s!}\hfib{g}{\fin(s)}\right)
    \times
    (\fin(r) + \fin(s) = \fin(n))
    }
  \\&=
  \sum_{k=0}^{n}\frac{1}{k!}\abs{\hfib{f}{\fin(k)}} 
    \cdot \frac{1}{(n-k)!}\abs{\hfib{g}{\fin(n-k)}}
  \\&\equiv
  \sum_{k=0}^{n}X_{k}Y_{n-k}
\end{align*}
and so we obtain the relation $\gf{X \cdot Y} = \gf{X} \cdot \gf{Y}$ between
the generating functions.


\subsection{Composition}
Continuing to take inspiration from nice relations between generating
functions, we look for some species $X \circ Y$ such that
\[
  \gf{X \circ Y} = \abs{X}\!(\gf{Y})
  =
  \sum_{n\geq0}\left(
    \sum_{k=0}^{n}\sum_{n_{1} + \dotsb + n_{k} = n}
    X_{k}\cdot \prod_{i=1}^{k}Y_{n_{i}}
  \right) z^{n}
\]
To categorify this equation, we replace the partition of $n$ with a partition
of the set $\fin(n)$, and we replace the product $\prod_{i}Y_{n_{i}}$ with a
dependent product type.  To do this, we first define partitions of a finite
set.
\begin{defn}
  For any $n : \mathbb{N}$ and $S : \fin(n) \to \finset$, the $\fin(n)$-indexed
  sum $\bigoplus_{i=1}^{n} S_{i}$ of the family $S$ is the type defined by
  induction on the naturals by
  \begin{alignat*}{2}
    \bigoplus_{i=1}^{0}S_{i} &\defeq \emptyt
    \qquad\qquad&
    \bigoplus_{i=1}^{\suc(n)}S_{i} &\defeq S_{n} + \bigoplus_{i=1}^{n} S_{i}
  \end{alignat*}
\end{defn}
\begin{defn}
  A partition of a finite set $A : \finset$ into $n : \mathbb{N}$ parts by a
  family $P : \fin(n) \to \finset$ is a term of type
  \[
    P \vdash_{n} A \defeq 
    \left(A = \bigoplus_{i=1}^{n} P_{i}\right)
  \]
  That is, it is a family $P : \fin(n) \to \finset$ such that $A$ is equal
  to the $\fin(n)$-indexed sum of $P$.
\end{defn}

With these, we can now define
\begin{defn}
  For species $f : X \to \finset$ and $g : Y \to \finset$, the composite
  species is given by 
  \begin{align*}
    (f \circ g) &: \left(
      \sm{x : X}(\fin(\card(f(x))) \to Y)
    \right)
    \to
    \finset
    \\
    (f \circ g) &: (x, P, p) \mapsto \bigoplus_{i=1}^{\card(f(x))}(g(P(i)))
  \end{align*}
\end{defn}
\noindent
For structure types, this gives
\begin{align*}
  &\left(\sm{A : \finset}\Phi(A)\right)
  \circ
  \left(\sm{B : \finset}\Psi(B)\right)
  \\&\eqvsym
  \sm{A : \finset}{C:\finset}
  \sm{B : \fin(\card(C)) \to \finset}
  \left(
    (B \vdash_{\card(C)} A)
    \times
    \Phi(C) 
    \times
    \prd{k : \fin(\card(C))}\Psi(B_{k})
  \right)
\end{align*}
So, the composition of the species $\Phi$ and $\Psi$ is the species of ``a
partitioned finite set, with $\Phi$ stuff on the partition and $\Psi$ stuff on
each element of the partition''.

The $n$th coefficient of the generating function is
\begin{align*}
  (X \circ Y)_{n}
  &=
  \frac{1}{n!}\abs{
    \sm{x:X}{P : \fin(\card(f(x))) \to Y}
    \left(\fin(n) = \bigoplus_{i=1}^{\card(f(x))} g(P(i))\right)
  }
  \\&=
  \abs{
    \sm{k:\mathbb{N}}
    \sm{m : \fin(k) \to \mathbb{N}}{p : m_{1} + \dotsb + m_{k} = n}
      \left(\sm{w : 1 \sslash k!}\hfib{f}{\fin(k)}\right)
    \times
      \prd{i : \fin(k)}\sm{w : 1 \sslash m_{i}!}\hfib{g}{\fin(m_{i})}
  }
  \\&=
  \sum_{k=0}^{n}\sum_{m_{1} + \dotsb + m_{k} = n}
  \frac{1}{k!}\abs{\hfib{f}{\fin(k)}} 
  \cdot 
  \prod_{i=1}^{k} 
  \frac{1}{m_{i}!}\abs{\hfib{g}{\fin(m_{i})}}
  \\&=
  \sum_{k=0}^{n}\sum_{m_{1} + \dotsb + m_{k} = n}
    X_{k} \cdot \prod_{i=1}^{k} Y_{m_{i}}
\end{align*}
And so $\gf{X \circ Y} = \abs{X}\!(\gf{Y})$.


\subsection{Differentiation}
Again, we would like to construct a species whose generating function has a
nice property.  Since
\[
  \frac{d}{dz}\sum_{n\geq0}X_{n}z^{n}
  =
  \sum_{n\geq1}n\, X_{n} z^{n-1}
  =
  \sum_{n\geq0} (n+1)X_{n+1} z^{n}
\]
we want to define a species $f' : X' \to \finset$ such that $\gf{X'} =
\frac{d}{dz}\gf{X}$.  Categorifying this equation gives the
\begin{defn}
  The derivative of a species $f : X \to \finset$ is
  \begin{align*}
    f' &: \sm{A : \finset}{x:X}(f(x) = A + \unit) \to \finset \\
    f' &: (A, x, p) \mapsto A
  \end{align*}
\end{defn}
\noindent
For structure types, we have
\[
  \left(\sm{A:\finset}\Phi(A)\right)'
  =
  \sm{A, B : \finset}\left(
    \Phi(B)
    \times
    (B = A + \unit)
  \right)
\]
So $\Phi'$ stuff on $A$ is ``$\Phi$ stuff on $A + \unit$''.

The $n$th coefficient of the generating function is
\begin{align*}
  X'_{n}
  &=
  \frac{1}{n!}\abs{
    \sm{A : \finset}{x:X} \left(
      (f(x) = A + \unit)
      \times
      (A = \fin(n))
    \right)
  }
  \\&=
  \frac{1}{n!}\abs{
    \sm{x:X} \left(
      (f(x) = \fin(n) + \unit)
    \right)
  }
  \\&=
  \frac{1}{n!}\abs{
    \hfib{f}{\fin(n + 1)}
  }
  \\&=
  (n+1) X_{n+1}
\end{align*}
giving
\begin{align*}
  \gf{X'}
  =
  \frac{d}{dz}\gf{X}
\end{align*}

\subsection{Pointing}
From generating function theory, we know that for any polynomial $P$, the
generating function of the sequence $P(n)\,X_{n}$ is given by
\[
  P(z\partial_{z})\gf{X} = \sum_{n\geq0} P(n)\, X_{n}\, z^{n}
\]
It suffices to consider the case $P(n) = n$, for which we have by
categorification the
\begin{defn}
  For any species $f : X \to \finset$, the pointing $\pointed{f} : \pointed{X}
  \to \finset$ is
  \begin{align*}
    f_{\bullet} &: \left(\sm{x:X}f(x)\right) \to \finset \\
    f_{\bullet} &: (x, w) \mapsto f(x)
  \end{align*}
\end{defn}
\noindent
For a structure type, we have
\[
  \pointed{\left(\sm{A:\finset}\Phi(A)\right)}
  \eqvsym
  \sm{A:\finset}(\Phi(A) \times A)
\]
So $\pointed{\Phi}$ stuff on $A$ is ``$\Phi$ stuff on $A$ and a distinguished
point of $A$''.

The $n$th coefficient of the generating function is
\begin{align*}
  (\pointed{X})_{n}
  &=
  \frac{1}{n!}\abs{
    \sm{x:X}{w:f(x)}(f(x)=\fin(n))
  }
  =
  \frac{1}{n!}\abs{\hfib{f}{\fin(n)}}\cdot\abs{\fin(n)}
  =
  n\, X_{n}
\end{align*}
And so $\gf{\pointed{X}} = (z\, \partial_{z})\gf{X}$.

\subsection{Inhabiting}
It's often useful to have a version of the species that only exists on
inhabited sets.  This is the easy
\begin{defn}
  For any species $f : X \to \finset$, the inhabited version of the species
  $f_{+} : X_{+} \to \finset$ is
  \begin{align*}
    f_{+} &: \left(\sm{x:X}\merely{f(x)}\right) \to \finset \\
    f_{+} &: (x, p) \mapsto f(x)
  \end{align*}
\end{defn}
\noindent
For a structure type,
\[
  \left(\sm{A \finset}\Phi(A)\right)_{+}
  \eqvsym
  \sm{A : \finset}(\Phi(A) \times \merely{A})
\]
So, as intended, $\Phi_{+}$ stuff on a set is ``being an inhabited set equipped
with $\Phi$ stuff''.

The $n$th coefficient of the generating function is
\[
  (X_{+})_{n}
  =
  \frac{1}{n!}\abs{\hfib{f}{\fin(n)}} \cdot \abs{\merely{\fin(n)}}
  =
  \begin{cases}
    0 & n = 0 \\
    X_{n} & n > 0
  \end{cases}
\]
since $\fin(n)$ is decidable and $\merely{\fin(n)}$ is a mere proposition.  So
$\gf{X_{+}} = \gf{X} - X_{0}$.


\section{Examples}
This section lists a handful of examples.  

\subsection{$(-2)$-stuff}  The simplest structure to put on a finite set is a
contractible one.  For example, we know that $\isfinset(A)$ is a mere 
proposition, and it is inhabited for all $A : \finset$, so it's contractible.
So the total space of the type is
\[
  \sm{A : \finset}\isfinset(A)
  \eqvsym
  \sm{A : \finset}\unit
  \eqvsym
  \finset
\]
So any species of contractible stuff on a finite set is equal to $\idfunc{} :
\finset \to \finset$, the species of finite sets.  Call this species $E \defeq
\idfunc{\finset}$, for the species of ensembles.
The fiber over $n$ is
\[
  \sm{A : \UU}\merely{A = \fin(n)} \equiv B\Aut(\fin(n))
\]
so the generating function of the species of ensembles is
\[
  \gf{E} = \sum_{n\geq0} \frac{z^{n}}{n!} = e^{z}
\]


\subsection{$(-1)$-stuff}  Moving up the hierarchy, a family of mere
propositions can produce more interesting examples.  Considered as an
exponential generating function, the generating function obtained from
$(-2)$-stuff has coefficients in $\{1\}$.  For $(-1)$-stuff, we can choose
coefficients from $\{0, 1\}$.  So for example, we have

\paragraph{Empty stuff}
A finite set equipped with the stuff $\Phi : A \mapsto \emptyt$ gives the
species
\[
  0 \defeq \rec{\emptyt}(\finset) : \emptyt \to \finset
\]
which has the generating function
\[
  \gf{0} = 0
\]

\paragraph{$n$-element sets}
The stuff of ``being an $n$-element set'' gives the species
\[
  (Z^{n} \sslash n!) \defeq 
  \fst : \left(
    \sm{A : \finset}(\card(A) = n)
  \right) \to \finset
\]
and it has the generating function
\[
  \gf{Z^{n} \sslash n!} = \frac{z^{n}}{n}
\]
As a special case, for $n = 0$ we have $\gf{Z^{n} \sslash n!} = 1$, so we'll
also write
\[
  1 \defeq (Z^{0} \sslash 0!)
\]


\paragraph{Inhabited finite sets}
This is the species $E_{+}$, and we clearly have
\[
  \gf{E_{+}} = \sum_{n\geq1}\frac{z^{n}}{n!} = e^{z} - 1
\]

\paragraph{Even and odd sets}
The stuff $\Phi$ of ``being an even set'' gives us the species
\[
  \mathrm{COSH} \defeq \fst :
  \left(\sm{A : \finset}{n:\mathbb{N}}\merely{A = \fin(2n)}\right)
  \to
  \finset
\]
So the fiber over $n$ is
\[
  \sm{w : 1 \sslash n!}{m:\mathbb{N}}(2m = n)
\]
giving the generating function
\[
  \gf{\mathrm{COSH}} = \sum_{\text{$n$ even}}\frac{z^{n}}{n!} = \cosh(z)
\]
Similarly, ``being an odd set'' is the species $\SINH$ with generating
function
\[
  \gf{\SINH} = \sum_{\text{$n$ odd}} \frac{z^{n}}{n!} = \sinh(z)
\]


\subsection{0-stuff}
On the next rung of the ladder we have families of sets.  Now we obtain
exponential generating functions with coefficients in $\mathbb{N}$.  For
example, 

\paragraph{Labeled $n$-element sets}
The stuff of ``being a labeled $n$-element set'' gives the species
\[
  Z^{n} \defeq \fst : \left(
    \sm{A : \finset} (A = \fin(n))
  \right) \to \finset
\]
with generating function
\[
  \gf{Z^{n}} = z^{n}
\]

\paragraph{Labeled finite sets}
This species is
\[
  \fst : \left(
    \sm{A : \finset}{n:\mathbb{N}}(A = \fin(n))
  \right) \to \finset
\]
and it has generating function
\[
  \sum_{n\geq0} z^{n} = \frac{1}{1 - z}
\]

\paragraph{Linear order}
A linear order on a set $A$ is a mere relation $\blank < \blank : A \to A \to
\prop$ that's transitive, antisymmetric, and total.  We have the species
\[
  L \defeq \fst : \left(
    \sm{A:\finset}{< : A \to A \to \prop}\left(
      \mathsf{Transitive}(<)
      \times \mathsf{Antisymmetric}(<)
      \times \mathsf{Total}(<)
    \right)
  \right)
  \to
  \finset
\]
It's not too hard to see that this species is equal to the species of labeled
finite sets; there is a natural total order on $\fin(\card(A))$, and the
elements of $A$ can be matched up with elements of $\fin(\card(A))$ by matching
the orders.  So the generating function of $L$ is also
\[
  \gf{L} = \sum_{n\geq0}z^{n} = \frac{1}{1-z}
\]

\paragraph{Permutations}
A permutation on $A$ is a bijection $\sigma : A \to A$.  Since $A$ is a set,
being a bijection is equivalent to being an equivalence, so we have by
univalence the species
\[
  \mathrm{Per} \defeq \fst : \left(
    \sm{A : \finset}(A = A)
  \right) \to \finset
\]
This has the same fiber over $n$ as the species of finite labeled sets, so we
again have
\[
  \gf{\mathrm{Per}} = \sum_{n\geq0}z^{n} = \frac{1}{1-z}
\]

\paragraph{$\finset$-coloring}
For $K$ a finite set, a $K$-coloring of $A$ is a map $\phi : A \to K$.  This gives the
species
\[
  \fst : \left(
    \sm{A : \finset}(A \to K)
  \right) \to \finset
\]
which has generating function
\[
  \gf{A \to K} = \sum_{n\geq0} \abs{K}^{n}\frac{z^{n}}{n!}
  = e^{\abs{K}z}
\]

Consider the property of being a $K$-colored, 1-element set.  This is the
species given by the stuff
\[
  \Phi(A) \defeq \merely{A = \fin(1)} \times (A \to K)
\]
which is equivalent to the species equipped with stuff
\[
  \tilde{\Phi}(A) \defeq K \times \merely{A = \fin(1)}
\]
and hence to the Cauchy product $K \cdot Z$.  Indeed, the generating function
is given by
\[
  \gf{\Phi} = \abs{K}z
\]
and so we can write $nZ$ for the species ``being a $\fin(n)$-colored 1-element
set''.  As the notation suggests,
\[
  \gf{E \circ nZ} = \abs{E}\!(\gf{nZ}) = e^{nz}
\]


\subsection{Fock space}
Consider the operators $a, a^{*} : \mathbb{C}[z] \to \mathbb{C}[z]$ defined by
\begin{align*}
  a\psi &= \psi' \\
  a^{*}\psi &= z\psi
\end{align*}
for all $\psi \in \mathbb{C}[z]$.  We equip $\mathbb{C}[z]$ with an inner
product by demanding that
\[
  \inner{a^{*}\psi}{\phi} = \inner{\psi}{a\phi}
  \qquad\qquad
  \lVert 1 \rVert = 1
\]
for all $\psi, \phi \in \mathbb{C}[z]$.  Completing $\mathbb{C}[z]$ in this
inner product gives Fock space $K[z]$.

\section{Cayley's Formula}
We recount \citeauthor{Joyal1981}'s proof of the following
\begin{thm}[Cayley's Formula] 
  The number of labeled trees on $n$ vertices is $n^{n-2}$.
\end{thm}

Recall that a tree is a connected graph such that any two edges are connected
by exactly one path.  A graph on a finite set $A$ is a mere relation $R : A
\to A \to \prop$, so we're looking at the species
\[
  T \defeq \sm{A:\finset}{R : A \to A \to \prop}\left(
      \mathsf{isTree}(R) \times (A = \fin(\card(A)))
    \right)
\]
Pointing this species twice gives a species $V \defeq T_{\bullet\bullet}$ of
vertebrates, so-called because we can think of the path connecting the two
special points as a vertebral column, with a rooted tree at each vertebra.  By
the calculation above for pointed species, we have $V_{n} = n^{2}\, T_{n}$ so
Cayley's formula follows if we can show that $V_{n} = n^{n}$.

To show this, note that $V$ is equivalent to the species $L_{+} \circ
T_{\bullet}$, which are inhabited linear orders of rooted trees.  Given a
vertebrate $v : V$, we disconnect it by forgetting the links between vertebrae,
then we induce a linear order on the connected components using the linear
order on the vertebral column.  Since $L_{n} = \mathrm{Per}_{n}$, it suffices
to consider $S_{+} \circ T_{\bullet}$, which is equal to $\mathrm{End}_{+}$.
Since $\mathrm{End}_{n} = n^{n}$, for $n > 0$ we have $V_{n} = n^{n}$, from
which follows Cayley's formula.



\bibliographystyle{apalike-url}
\pdfbookmark{References}{References}
\bibliography{references}

\end{document}