Computational category theory

Front Cover......Page 1
Contents......Page 7
Foreword......Page 11
Preface......Page 15
1 Introduction......Page 17
1.1 The contents......Page 20
1.2.1 Textbooks on category theory......Page 22
1.2.3 A selection of textbooks on functional programming......Page 23
1.3 Acknowledgements......Page 24
2 Functional Programming in ML......Page 25
2.1 Expressions, values and environments......Page 27
2.2 Functions......Page 29
2.2.2 Higher order functions......Page 30
2.3 Types......Page 31
2.3.2 Compound types......Page 32
2.4 Type polymorphism......Page 33
2.5 Patterns......Page 36
2.6 Defining types......Page 37
2.7 Abstract types......Page 40
2.8 Exceptions......Page 42
2.10 Exercises......Page 43
3.1 Categories......Page 51
3.1.1 Diagram chasing......Page 54
3.1.2 Subcategories, isomorphisms, monics and epis......Page 55
3.2.2 Graphs......Page 56
3.2.4 Relations and partial orders......Page 57
3.2.6 Deductive systems......Page 58
3.2.7 Universal algebra: terms, algebras and equations......Page 59
3.2.8 Sets with structure and structure-preserving arrows......Page 62
3.3 Categories computationally......Page 63
3.4.1 The category of finite sets......Page 65
3.4.2 Terms and term substitutions: the category T_tau^Fin......Page 66
3.4.3 A finite category......Page 68
3.5 Functors......Page 69
3.5.2 Examples......Page 70
3.6 Duality......Page 71
3.7 An assessment......Page 73
3.9 Exercises......Page 76
4 Limits and Colimits......Page 81
4.1 Definition by universality......Page 83
4.2 Finite colimits......Page 84
4.2.1 Initial objects......Page 85
4.2.2 Binary coproducts......Page 86
4.2.3 Coequalizers and pushouts......Page 88
4.3 Computing colimits......Page 90
4.4 Graphs, diagrams and colimits......Page 95
4.5 A general construction of colimits......Page 98
4.6 Colimits in the category of finite sets......Page 104
4.7 A calculation of pushouts......Page 106
4.8 Duality and limits......Page 109
4.9 Limits in the category of finite sets......Page 111
4.10 An application: operations on relations......Page 113
4.11 Exercises......Page 116
5 Constructing Categories......Page 119
5.1 Comma categories......Page 120
5.1.1 Representing comma categories......Page 121
5.2 Colimits in comma categories......Page 123
5.3 Calculating colimits of graphs......Page 125
5.4.1 Natural transformations......Page 129
5.4.2 Functor categories......Page 130
5.5 Colimits in functor categories......Page 132
5.6 Duality and limits......Page 134
5.7 Abstract colimits and limits......Page 136
5.7.1 Abstract diagrams and colimits......Page 137
5.7.2 Category constructions......Page 138
5.7.4 Discussion......Page 139
5.8 Exercises......Page 140
6 Adjunctions......Page 143
6.1 Definitions of adjunctions......Page 144
6.2 Representing adjunctions......Page 146
6.3 Examples......Page 147
6.3.2 Components of a graph......Page 148
6.3.3 Free algebras......Page 150
6.3.4 Graph theory......Page 152
6.3.6 Adjunctions and comma categories......Page 154
6.3.7 Examples from algebra and topology......Page 155
6.4 Computing with adjunctions......Page 156
6.5 Free algebras......Page 158
6.5.1 Constructing free algebras......Page 159
6.5.2 A program......Page 160
6.5.3 An example: transitive closure......Page 162
6.5.4 Other constructions of free algebras......Page 165
6.6 Exercises......Page 168
7 Toposes......Page 171
7.1 Cartesian closed categories......Page 172
7.1.1 An example: the category of finite sets......Page 173
7.2 Toposes......Page 175
7.2.1 An example: the topos of finite sets......Page 177
7.2.2 Computing in a topos......Page 178
7.2.3 Logic in a topos......Page 180
7.2.4 An example: a three-valued logic......Page 182
7.3 Conclusion......Page 186
7.4 Exercises......Page 187
8 A Categorical Unification Algorithm......Page 189
8.1 The unification of terms......Page 190
8.2 Unification as a coequalizer......Page 191
8.3 On constructing coequalizers......Page 192
8.4 A categorical program......Page 196
9 Constructing Theories......Page 203
9.1 Preliminaries......Page 204
9.2 Constructing theories......Page 206
9.3 Theories and institutions......Page 210
9.4 Colimits of theories......Page 213
9.5 Environments......Page 215
9.6 Semantic operations......Page 216
9.7 Implementing a categorical semantics......Page 217
10 Formal Systems for Category Theory......Page 219
10.1 Formal aspects of category theory......Page 220
10.2 Category theory in OBJ......Page 223
10.3 Category theory in a type theory......Page 232
10.4 Categorical data types......Page 234
A ML Keywords......Page 239
B Index of ML Functions......Page 241
C Other ML Functions......Page 245
D Answers to Programming Exercises......Page 247
Back Cover......Page 268