Peter LeFanu Lumsdaine: Computads, cell complexes, and theories

ABSTRACT: What does it mean for an object to be *freely generated* or *presented*?

We all learn one answer in our first category theory course: free objects are the values of a left adjoint functor.  Life, however, is not always quite so simple; there are many kinds of “free presentation” which this does not suffice to describe.  *Computads* and *cell complexes* are two more elaborate ways of freely generating/presenting an object, in settings where the specification of later generators may refer to the structure presented by earlier ones — e.g. specifying the boundary along which to glue on a new cell.

Similar issues arise with defining *theories* in more sophisticated logical settings.  For instance, in the essentially-algebraic theory of a category, the domain of the composition operation refers to the source and target operations.  Finally, the issue occurs most thornily in specifying the rules of a complex type theory.