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
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
3 Categories and Functors
3.1 Categories
3.1.1 Diagram chasing
3.1.2 Subcategories, isomorphisms, monics and epis
3.2 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
3.3 Categories computationally
3.4 Categories as values
3.4.1 The category of finite sets
3.4.2 Terms and term substitutions: the category T_tau^Fin
3.4.3 A finite category
3.5 Functors
3.5.1 Functors computationally
3.5.2 Examples
3.6 Duality
3.7 An assessment*
3.8 Conclusion
3.9 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
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
6 Adjunctions
6.1 Definitions of adjunctions
6.2 Representing adjunctions
6.3 Examples
6.3.1 Floor and ceiling functions: converting real numbers to integers
6.3.2 Components of a graph
6.3.3 Free algebras
6.3.4 Graph theory
6.3.5 Limits and colimits
6.3.6 Adjunctions and comma categories
6.3.7 Examples from algebra and topology
6.4 Computing with adjunctions
6.5 Free algebras
6.5.1 Constructing free algebras
6.5.2 A program
6.5.3 An example: transitive closure
6.5.4 Other constructions of free algebras
6.6 Exercises
7 Toposes
7.1 Cartesian closed categories
7.1.1 An example: the category of finite sets
7.2 Toposes
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
7.3 Conclusion
7.4 Exercises
8 A Categorical Unification Algorithm
8.1 The unification of terms
8.2 Unification as a coequalizer
8.3 On constructing coequalizers
8.4 A categorical program
9 Constructing Theories
9.1 Preliminaries
9.2 Constructing theories
9.3 Theories and institutions
9.4 Colimits of theories
9.5 Environments
9.6 Semantic operations
9.7 Implementing a categorical semantics
10 Formal Systems for Category Theory
10.1 Formal aspects of category theory
10.2 Category theory in OBJ
10.3 Category theory in a type theory
10.4 Categorical data types
A ML Keywords
B Index of ML Functions
C Other ML Functions
D Answers to Programming Exercises 231