# Practical Foundations of Mathematics

### Paul Taylor

#
Chapter 5

Limits and Colimits

Products may easily be defined for infinitely many factors, and also considered
in the opposite category. However, unlike meets and joins in posets, this
does not exhaust the possible types of limits and colimits in categories.
Since most of the interesting phenomena may be observed more clearly in the
concrete cases of pullback, equaliser, pushout and coequaliser, we postpone
the abstract definition to Section 7.3.
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.