Adjunctions

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.