of the configuration of an implemented module from a specification. Finally conclusions are drawn in Section 5.

2 Background

In this section we explain the concepts and notation from 2-dimensional category theory before defining the property of adjointness and the structure of a monad. By working within a 2-dimensional category we gain greater expressive power based on the horizontal and vertical composition of natural transformations and functors.

2.1 A 2-dimensional Category

We use [8, 16] to present the background to Kock's work which is based on the structure of a 2-dimensional category. Since constructions are made on categories, functors, as the structure-preserving `homo-morphisms' between categories, are defined within the category of all categories. Functors are arrows (morphisms) which model the objects and arrows of one category in another category. The modelling is made by functions on the objects and arrows of the first category in such a way that a single entity of these objects, and the arrows between them, is constructed in the second category.

From considering functors as arrows between any two categories, we can define a category of functors with arrows called natural transformations. The naturality condition for the family of arrows that defines the transformation is expressed by a commutative diagram in the second (or target) category.

Categories and functors themselves form a category Cat, which is a large category with objects that are small categories. Within Cat both the vertical and the horizontal composition of two natural transformations can be defined with a rule that relates these compositions by an identity. This is the basis of 2-dimensional category theory. It is important to note that the objects for vertical composition are the functors, whereas for horizontal composition the objects are the categories. The definition of a two-dimensional category is based on the following definition of a double category.

Definition 2.1.1 (A Double Category) A double category is the set of arrows of two different categories under two different operations of composition, ? and ffi, which together satisfy the interchange law. 2

Definition 2.1.2 (A Two-Dimensional Category) A two-dimensional category is a double category in which every identity arrow for the first of the two compositions is also an identity for the second composition. It is often called a 2-dimensional or 2-category .
2

Notation 2.1.3 In [7] Kock uses the following standard notation from 2- dimensional category theory: