ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 2
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| We shall now progress from concrete categories
| to abstract ones, in three easy stages.
|
| Definition 1.2. A 'graph' (usually called a 'directed graph') consists
| of two classes: the class of 'arrows' (or 'oriented edges') and the class
| of 'objects' (usually called 'nodes' or 'vertices') and two mappings from
| the class of arrows to the class of objects, called 'source' and 'target'
| (often also 'domain' and 'codomain').
|
| o--------------o source o--------------o
| | | ----------------> | |
| | Arrows | | Objects |
| | | ----------------> | |
| o--------------o target o--------------o
|
| One writes "f : A -> B" for "source f = A and target f = B".
| A graph is said to be 'small' if the classes of objects and
| arrows are sets.
|
| Example C4. The category of small 'graphs' is another concrete category.
| Its objects are small graphs and its morphisms are functions F which send
| arrows to arrows and vertices to vertices so that, whenever f : A -> B,
| then F(f) : F(A) -> F(B).
|
| A 'deductive system' is a graph in which to each object A there
| is associated an arrow 1_A : A -> A, the 'identity' arrow, and to
| each pair of arrows f : A -> B and g : B -> C there is associated
| an arrow gf : A -> C, the 'composition' of f with g. A logician
| may think of the objects as 'formulas' and of the arrows as
| 'deductions' or 'proofs', hence of
|
| f : A -> B g : B -> C
| ---------------------------
| gf : A -> C
|
| as a 'rule of inference'.
|
| (Deductive systems will be discussed further in Part 1.)
|
| A 'category' is a deductive system in which the following equations hold,
| for all f : A -> B, g : B -> C, and h : C -> D.
|
| f 1_A = f = 1_B f,
|
| (hg)f = h(gf).
|
| Of course, all concrete categories are categories. A category is
| said to be 'small' if the classes of arrows and objects are sets.
| While the concrete categories described in examples 1 to 4 are not
| small, a somewhat surprising observation is summarized as follows:
|
| Slogan 2. Many objects of interest to mathematicians
| are themselves small categories.
|
| L&S, page 5.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤