Universal properties galore have arisen in the earlier chapters, and it is high time we gave a unified framework for them. In 1948 Pierre Samuel identified universal properties as a common formulation of several constructions in topology, and the Bourbaki school used them in their comprehensive account of mathematics. Independently, Daniel Kan introduced adjoint pairs of functors, with the tensor product and internal hom for vector spaces as his main example (1958). The name was suggested by Sammy Eilenberg, by analogy with Ta,b = a,T*b for operators in a Hilbert space, which notation had itself been proposed by Marshall Stone.
Nowadays, every user of category theory agrees that this is the concept which justifies the fundamental position of the subject in mathematics.
There are several other formulations (such as ends and Kan extensions), and which of them to use is a matter of personal taste. The symmetrical presentation of a pair of adjoint functors between two categories will be given in Section 7.2, but this raises logical questions because of the choice of a particular product or whatever within its isomorphism class. We prefer diagrammatic reasoning, which opens the calculations out to view, especially in complicated situations, and avoids the Choice. We shall also show that the naturality conditions on adjoint functors - all too easily dismissed as bureaucracy - are directly related to substitution- and continuation-invariance of the rules of type theory.
The most commonly used universal constructions are limits and colimits. We devote Sections 7.3-7.5 to them and to how they relate to other adjunctions, using the fact that left adjoints preserve colimits to fashion each from the other. Limits and colimits of topological spaces have an almost completely ``soft'' construction, and we also investigate free algebras, leading into the theory of monads (Section 7.5).
Often the thing which is required is obtained as a composite of two universal constructions: recognising it as such makes the development more modular. Sometimes the construction can only be done in a few simple cases, others being too complicated to be judged reliable. When it becomes apparent that it is an adjoint - frequently to something completely trivial, for example pullback between slices is right adjoint to composition - the general case quickly falls into line (Exercise 7.42).
Finally we return to the task of showing the equivalence between syntax and semantics. Adjunctions not only describe the logical connectives themselves, but also characterise the category Cn[]L of contexts and substitutions. Equivalences, in their strong form themselves examples of adjunctions, settle the issue of the choice of the structure (Section 7.6). Finally, Section 7.7 proves some deep results about syntax using just adjunctions and pullbacks.