ñòð. 1 |

Preface iii

1 Finite discrete sketches 1

1.1 Sketches with sums 1

1.2 The sketch for Â¯elds 3

1.3 Term algebras for FD sketches 5

2 More about sketches 12

2.1 Finite limit sketches 12

2.2 Initial term models of FL sketches 16

2.3 The theory of an FL sketch 19

2.4 General deÂ¯nition of sketch 21

3 The category of sketches 26

3.1 Homomorphisms of sketches 26

3.2 Parametrized data types as pushouts 28

3.3 The model category functor 33

4 Fibrations 38

4.1 Fibrations 38

4.2 The Grothendieck construction 43

4.3 An equivalence of categories 48

4.4 Wreath products 51

5 Toposes 56

5.1 DeÂ¯nition of topos 57

5.2 Properties of toposes 60

5.3 Is a two-element poset complete? 64

5.4 Presheaves 66

5.5 Sheaves 67

5.6 Fuzzy sets 72

5.7 External functors 75

5.8 The realizability topos 79

i

ii Contents

Answers to Exercises 83

Solutions for Chapter 1 83

Solutions for Chapter 2 85

Solutions for Chapter 3 87

Solutions for Chapter 4 88

Solutions for Chapter 5 92

Bibliography 97

Index 102

Preface

This is the electronic supplement to Category Theory for Computing Sci-

ence, second edition, Prentice-Hall International, 1995, ISBN 0-13-

323809-1. It consists of (revisions of) Â¯ve chapters from the Â¯rst edition of that

book, as well as continuing updates of the Â¯rst and second editions.

The chapters included here are, as numbered in the Â¯rst edition, Chapters 7

(Finite discrete sketches), 9 (More about sketches), 10 (The category of sketches),

11 (Fibrations) and 14 (Toposes).

References, both in the published book and here to material in this electronic

supplement are preÂ¯xed by ` ES', while references to the printed book are un-

adorned. Thus a reference to 4.5 of Chapter 3 is a reference to Section 4.5 of

Chapter 3 of the printed book, while references to Section 4.5 of Chapter ES 3 is

a reference to Section 4.5 of Chapter 3 of this supplement. A reference without a

chapter number refers, as usual, to the current chapter.

iii

1

Finite discrete sketches

This chapter discusses FD (Â¯nite discrete) sketches, which are a more general kind

of sketch than that described in Chapter 7. The sketches described here allow

the speciÂ¯cation of objects which are sums as well as products. Section ES 1.1

introduces these sketches. Section ES 1.2 gives a detailed description of the sketch

for Â¯elds as an example of an FD sketch. In Section ES 1.3, we show how to modify

initial algebra construction so that it works for FD sketches. FD sketches have

theories, too, but discussion of that is postponed until Chapter ES 2.

1.1 Sketches with sums

Using sum cocones as well as product cones in a sketch allows one to express

alternatives as well as n-ary operations.

1.1.1 A Â¯nite discrete sketch, or FD sketch, = ( ; ; ; ), consists

of a Â¯nite graph , a Â¯nite set of Â¯nite diagrams , a Â¯nite set of discrete

cones with Â¯nite bases, and a Â¯nite set of discrete cocones with Â¯nite bases.

in Set is a graph homomorphism M : Â¡ Set !

A model of the FD sketch

which takes the diagrams in to commutative diagrams, the cones in to

product cones, and the cocones in to sum cocones.

1.1.2 The sketch for lists The FD sketch for Â¯nite lists illustrates how FD

sketches can be used to specify a data type which has an exceptional case for

which an operation is not deÂ¯ned. (Compare 7.1.6.) The graph has nodes 1, d (the

data), l (the lists) and l+ (the nonempty lists). There are no diagrams. There is a

cone with empty base expressing the fact that 1 must become a terminal object

in a model, another cone

l+

Â¡ @

head Â¡ @ tail

Â¡

Âª R

@

d l

and one cocone

l+

1

@ Â¡

@ Â¡

@

R Â¡

Âª

l

1

2 Finite discrete sketches

These can be summed up in the expressions l+ = d Â£ l (a nonempty list has a

datum as head and a list as tail) and l = 1 + l+ : (a list is either the empty list {

the single member of the terminal set { or a nonempty list). The fact that a sum

becomes a disjoint union in a model in Set enables us to express alternatives in

the way exhibited by this description. We thereby avoid the problem mentioned

in 7.1.6: we can deÂ¯ne head for only nonempty lists because we have a separate

sort for nonempty lists.

If S is any Â¯nite set, there is a model M of this sketch for which M (d) = S,

M (1) is the singleton set containing only the empty list hi, M (l) is the set of Â¯nite

lists of elements of S, and M (l+ ) is the set of Â¯nite nonempty lists of elements

of S. M (head) and M (tail) pick out the head and tail of a nonempty list. This is

an initial term algebra (to be deÂ¯ned in Section ES 1.3) for the sketch extended

by one constant for each element of S.

1.1.3 Given a Â¯nite set S, the model M just mentioned is certainly not the only

model of the sketch for which M (d) is S. Another model has M (l) all Â¯nite and

inÂ¯nite lists of elements of S, with M (l+ ) the nonempty lists and M (head) and

M (tail) as before. This model contains elements inaccessible by applying opera-

tions to constants: you cannot get inÂ¯nite lists by iterating operations starting

with constants. They are junk as deÂ¯ned in 7.6.3.

1.1.4 The sketch for natural numbers We will now modify the sketch 7.1.5

in a way which shows how FD sketches can model overÂ°ow.

The graph contains nodes we will call 1, n, nover and n + nover , which we

interpret, respectively, as a one-element set, a set of natural numbers (of which

there may be only Â¯nitely many), an overÂ°ow element and the set of all natural

numbers. The only cone is the one implicit in the name 1: the cone has 1 as the

vertex and the empty base. There is similarly a (discrete) cocone implicit in the

name n + nover . There is a constant operation zero : 1 Â¡ n and a unary operation

!

succ : n Â¡ n + nover . There are no diagrams.

!

There are many models of this sketch in Set. Here are three of them. They

ñòð. 1 |