Practical Foundations of Mathematics

Paul Taylor

4.1  Categories

DEFINITION 4.1.1 A category C consists of

(a)

a class of objects, obC,

(b)

for each pair of objects X,Y Î obC, a set of morphisms, C(X,Y) (for f Î C(X ,Y) we write f:X® Y, calling X the source and Y the target; the words domain and codomain are synonyms for source and target, and map and arrow are synonyms for morphism ; as a throwback to the time when categories were only used for algebras and homomorphisms, C(X,Y) is called the hom-set),

(c)

for each object X Î obC, an identity, \id_X Î C(X,X), and

(d)

for each triplet of objects, X, Y, Z Î ob C, a composition,

C(X,Y)xC(Y,Z)® C(X,Z),

which we write synonymously as f;g or go f (composition is a function between hom- sets, whereas f:X® Y is an abstract arrow),

such that f;id = f = id;f and f;(g;h) = (f;g);h, so the composition (;) is associative and id is a unit:

CONVENTION 4.1.2 The order of composition is a contentious issue. The left-handed notation (o) is older, both in category theory and in mathematics as a whole, and comes from the custom of writing function- application on the left - apart from the factorial function! We shall not challenge this custom itself: juxtaposition will always mean application on the left; moreover we shall adopt the convention from the l-calculus that FF X means (FF)X. If functional composition arises by abstraction of application, it is clearer to use the left-handed notation.

For those literate in Arabic or Hebrew, diagram-chasing in the right-to-left notation may present no problem, but for the rest of us it can be rather confusing. There are even situations, such as the composition of adjunctions (Lemma  3.6.6), where it helps to use both conventions together. Of course we distinguish them by using two different symbols (; and o), and we will always use one or other of them, without relying on juxtaposition. In practice there is no need to decorate these symbols with the objects to which they apply, though it is useful to annotate \id_X.

Categories as theories   In this book we shall be most interested in how categories can describe type- theoretic phenomena. The objects are contexts (lists of typed variables and predicates) and the morphisms are assignments (substitutions) of terms or proofs to these variables.

Categories as congregations   First, however, we give the usual list of mathematical structures and their homomorphisms. These categories are traditionally named by their objects, but in some cases such as matrices and programs the arrows are more prominent: following Peter Freyd and Andre Scedrov [FS90], we speak of the category composed of named maps, here relations.

LEMMA 4.1.3 Sets and binary relations form a category Rel, where the identity on X is the equality relation ( = _X), and the composition is the relational one given in Definition 1.3.7.

PROOF: Let R: X\leftharpoondown \rightharpoonup Y. Then

omitted eqnarray* environment

where Q: W\leftharpoondown \rightharpoonup X and S: Y\leftharpoondown\rightharpoonup Z.[]

PROPOSITION 4.1.4 The following form categories:

=- to # =0pt # =2em plus1em minus.5em # =1em #=0pt objects morphisms Section S: Y\leftharpoondown\rightharpoonup Z Set