# Practical Foundations of Mathematics

### Paul Taylor

#
Chapter 4

Cartesian Closed Categories

C ategory theory unifies the symbolic (Formalist) and model-based
(Platonist) views of mathematics. In particular it offers an agnostic solution
to the question that we raised in Section 1.3 of whether
a function is an algorithm or an input-output relation.
Traditionally, categories were *congregations*, each object being
a *set with structure*: a topological space, an algebra or a model
of some theory. The morphisms are functions that preserve this structure
(homomorphisms), so the notion of composition is ultimately that for relations
(Definition 1.3.7). As an approach to logic,
this went round ``three sides of a square'' ( *cf* Remark
1.6.13 for model theory) and so ran into some
foundational problems over the category of all categories.

In informatics, the principal examples are constructed from l-calculi
and programming languages; being syntactic, they are typically recursively
enumerable. Composition is by substitution of terms (Definition
1.1.10), or by the cut rule (Definition
1.4.8), which uses old conclusions as new hypotheses.
A category *Cn*^{[]}_{L} of this kind encodes a certain
theory *L* itself, instead of collecting its models; we call it the
*category of contexts and substitutions* by analogy with categories
of *objects and homomorphisms* in semantics.

We shall give a novel construction of *Cn*^{[]}_{L}
that embodies well-established techniques for proving correctness of
programs and works uniformly for any fragment of logic. At the unary level,
the ideas come from geometry and physics (groups), automata and topology;
we also carry it out for algebraic theories ( *Cn*^{×}_{L})
before turning to the l-calculus ( *Cn*^{® }_{L}
).

The fragment of logic in question, [], corresponds to certain categorical
structure defined by universal properties: products and exponentials
in this chapter, coproducts and factorisation systems in the next. The
recursively defined interpretation functor
[[-]]:*Cn*^{[]}_{L}® *S* preserves this structure, so
the semantic universe *S* must also have it.
*Cn*^{[]}_{L} is also called the *classifying category* for (models of)
the theory, because there is a correspondence between such functors and
models in *S*.