(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.)
Traditionally, a species is defined as a functor
So what happens when we try to define species inside a constructive type theory? The crucial piece is
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
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
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
- 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 type
corresponding 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, since is 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.
We can now define species in HoTT as functions of type
Here’s another nice thing about the theory of species in HoTT. In HoTT, coends whose index category are groupoids are just plain
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.