Computational category theory

Contents......Page 4
Foreword......Page 8
Preface......Page 12
Introduction......Page 14
1.1 The contents......Page 17
1.2 Accompanying texts......Page 19
1.3 Acknowledgements......Page 21
Functional Programming in ML......Page 22
2.1 Expressions, values and environments......Page 24
2.2 Functions......Page 26
2.3 Types......Page 28
2.4 Type polymorphism......Page 30
2.5 Patterns......Page 33
2.6 De ning types......Page 34
2.7 Abstract types......Page 37
2.8 Exceptions......Page 39
2.10 Exercises......Page 40
3.1 Categories......Page 48
3.2 Examples......Page 53
3.3 Categories computationally......Page 60
3.4 Categories as values......Page 62
3.5 Functors......Page 66
3.6 Duality......Page 68
3.7 An assessment......Page 70
3.9 Exercises......Page 73
Limits and Colimits......Page 78
4.1 De nition by universality......Page 80
4.2 Finite colimits......Page 81
4.3 Computing colimits......Page 87
4.4 Graphs, diagrams and colimits......Page 92
4.5 A general construction of colimits......Page 95
4.6 Colimits in the category of  nite sets......Page 101
4.7 A calculation of pushouts......Page 103
4.8 Duality and limits......Page 106
4.9 Limits in the category of  nite sets......Page 108
4.10 An application: operations on relations......Page 110
4.11 Exercises......Page 113
Constructing Categories......Page 116
5.1 Comma categories......Page 117
5.2 Colimits in comma categories......Page 120
5.3 Calculating colimits of graphs......Page 122
5.4 Functor categories......Page 126
5.5 Colimits in functor categories......Page 129
5.6 Duality and limits......Page 131
5.7 Abstract colimits and limits......Page 133
5.8 Exercises......Page 137
Adjunctions......Page 140
6.1 De nitions of adjunctions......Page 141
6.2 Representing adjunctions......Page 143
6.3 Examples......Page 144
6.4 Computing with adjunctions......Page 153
6.5 Free algebras......Page 155
6.6 Exercises......Page 165
Toposes......Page 168
7.1 Cartesian closed categories......Page 169
7.2 Toposes......Page 172
7.3 Conclusion......Page 183
7.4 Exercises......Page 184
A Categorical Unification Algorithm......Page 186
8.1 The uni cation of terms......Page 187
8.2 Uni cation as a coequalizer......Page 188
8.3 On constructing coequalizers......Page 189
8.4 A categorical program......Page 193
Constructing Theories......Page 200
9.1 Preliminaries......Page 201
9.2 Constructing theories......Page 203
9.3 Theories and institutions......Page 207
9.4 Colimits of theories......Page 210
9.5 Environments......Page 212
9.6 Semantic operations......Page 213
9.7 Implementing a categorical semantics......Page 214
Formal Systems for Category Theory......Page 216
10.1 Formal aspects of category theory......Page 217
10.2 Category theory in OBJ......Page 220
10.3 Category theory in a type theory......Page 229
10.4 Categorical data types......Page 231
ML Keywords......Page 236
Index of ML Functions......Page 238
Other ML Functions......Page 242
Exercises......Page 244