ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 24
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 3. Cartesian Closed Categories Equationally Presented
|
| A 'category' is a deductive system in which
| the following equations hold between proofs:
|
| E1. f 1_A = f,
|
| 1_B f = f,
|
| (hg)f = h(gf),
|
| for all f : A -> B, g : B -> C, h : C -> D.
|
| Thus, from any deductive system one may obtain a category
| by imposing a suitable equivalence relation between proofs.
|
| A 'cartesian category' is both a category
| and a conjunction calculus satisfying the
| additional equations:
|
| E2. f = O_A, for all f : A -> T.
|
| E3a. p1_A,B <f, g> = f,
|
| E3b. p2_A,B <f, g> = g,
|
| E3c. <p1_A,B h, p2_A,B h> = h,
|
| for all f : C -> A, g : C -> B, h : C -> A & B.
|
| E2 asserts T is a 'terminal object'.
| One usually writes T = 1, and
| we shall do so from now on.
| An equivalent formulation
| of E2 is:
|
| E'2. 1_1 = O_1,
|
| O_B f = O_A,
|
| for all f : A -> B.
|
| E3 asserts that A & B is a product of A and B
| with projections p1_A,B and p2_A,B. We shall
| adopt the usual notation A & B = A x B.
|
| As a consequence of E3, let us record the 'distributive law':
|
| <f, g> h = <fh, gh>
|
| for all f : C -> A, g : C -> B, h : D -> C.
|
| Proof. We show this as follows, omitting subscripts:
|
| <f, g> h = <p1(<f, g> h), p2(<f, g> h)>
|
| = <(p1<f, g>) h, (p2<f, g> h)>
|
| = <fh, gh>.
|
| We shall also write
|
| f x g = f & g = <f p1_A,C, g p2_A,C>,
|
| whenever f : A -> B and g : C -> D, and note
| that x : $A$ x $A$ -> $A$ is a functor (see
| Part 0, Definition 1.3). Indeed, we have:
|
| 1_A x 1_C = <1_A p1_A,C, 1_C p2_A,C>
|
| = <p1_A,C, p2_A,C>
|
| = <p1_A,C 1_AxC, p2_A,C 1_AxC>
|
| = 1_AxC,
|
| and, omitting subscripts, by the distributive law,
|
| (f x g)(f' x g') = <f p1, g p2> <f' p1, g' p2>
|
| = <f p1 <f' p1, g' p2>, g p2 <f' p1, g' p2>
|
| = <f f' p1, g g' p2>
|
| = f f' x g g'.
|
| L&S, pages 52-53.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤