DEFINITION 4.1.1 A category C consists of
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 \idX.
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: