Peter LeFanu Lumsdaine: Computads, cell complexes, and theories
Time: Wed 2017-03-15 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Participating: Peter LeFanu Lumsdaine (SU)
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.