ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 26
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| We shall state another useful equation,
| which may also be regarded as a kind of
| distributive law.
|
| h*k = (h <k p1_D,B, p2_D,B>)*,
|
| where h : A x B -> C and k : D -> A.
|
| Proof. We show this as follows,
| omitting subscripts:
|
| h*k = (!e! <h*k p1, p2>)*
|
| = (!e! <h*p1, p2> <k p1, p2>)*
|
| = (h <k p1, p2>)*.
|
| Quite important is the following bijection,
| which holds in any cartesian closed category.
|
| Hom(A, B) ~=~ Hom(1, B^A).
|
| Proof. As in Section 1, with any f : A -> B
| we associate #f : 1 -> B^A, called the 'name'
| of f by Lawvere, given by
|
| #f = (f p2_1,A)*,
|
| and with any g : 1 -> B^A we associate
| g` : A -> B, read "g of", given by
|
| g` = !e!_B,A <g O_A, 1_A>.
|
| We then calculate
|
| (#f)` = f,
|
| #(g`) = g.
|
| L&S, pages 54-55.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤