《Category Theory for CS》

【实例截图】

【核心代码】

Contents
Preface xi
1 Preliminaries 1
1.1 Sets 1
1.2 Functions 3
1.3 Graphs 8
1.4 Homomorphisms of graphs 11
2 Categories 15
2.1 Basic definitions 15
2.2 Functional programming languages as categories 20
2.3 Mathematical structures as categories 23
2.4 Categories of sets with structure 27
2.5 Categories of algebraic structures 32
2.6 Constructions on categories 35
2.7 Properties of objects and arrows in a category 40
2.8 Monomorphisms and subobjects 47
2.9 Other types of arrow 53
2.10 Factorization systems 58
3 Functors 65
3.1 Functors 65
3.2 Actions 74
3.3 Types of functors 80
3.4 Equivalences 84
3.5 Quotient categories 88
4 Diagrams, naturality and sketches 93
4.1 Diagrams 93
4.2 Natural transformations 101
4.3 Natural transformations between functors 109
4.4 The Godement calculus of natural transformations 117
4.5 The Yoneda Lemma and universal elements 121
4.6 Linear sketches (graphs with diagrams) 127
4.7 Linear sketches with constants: initial term models 133
4.8 2-categories 140
vii
viii Contents
5 Products and sums 153
5.1 The product of two objects in a category 153
5.2 Notation for and properties of products 157
5.3 Finite products 168
5.4 Sums 178
5.5 Natural numbers objects 182
5.6 Deduction systems as categories 186
5.7 Distributive categories 188
6 Cartesian closed categories 195
6.1 Cartesian closed categories 195
6.2 Properties of cartesian closed categories 202
6.3 Typed λ-calculus 208
6.4 λ-calculus to category and back 210
6.5 Arrows vs. terms 212
6.6 Fixed points in cartesian closed categories 215
7 Finite product sketches 219
7.1 Finite product sketches 220
7.2 The sketch for semigroups 225
7.3 Notation for FP sketches 231
7.4 Arrows between models of FP sketches 234
7.5 The theory of an FP sketch 237
7.6 Initial term models for FP sketches 239
7.7 Signatures and FP sketches 245
8 Finite discrete sketches 251
8.1 Sketches with sums 251
8.2 The sketch for fields 254
8.3 Term algebras for FD sketches 257
9 Limits and colimits 265
9.1 Equalizers 265
9.2 The general concept of limit 268
9.3 Pullbacks 273
9.4 Coequalizers 277
9.5 Cocones 280
9.6 More about sums 285
9.7 Unification as coequalizer 289
9.8 Properties of factorization systems 294
Contents ix
10 More about sketches 299
10.1 Finite limit sketches 299
10.2 Initial term models of FL sketches 304
10.3 The theory of an FL sketch 307
10.4 General definition of sketch 309
11 The category of sketches 313
11.1 Homomorphisms of sketches 313
11.2 Parametrized data types as pushouts 315
11.3 The model category functor 320
12 Fibrations 327
12.1 Fibrations 327
12.2 The Grothendieck construction 332
12.3 An equivalence of categories 338
12.4 Wreath products 341
13 Adjoints 347
13.1 Free monoids 347
13.2 Adjoints 350
13.3 Further topics on adjoints 356
13.4 Locally cartesian closed categories 360
14 Algebras for endofunctors 363
14.1 Fixed points for a functor 363
14.2 Recursive categories 368
14.3 Triples 372
14.4 Factorizations of a triple 374
14.5 Scott domains 376
15 Toposes 383
15.1 Definition of topos 384
15.2 Properties of toposes 387
15.3 Is a two-element poset complete? 391
15.4 Presheaves 393
15.5 Sheaves 395
15.6 Fuzzy sets 400
15.7 External functors 403
15.8 The realizability topos 408
x Contents
16 Categories with monoidal structure 413
16.1 Closed monoidal categories 413
16.2 Properties of A−◦C 417
16.3 ∗-autonomous categories 422
16.4 The Chu construction 424
Solutions to the exercises 431
Solutions for Chapter 1 431
Solutions for Chapter 2 433
Solutions for Chapter 3 442
Solutions for Chapter 4 449
Solutions for Chapter 5 460
Solutions for Chapter 6 467
Solutions for Chapter 7 471
Solutions for Chapter 8 475
Solutions for Chapter 9 477
Solutions for Chapter 10 488
Solutions for Chapter 11 489
Solutions for Chapter 12 491
Solutions for Chapter 13 494
Solutions for Chapter 14 498
Solutions for Chapter 15 506
Solutions for Chapter 16 510
Bibliography 517
Index 531