ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 6
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Definition 1.5. An arrow f : A -> B in a category is called an 'isomorphism'
| if there is an arrow g : B -> A such that gf = 1_A and fg = 1_B. One writes
| A ~=~ B to mean that such an isomorphism exists and says that A is 'isomorphic'
| with B.
|
| In particular, a functor F : $A$ -> $B$ between two categories is an isomorphism
| if there is a functor G : $B$ -> $A$ such that GF = 1_$A$ and FG = 1_$B$. We also
| remark that a group is a one-object category in which all arrows are isomorphisms.
|
| To end this section, we shall record three basic isomorphisms.
| Here $1$ is the category with one object and one arrow.
|
| Proposition 1.6. For any categories $A$, $B$, $C$,
|
| $A$ x $1$ ~=~ $A$,
|
| $A$ x $B$ ~=~ $B$ x $A$,
|
| $A$ x ($B$ x $C$) ~=~ ($A$ x $B$) x $C$.
|
| L&S, page 7.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤