ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 4
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| It follows from slogans 1 and 2 that small categories
| themselves should be the objects of a category worthy
| of study.
|
| Example C5. The category Cat has as objects small categories
| and as morphisms functors, which we shall now define.
|
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
| first of all a morphism of graphs (see Example C4),
| that is, it sends objects of $A$ to objects of $B$
| and arrows of $A$ to arrows of $B$ such that, if
| f : A -> A', then F(f) : F(A) -> F(A'). Moreover,
| a functor preserves identities and composition;
| thus:
|
| F(1_A) = 1_F(A),
|
| F(gf) = F(g)F(f).
|
| In particular, the identity functor 1_$A$ : $A$ -> $A$ leaves
| objects and arrows unchanged and the composition of functors
| F : $A$ -> $B$ and G : $B$ -> $C$ is given by:
|
| (GF)(A) = G(F(A)),
|
| (GF)(f) = G(F(f)),
|
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
|
| The reader will now easily check the following assertion.
|
| Proposition 1.4. When sets, monoids, and preordered sets
| are regarded as small categories, the morphisms between
| them are the same as the functors between them.
|
| The above definition of a functor F : $A$ -> $B$ applies equally well
| when $A$ and $B$ are not necessarily small, provided we allow mappings
| between classes. Of special interest is the situation when $B$ = Sets
| and $A$ is small.
|
| Slogan 3. Many objects of interest to mathematicians
| may be viewed as functors from small categories to Sets.
|
| Example F1. A set may be viewed as a functor
| from a discrete one-object category to Sets.
|
| Example F2. A small graph may be viewed
| as a functor from the small category
|
| . -> .
| ->
|
|(with identity arrows not shown) to Sets.
|
| Example F3. If $M$ = (M, 1, .) is a monoid
| viewed as a one-object category, an $M$-set
| may be regarded as a functor from $M$ to Sets.
|(An $M$-set is a set A together with a mapping
| M x A -> A, usually denoted by (m, a) ~> ma,
| such that 1a = a and (m.m')a = m(m'a) for all
| a in A, m and m' in M.)
|
| L&S, pages 6-7.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤