ñòð. 34 |

is a pullback. If g is a function with the same property, then g(x) 2 S if and only

b

if f (x) is, which means that g(x) = Â¤ if and only if f (x) = Â¤. Also, if g(x) 6Â¤,

=

b b in all cases.

then x 2 T0 so that g(x) = f (x) = f(x). Thus g = f

7. Since each object has a unique arrow to 1, there is a one to one correspondence

between subobjects of an object A and partial arrows of A to 1. But partial

!e

arrows of A to 1 are in one to one correspondence with arrows A Â¡ 1. Thus

Hom(A; 1) Â» Sub(A) which is the deÂ¯ning property of -.

e=

Section 5.4

Â¡!

1. We are thinking of = 0 Â¡ 1 as a category and 0 and 1 as two objects.

!

Â¡ Set. In

!

The category of graphs is the category of contravariant functors

particular, the objects 0 and 1 represent functors and the question is which ones.

Let us denote the two nonidentity arrows of by s and t (mnemonic for `source'

and `target'). A functor F : Â¡ Set determines and is determined by the two

!

sets F (1) and F (0) and the two arrows F (s) : F (1) Â¡ F (0) and f (t) : F (1) Â¡

! !

F (0). In the case that F = Hom(Â¡; 0), the two sets are Hom(0; 0) and Hom(1; 0)

which are a one-element set and the empty set, respectively, and the functions

are the unique functions that exists in that case. Thus the contravariant functor

represented by 0 is the graph 1 which we have also called No.

For take the functor represented by 1, the two sets are Hom(1; 1) = fid1 g and

Hom(0; 1) = fs, tg. The two arrows take the element of Hom(1; 1) to s and t

respectively. The graph 2 that we have also called No has just one arrow and two

nodes which are the source and target of the arrow, respectively, and so is the

graph represented by 1.

96 Solutions for section 5.5

2. There are two ways of dealing with this question and similar ones. We al-

ready have an explicit description of the subobject classiÂ¯er in this category and

we could simply examine the set of nodes and set of arrows and see that their

subfunctors have the desired structure. However, there is an easier way, once we

know there is a subobject classiÂ¯er. For the set of subobjects of the graph No is

Hom(No; -) which, in turn, is isomorphic by the preceding problem, to the set of

nodes of -. Similarly, the set of subobjects of the graph Ar is Hom(Ar; -), which

is the set of arrows of -.

3. Let NT(F; G) denote the set of natural transformations between functors F

and G. The Yoneda lemma implies that if [M Â¡ N ] = F , then

!

F (X) Â» NT(Hom(Â¡; X); F ) Â» NT(Hom(Â¡; X); [M Â¡ N ])

!

= =

Â»

= NT(Hom(Â¡; X) Â£ M; N )

4. We have that

Â» Â»

Sub(Hom(Â¡; X)) = NT(Hom(Â¡; X); -) = -(X)

the latter by the Yoneda Lemma.

Section 5.5

W

1. a. Let C = fc 2 j a ^ c Â· bg. Then a ) b = c. Then

c2C

_ _

a ^ (a ) b) = a ^ (a ^ c) Â· b

c=

c2C c2C

since a join of elements less than b is also less than b. Therefore, if c Â· a ) b then

a ^ c Â· b. On the other hand, if a ^ c Â· b, then c 2 C so that c Â· a ) b.

b. The fact that a Â· b ^ c if and only if a Â· b and a Â· c means that when

the Heyting algebra is considered as a category, Hom(a; b ^ c) = Hom(a; b) Â£

Hom(a; c). This means that b ^ c is the categorical product of b and c. But then

a ^ c Â· b if and only if c Â· a ) b means that Hom(a Â£ c; b) = Hom(c; a ) b),

which means that a ) b is the internal hom.

Bibliography

At the end of each entry, the pages on which that entry is cited are listed in parentheses.

AdÂ¶mek, J. and J. RosiÂ·ky (1994). Locally Presentable and Accessible Categories. Cam-

a c

bridge University Press. (12, 13, 25)

Asperti, A. and S. Martini (1992). `Categorical models of polymorphism'. Information

and Computation, volume 99, pages 1{79. (43)

Bagchi, A. and C. Wells (1994). `Graph-based logic and sketches I: The general frame-

work'. Available by gopher from the site gopher.cwru.edu, path=/class/mans/

math/pub/wells/. (24, 25)

Barr, M. and C. Wells (1985). Toposes, Triples and Theories, volume 278 of Grundlehren

der mathematischen Wissenschaften. Springer-Verlag, New York. A list of correc-

tions and additions is maintained in [Barr and Wells, 1993]. (16, 20, 22, 24, 25, 57,

59, 60, 61, 62, 66, 68)

Barr, M. and C. Wells (1994). `The categorical theory generated by a limit sketch'.

Available by gopher from the site gopher.cwru.edu, path=/class/mans/math/

pub/wells/. (20, 25)

Barr, M., C. McLarty, and C. Wells (1985). `Variable set theory'. Technical report,

McGill University. (72)

Barr, M. (1986). `Fuzzy sets and topos theory'. Canadian Math. Bull., volume 24, pages

501{508. (72)

Barr, M. (1986). `Models of sketches'. Cahiers de Topologie et GÂ¶omÂ¶trie DiffÂ¶rentielle

ee e

CatÂ¶gorique, volume 27, pages 93{107. (17)

e

Barr, M. (1989). `Models of Horn theories'. Contemporary Mathematics, volume 92,

pages 1{7. (12)

Bastiani, A. and C. Ehresmann (1972). `Categories of sketched structures'. Cahiers de

Topologie et GÂ¶omÂ¶trie DiffÂ¶rentielle, volume 13, pages 104{213. (20, 25)

ee e

Bell, J. (1988). Toposes and Local Set Theories: An Introduction. Oxford Logic Guides.

Oxford University Press. (57)

Boileau, A. and A. Joyal (1981). `La logique des topos'. Symbolic Logic, volume 46,

pages 6{16. (57)

Carboni, A., P. Freyd, and A. Scedrov (1988). `A categorical approach to realizability

and polymorphic types'. In Mathematical Foundations of Programming Language

Semantics, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, volume 298

of Lecture Notes in Computer Science, pages 23{42. Springer-Verlag. (79)

Cartmell, J. (1986). `Generalized algebraic theories and contextual categories'. Annals

Pure Applied Logic, volume 32, pages 209{243. (13)

Cockett, J. R. B. and D. Spencer (1992). `Strong categorical datatypes i'. In Category

Theory 1991, R. Seely, editor. American Mathematical Society. (41)

97

98 Bibliography

Coquand, T. and G. Huet (1988). `The calculus of constructions'. Information and

Computation, volume 76, pages 95{120. (43)

Coquand, T. (1988). `Categories of embeddings'. In Proceedings of the Third Annual

Symposium on Logic in Computer Science, Edinburgh, 1988, pages 256{263. Com-

puter Society Press and IEEE. (43)

Coste, M. (1976). `Une approche logique des thÂ¶ories dÂ¶Â¯nissables par limites projectives

e e

Â¯nies'. In SÂ¶minaire BÂ¶nabou. UniversitÂ¶ Paris-Nord. (13)

e e e

Duval, D. and J.-C. Reynaud (1994). `Sketches and computation (1)'. Mathematical

Structures in Computer Science, volume 4. (9)

Duval, D. and J.-C. Reynaud (1994). `Sketches and computation (2)'. Mathematical

Structures in Computer Science, volume 4. (9)

Ehresmann, C. (1968). `Esquisses et types des structures algÂ¶briques'. Bul. Inst. Polit.

e

IaÂ»i, volume XIV. (20, 25)

s

Ehrhard, T. (1988). `A categorical semantics of constructions'. In Proceedings of the

Third Annual Symposium on Logic in Computer Science, Edinburgh, 1988. Com-

puter Society Press and IEEE. (43)

Ehrig, H., H. Kreowski, J. Thatcher, E. Wagner, and J. Wright (1984). `Parameter pass-

ing in algebraic speciÂ¯cation languages'. Theoretical Computer Science, volume 28,

pages 45{81. (31)

Eilenberg, S. (1976). Automata, Languages and Machines, Vol. B. Academic Press.

(55)

ñòð. 34 |