CATEGORY THEORY FOR COMPUTING SCIENCE MICHAEL BARR AND CHARLES WELLS

Transmitted by Richard Blute, Robert Rosebrugh and Alex Simpson. Reprint published on 2012-09-19, revised 2013-09-22. 2010 Mathematics Subject Classification: 18-01,68-01. Key words and phrases: Category theory, computing science.

1

Preface to the TAC reprint (Revised 2013-09-22) This is a reprint of the final version, published by the Centre de Recherche Math´ematique at the Universit´e de Montr´eal. We are now aware of the following errors. If any others are reported, we will post corrections at ftp.math.mcgill.ca/barr/pdffiles/ctcserr.pdf and at http://www. abstractmath.org/CTCS/ctcserr.pdf. There is a diagram missing in the solution to problem 4.1.4. The problem is on page 98 and the solution on page 438. The diagram is C0

/

id

C1

F0

F1

D0

id

/

D1

On page 302, the second of the first line of diagrams near the middle of the page should be c3 ??? ?? ??p2 p1 ?? hp ,p i 1 2 ?? ?? o / c1 c1 c2 p1

p2

The left bottom p1 goes in the wrong direction and there is a spurious 0. Dan Synek has pointed out that the definition of cone is not really coherent because it depends on an ambient category and there is none. Accordingly, we define a cone as a rooted graph in which there is exactly one arrow from the root to each other node (along with, in general, other arrows). A cone in a category is a limit cone if the root is the limit in the usual sense if the arrows out of the root are the transition arrows of a limit of the remaining nodes and arrows of the cone. A model of the sketch is required to take each cone to a limit cone. He also pointed out that in the description of the sketch for categories, three arrows have to be added to the underlying graph of the sketch, all appearing in display in the middle of page 303. The / c0 (“the object in first one, on the left hand diagram of that display, is the unlabeled arrow c2 / the middle of a composite”). The other two are arrows c3 c0 so that the right hand diagram of the same display becomes: c3 3E yy 33EEE yy 3 EE p3 y yy p2 333 EEE y yy 33 EEE |yy " c1 c1 E 333 c1 EE 33 yy E y y EE 33 E 3 yyyy s s EEE 33 t t y EE3 y |yy " p1

c0

c0

Category Theory for Computing Science

Michael Barr Charles Wells

c °Michael Barr and Charles Wells, 1998

Category Theory for Computing Science

Michael Barr Department of Mathematics and Statistics McGill University Charles Wells Department of Mathematics Case Western Reserve University

For Becky, Adam and Joe and Matt and Peter

Contents Preface

xi

1 Preliminaries 1.1 Sets 1.2 Functions 1.3 Graphs 1.4 Homomorphisms of graphs

1 1 3 8 11

2 Categories 2.1 Basic definitions 2.2 Functional programming languages as categories 2.3 Mathematical structures as categories 2.4 Categories of sets with structure 2.5 Categories of algebraic structures 2.6 Constructions on categories 2.7 Properties of objects and arrows in a category 2.8 Monomorphisms and subobjects 2.9 Other types of arrow 2.10 Factorization systems

15 15 20 23 27 32 35 40 47 53 58

3 Functors 3.1 Functors 3.2 Actions 3.3 Types of functors 3.4 Equivalences 3.5 Quotient categories

65 65 74 80 84 88

4 Diagrams, naturality and sketches 4.1 Diagrams 4.2 Natural transformations 4.3 Natural transformations between functors 4.4 The Godement calculus of natural transformations 4.5 The Yoneda Lemma and universal elements 4.6 Linear sketches (graphs with diagrams) 4.7 Linear sketches with constants: initial term models 4.8 2-categories

93 93 101 109 11