ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 10
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| If we compare Slogans 1 and 3, we are led to ask:
| which categories may be viewed as categories of
| functors into Sets? In preparation for an answer
| to that question we need another definition.
|
| Definition 2.5. If A and B are objects of a category $A$,
| we denote by Hom_$A$ (A, B) the class of arrows A -> B.
| (Later, the subscript $A$ will often be omitted.)
| If it so happens that Hom_$A$ (A, B) is a set
| for all objects A and B, $A$ is said
| to be 'locally small'.
|
| One purpose of this definition is
| to describe the following functor.
|
| Example F4. If $A$ is a locally small category,
| then there is a functor
|
| Hom_$A$ : $A$^op x $A$ -> Sets.
|
| For an object (A, B) of $A$^op x $A$, the value of this
| functor is Hom_$A$ (A, B), as suggested by the notation.
| For an arrow (g, h) : (A, B) -> (A', B') of $A$^op x $A$,
| where g : A' -> A and h : B -> B' in $A$, Hom_$A$ (g, h)
| sends f in Hom_$A$ (A, B) to hfg in Hom_$A$ (A', B').
|
| Applying the isomorphism
|
| Sets^($A$^op x $A$) -> (Sets^$A$)^($A$^op)
|
| of Proposition 2.3, we obtain a functor
|
| (Hom_$A$)* : $A$^op -> Sets^$A$
|
| and, dually, a functor
|
| (Hom_$A$^op)* : $A$ -> Sets^($A$^op).
|
| We shall see that the latter functor allows us to assert that
| $A$ is isomorphic to a "full" subcategory of Sets^($A$^op).
|
| L&S, page 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/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤