ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 8
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| To appreciate the usefulness of natural transformations,
| the reader should prove for himself the following, which
| supports Slogan 3.
|
| Proposition 2.2. When objects such as sets, small graphs, and
| $M$-sets are viewed as functors into Sets (see Examples F1 to F3
| in Section 1), the morphisms between two objects are precisely the
| natural transformations. Thus, the categories of sets, small graphs,
| and $M$-sets may be identified with the functor categories Sets^$1$,
| Sets^(o>>o), and Sets^$M$, respectively.
|
| Of course, morphisms between sets are mappings, morphisms between graphs
| were described in Definition 1.3, and morphisms between $M$-sets are
| $M$-homomorphisms. (An $M$-homomorphism f : A -> B between $M$-sets
| is a mapping such that f(ma) = mf(a) for all m in M and a in A.
|
| We record three more basic isomorphisms in the spirit of Proposition 1.6.
|
| Proposition 2.3. For any categories $A$, $B$, $C$,
|
| $A$^$1$ ~=~ $A$,
|
| $C$^($A$ x $B$) ~=~ ($C$^$B$)^$A$,
|
| ($A$ x $B$)^$C$ ~=~ $A$^$C$ x $B$^$C$.
|
| We shall leave the lengthy proof of this to the reader. We only mention here
| the functor $C$^($A$ x $B$) -> ($C$^$B$)^$A$, which will be used later.
| We describe its action on objects by stipulating that it assigns to
| a functor F : $A$ x $B$ -> $C$ the functor F* : $A$ -> $C$^$B$
| which is defined as follows:
|
| For any object A of $A$,
|
| the functor F*(A) : $B$ -> $C$
| is given by
|
| F*(A)(B) = F(A, B),
| F*(A)(g) = F(1_A, g),
|
| for any object B of $B$
| and any arrow g : B -> B' in $B$.
|
| For any arrow f : A -> A',
|
| the natural transformation F*(A) -> F*(A')
| is given by
|
| F*(f)(B) = F(f, 1_B),
|
| for all objects B of $B$.
|
| Finally, to any natural transformation t : F -> G
| between functors F, G : $A$ x $B$ -> $C$ we assign
| the natural transformation t* : F* -> G* which is
| given by
|
| t*(A)(B) = t(A, B)
|
| for all objects A of $A$ and B of $B$.
|
| L&S, pages 8-9.
|
| 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. In this transcription the symbol "o>>o"
indicates the small category that is otherwise represented,
minus identity arrows, by either of the following diagrams:
. -> .
->
or
o--------------o o--------------o
| | ----------------> | |
| | | |
| | ----------------> | |
o--------------o o--------------o
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤