(Post by Brent Yorgey)

My dissertation was on the topic of combinatorial species, and specifically on the idea of using species as a foundation for thinking about generalized notions of algebraic data types. (Species are sort of dual to containers; I think both have intereseting and complementary things to offer in this space.) I didn’t really end up getting very far into practicalities, instead getting sucked into a bunch of more foundational issues.

To use species as a basis for computational things, I wanted to first “port” the definition from traditional, set-theory-based, classical mathematics into a constructive type theory. HoTT came along at just the right time, and seems to provide exactly the right framework for thinking about a constructive encoding of combinatorial species.

For those who are familiar with HoTT, this post will contain nothing all that new. But I hope it can serve as a nice example of an “application” of HoTT. (At least, it’s more applied than research in HoTT itself.)

# Combinatorial Species

Traditionally, a species is defined as a functor *i.e.* lists) maps the finite set of labels

# Constructive Finiteness

So what happens when we try to define species inside a constructive type theory? The crucial piece is *finite* set, since the notion of finiteness is nontrivial in a constructive setting.

One might well ask why we even care about finiteness in the first place. Why not just use the groupoid of *all* sets and bijections? To be honest, I have asked myself this question many times, and I still don’t feel as though I have an entirely satisfactory answer. But what it seems to come down to is the fact that species can be seen as a categorification of generating functions. Generating functions over the semiring *finite* sets. Finite label sets are also important insofar as our goal is to actually use species as a basis for *computation*. In a computational setting, one often wants to be able to do things like enumerate all labels (*e.g.* in order to iterate through them, to do something like a map or fold). It will therefore be important that our encoding of finiteness actually has some computational content that we can use to enumerate labels.

Our first attempt might be to say that a finite set will be encoded as a type

However, this is unsatisfactory, since defining a suitable notion of bijections/isomorphisms between such finite sets is tricky. Since *i.e.* paths) as morphisms—but this does not work with the above definition of finite sets. In *one* path between them—intuitively, this is because paths between *particular* relation to

So elements of the above type are not just finite sets, they are finite sets *with a total order*, and paths between them must be order-preserving; this is too restrictive. (However, this type is not without interest, and can be used to build a counterpart to L-species. In fact, I think this is exactly the right setting in which to understand the relationship between species and L-species, and more generally the difference between isomorphism and *equipotence* of species; there is more on this in my dissertation.)

# Truncation to the Rescue

We can fix things using propositional truncation. In particular, we define

That is, a “finite set” is a type *hidden* evidence that

- First, we can pull the size
out of the propositional truncation, that is, . Intuitively, this is because if a set is finite, there is only one possible size it can have, so the evidence that it has that size is actually a mere proposition. - More generally, I mentioned previously that we sometimes want to use the computational evidence for the finiteness of a set of labels,
*e.g.*enumerating the labels in order to do things like maps and folds. It may seem at first glance that we cannot do this, since the computational evidence is now hidden inside a propositional truncation. But actually, things are exactly the way they should be: the point is that we can use the bijection hidden in the propositional truncation*as long as the result does not depend on the particular bijection we find there*. For example, we cannot write a function which returns the value of typecorresponding to , since this reveals something about the underlying bijection; but we can write a function which finds the smallest value of (with respect to some linear ordering), by iterating through all the values of and taking the minimum. - It is not hard to show that if
, then is a set ( *i.e.*a 0-type) with decidable equality, sinceis equivalent to the 0-type . Likewise, itself is a 1-type. - Finally, note that paths between inhabitants of
now do exactly what we want: a path is really just a path between 0-types, that is, a bijection, since trivially.

# Constructive Species

We can now define species in HoTT as functions of type *i.e.* a pair of mappings satisfying such-and-such properties”. When constructing a particular species one must explicitly demonstrate the functoriality properties; since the mappings are just functions on sets, it is quite possible to write down mappings which are not functorial. But in HoTT, all functions are functorial with respect to paths, and we are using paths to represent the morphisms in

Here’s another nice thing about the theory of species in HoTT. In HoTT, coends whose index category are groupoids are just plain *quotient* of the corresponding

There’s lots more in my dissertation, of course, but these are a few of the key ideas specifically relating species and HoTT. I am far from being an expert on either, but am happy to entertain comments, questions, etc. I can also point you to the right section of my dissertation if you’re interested in more detail about anything I mentioned above.