R.M. Burstall University of Edinburgh

This is a version of Computational Category Theory that is available for personal use only. Distributing copies, multiple downloads, availability at other websites, or use of any of the text for commercial purposes is strictly forbidden. Full copyright remains with the authors.

Contents

1 Introduction 1.1 The contents 1.2 Accompanying texts 1.2.1 Textbooks on category theory 1.2.2 ML references and availability 1.2.3 A selection of textbooks on functional programming 1.3 Acknowledgements

1 4 6 6 7 7 8

2 Functional Programming in ML 2.1 Expressions, values and environments 2.2 Functions 2.2.1 Recursive definitions 2.2.2 Higher order functions 2.3 Types 2.3.1 Primitive types 2.3.2 Compound types 2.3.3 Type abbreviation 2.4 Type polymorphism 2.5 Patterns 2.6 Defining types 2.7 Abstract types 2.8 Exceptions 2.9 Other facilities 2.10 Exercises

9 11 13 14 14 15 16 16 17 17 20 21 24 26 27 27

3 Categories and Functors 3.1 Categories

35 35 vii

3.2

3.3 3.4

3.5

3.6 3.7 3.8 3.9

3.1.1 Diagram chasing 3.1.2 Subcategories, isomorphisms, monics and epis Examples 3.2.1 Sets and finite sets 3.2.2 Graphs 3.2.3 Finite categories 3.2.4 Relations and partial orders 3.2.5 Partial orders as categories 3.2.6 Deductive systems 3.2.7 Universal algebra: terms, algebras and equations 3.2.8 Sets with structure and structure-preserving arrows Categories computationally Categories as values 3.4.1 The category of finite sets 3.4.2 Terms and term substitutions: the category T Ω F in 3.4.3 A finite category Functors 3.5.1 Functors computationally 3.5.2 Examples Duality An assessment∗ Conclusion Exercises

4 Limits and Colimits 4.1 Definition by universality 4.2 Finite colimits 4.2.1 Initial objects 4.2.2 Binary coproducts 4.2.3 Coequalizers and pushouts 4.3 Computing colimits 4.4 Graphs, diagrams and colimits 4.5 A general construction of colimits 4.6 Colimits in the category of finite sets 4.7 A calculation of pushouts 4.8 Duality and limits 4.9 Limits in the category of finite sets 4.10 An application: operations on relations 4.11 Exercises

38 39 40 40 40 41 41 42 42 43 46 47 49 49 50 52 53 54 54 55 57 60 60 65 67 68 69 70 72 74 79 82 88 90 93 95 97 100

5 Constructing Categories 5.1 Comma categories 5.1.1 Representing comma categories 5.2 Colimits in comma categories 5.3 Calculating colimits of graphs 5.4 Functor categories 5.4.1 Natural transformations 5.4.2 Functor categories 5.5 Colimits in functor categories 5.6 Duality and limits 5.7 Abstract colimits and limits∗ 5.7.1 Abstract diagrams and colimits 5.7.2 Category constructions 5.7.3 Indexed colimit structures 5.7.4 Discussion 5.8 Exercises

103 104 105 107 109 113 113 114 116 118 120 121 122 123 123 124

6 Adjunctions 127 6.1 Definitions of adjunctions 128 6.2 Representing adjunctions 130 6.3 Examples 131 6.3.1 Floor and ceiling functions: converting real numbers to integers 132 6.3.2 Components of a graph 132 6.3.3 Free algebras 134 6.3.4 Graph theory 136 6.3.5 Limits and colimits 138 6.3.6 Adjunctions and comma categories 138 6.3.7 Examples from algebra and topology 139 6.4 Computing with adjunctions 140 6.5 Free algebras 142 6.5.1 Constructing free algebras 143 6.5.2 A program 144 6.5.3 An example: transitive closure 146 6.5.4 Other constructions of free algebras 149 6.6 Exercises 152 7 Toposes 7.1 Cartesian closed categories 7.1.1 An example: the category of finite sets 7.2 Toposes

155 156 157 159

7.3 7.4

7.2.1 An example: the topos of finite sets 7.2.2 Computing in a topos 7.2.3 Logic in a topos 7.2.4 An example: a three-valued logic Conclusion Exercises

161 162 164 166 170 171

8 A Categorical Unification Algorithm 8.1 The unification of terms 8.2 Unification as a coequalizer 8.3 On