This chapter is an account of first order logic, originally motivated by the needs of homological algebra - the understanding of sets, functions and relations came later. As we said in Chapter II, products, equalisers, sums and quotients of equivalence relations provide the real foundation for algebra, rather than the powerset. The diversity of the behaviour of finite limits and colimits is striking: the basic features of groups, rings, vector spaces and topology may often be discovered just by looking for the coproducts in these categories.
Besides these traditional applications in mathematics, we also show how stable disjoint coproducts (as in Set) interpret the conditional declarative language, with if then else fi. The extension to while in Section 6.4 shows that general coequalisers in Set are much more complicated than equalisers or quotients.
As in the l-calculus, the need for the operations of logic to respect substitution must be expressed in category theory. In Chapters VIII and IX we shall show in terms of syntax that pullbacks effect substitution, but in this chapter relational algebra exhibits the same behaviour.
Limits and colimits also interact in that we can try to construct one from the other as in Theorem 3.6.9. However, size issues arise in the case of categories, where they did not for lattices, so we postpone the general result until Theorem 7.3.12 . By way of preparation we consider factorisation systems, which abstract the image of a function. This useful technique is frequently relegated to an exercise, and the lemmas repeatedly re-proved in papers which use it. Here we treat it in full as we shall need it for the study of the existential quantifier in Section 9.3.