ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 7
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. Natural Transformations
|
| In this section we shall investigate morphisms between functors.
|
| Definition 2.1. Given functors F, G : $A$ -> $B$,
| a 'natural transformation' t : F -> G is a family
| of arrows t(A) : F(A) -> G(A) in $B$, one arrow for
| each object A of $A$, such that the following square
| commutes for all arrows f : A -> B in $A$:
|
| t(A)
| F(A) o------------------>o G(A)
| | |
| | |
| F(f) | | G(f)
| | |
| v v
| F(B) o------------------>o G(B)
| t(B)
|
| that is to say, such that
|
| G(f)t(A) = t(B)F(f).
|
| It is this concept about which it has been said that it
| necessitated the invention of category theory. We shall
| give examples of natural transformations later. For the
| moment, we are interested in another example of a category.
|
| Example C8. Given categories $A$ and $B$, the 'functor category' $B$^$A$ has
| as objects functors F : $A$ -> $B$ and as arrows natural transformations.
| The 'identity' natural transformation 1_F : F -> F is of course given
| by stipulating that (1_F)(A) = 1_(F(A)) for each object A of $A$.
| If t : F -> G and u : G -> H are natural transformations,
| their 'composition' u o t is given by stipulating that
|
| (u o t)(A) = u(A)t(A)
|
| for each object A of $A$.
|
| L&S, page 8.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
Note On Notation. An expression like "1_F(A)"
shall be interpreted as equivalent to "1_(F(A))".
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤