Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

ONT Re: Higher Order Categorical Logic


¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

Note 9

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

| This may be as good a place as any to mention that
| natural transformations may also be composed with
| functors.
|
| Definition 2.4.  In the situation
|
|               F
|      L       --->      K
| $D$ ---> $A$      $B$ ---> $C$,
|              --->
|               G
|
| if t : F -> G is a natural transformation, one obtains natural
| transformations Kt : KF -> KG between functors from $A$ to $C$
| and tL : FL -> GL between functors from $D$ to $B$ defined as
| follows:
|
| (Kt)(A)  =  K(t(A)),
|
| (tL)(D)  =  t(L(D)),
|
| for all objects A of $A$ and D of $D$.
|
| If H : $A$ -> $B$ is another functor and
| u : G -> H another natural transformation,
| then the reader will easily check the
| following "distributive laws":
|
| K(u o t)  =  (Ku) o (Kt),
|
| (u o t)L  =  (uL) o (tL).
|
| L&S, pages 9-10.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤