A BRICS Mini-Course
March 4, 11 and 18, 1998
Anthony J. Power
LFCS (Laboratory for Foundations of Computer Science), University of Edinburgh, Scotland, UK
We introduce the notion of 2-category and outline the basic theory of 2-categories. The notion of 2-category arises in the study of programming languages as follows. Given an idealised programming language, its types and constructors generate a category with structure. Its models are given by structure preserving functors from that generic structured category to any other category possessing such structure. The collection of all such structured categories and functors between them form a 2-category, and properties of such 2-categories support programming constructs, for instance making precise the idea of the language generated by syntax.
We study adjunctions within a 2-category, pasting composition, adjunctions between 2-categories, and the various notions of limit in a 2-category. We also give coherence results that allow one to make simplifying assumptions about the various structures, which can otherwise be very complicated. This is all illustrated by a selection of examples arising from programming languages.