Category theory has been tightly connected to abstract mathematics since the first paper on cohomology by Eilenberg and Mac Lane [EML45] which establishes its basic notions. This appendix is a reminder of a few elementary definitions and results in this branch of mathematics. We refer to [ML71, AL91] for adequate introductions and wider perspectives.

In mathematical practice, category theory is helpful in formalizing a problem, as it is a good habit to ask in which category we are working in, if a certain transformation is a functor, if a given subcategory is reflective, etc. Using category theoretical terminology, one can often express a result in a more modular and abstract way. A list of ‘prescriptions’ for the use of category theory in computer science can be found in [Gog91].

Categorical logic is a branch of category theory that arises from the observation due to Lawvere that logical connectives can be suitably expressed by means of universal properties. In this way one represents the models of, say, intuitionistic propositional logic, as categories with certain closure properties where sentences are interpreted as objects and proofs as morphisms (cf. section 4.3).

The tools developed in categorical logic begin to play a central role in the study of programming languages. A link between these two apparently distant topics is suggested by:

• The role of (typed) λ-calculi in the work of Landin, McCarthy, Strachey, and Scott on the foundations of programming languages.

• […]