. 1
( 10)



>>

CATEGORIES
TYPES
AND STRUCTURES
An Introduction to Category Theory for the working computer scientist




Andrea Asperti

Giuseppe Longo




I
INTRODUCTION

The main methodological connection between programming language theory and category theory is
the fact that both theories are essentially ’theories of functions.“ A crucial point, though, is that the
categorical notion of morphism generalizes the set-theoretical description of function in a very broad
sense, which provides a unified understanding of various aspects of the theory of programs. This is
one of the reasons for the increasing role of category theory in the semantic investigation of programs
if compared, say, to the set-theoretic approach. However, the influence of this mathematical
discipline on computer science goes beyond the methodological issue, as the categorical approach to
mathematical formalization seems to be suitable for focusing concerns in many different areas of
computer science, such as software engineering and artificial intelligence, as well as automata theory
and other theoretical aspects of computation.
This book is mostly inspired by this specific methodological connection and its applications to the
theory of programming languages. More precisely, as expressed by the subtitle, it aims at a self-
contained introduction to general category theory (part I) and at a categorical understanding of the
mathematical structures that constituted, in the last twenty or so years, the theoretical background of
relevant areas of language design (part II). The impact on functional programming, for example, of
the mathematical tools described in part II, is well known, as it ranges from the early dialects of Lisp,
to Edinburgh ML, to the current work in polymorphisms and modularity. Recent applications, such
as CAML, which will be described, use categorical formalization for the purposes of implementation.
In addition to its direct relevance to theoretical knowledge and current applications, category theory
is often used as an (implicit) mathematical jargon rather than for its explicit notions and results.
Indeed, category theory may prove useful in construction of a sound, unifying mathematical
environment, one of the purposes of theoretical investigation. As we have all probably experienced, it
is good to know in which ’category“ one is working, i.e., which are the acceptable morphisms and
constructions, and the language of categories may provide a powerful standardization of methods and
language. In other words, many different formalisms and structures may be proposed for what is
essentially the same concept; the categorical language and approach may simplify through abstraction,
display the generality of concepts, and help to formulate uniform definitions. This has been the case,
for example, in the early applications of category theory to algebraic geometry.
The first part of this book should encourage even the reader with no specific interest in
programming language theory to acquire at least some familiarity with the categorical way of looking
at formal descriptions. The explicit use of deeper facts is a further step, which becomes easier with
access to this information. Part II and some chapters in part I are meant to take this further step, at




II
least in one of the possible directions, namely the mathematical semantics of data types and programs
as objects and morphisms of categories.
We were urged to write the general introduction contained in part I, since most available books in
category theory are written for the ’working mathematician“ and, as the subject is greatly indebted to
algebraic geometry and related disciplines, the examples and motivations can be understood only by
readers with some acquaintance with nontrivial facts in algebra or geometry. For most computer
scientists, it is not much help in the understanding of ’natural transformations“ to see an involved
example based on tensor products in categories of sheaves. Thus our examples will be based on
elementary mathematical notions, such as the definition of monoid, group, or topological space, say,
and on structures familiar for readers with some acquaintance with the tools in programming language
semantics. In particular, partial orders and the various categories of domains for denotational
semantics will often be mentioned or introduced, as well as basic results from computability theory.
For example, we will try to present the fundamental operation of ’currying“ for cartesian closed
categories with reference to the connection between the universal function and the g del- numbering
of the partial recursive functions. Partial morphisms will be presented as a generalization of a
common notion in theory of computation.
Category theory may be presented in a very abstract way: as a pure game of arrows and diagrams.
It is useful to reach the point where acquaintance with the formal (essentially, equational) approach is
so firm that it makes sense independently of any ’structural“ understanding. In this book, though, we
will stress the role of structures, and we will always try to give an independent meaning to abstract
notions and results. Each definition and fact will be exemplified, or even derived, from applications
or structures in some way indebted to computing. However, in order to stress the role of the purely
equational view, the last chapters of each part (essentially chapters 7 and 11) will be largely based on
a formal, computational approach. Indeed, even if mathematically very abstract, the equational
arguments turn out to be particularly relevant from a computer science perspective.


The early versions of this book grew out of two graduate courses taught by Longo in Pisa, in
1984/85, and at Carnegie Mellon University, in 1987/88. Then the book was entirely revised under
the influence of Asperti•s work for his Ph.D. dissertation. In particular, chapters 7 and 11, the
technically most difficult, are part of his dissertation.
We are indebted to several people. The joint work with Simone Martini and Eugenio Moggi in
several papers directly influenced many chapters. Moreover, Eugenio suggested, in handwritten notes
and electronic mail messages, the basic ideas for the categorical understanding of polymorphism via
internal categories and realizability toposes. Their mathematical insights and suggestions also
influenced other parts of the book.
We must acknowledge the influence on our approach of the ideas and work of Dana Scott and
Gordon Plotkin, who also encouraged us and made comments on early drafts. Pino Rosolini helped




III
us with comments and many suggestions. Jean Yves Girard and Yves Lafont brought to our attention
the tidy categorical meaning of linear logic and its applications to computing. Roberto Amadio and
many students helped us by detecting errors and incompleteness in the presentation. We are looking
forward to aknowledge the readers who will detect the remaining errors.


The first draft of this book was completed while the authors were visiting Carnegie Mellon
University, in 1987/88. Longo would like to thank the Computer Science Dept. of CMU for its very
generous hospitality while he was teaching there that academic year. The circulation of the draft, its
complete revision, and the writing of the final version of the book have been made possible by the
Joint Collaboration Contract ST2J-0374-C (EDB) of the European Economic Community and by the
Italian CNR "Stanford-grant" #89.00002.26. The authors would like to thank INRIA, Rocquencourt,
for a postdoc granted to Asperti while completing this work and l•Ecole Normale SupŽrieure, Paris,
for inviting Longo to teach a graduate course in 1989/90 based partly on this book.




IV
TABLE OF CONTENTS


PART I: Categories and Structures

CATEGORIES ......................................................................................1
1.1 Category: Definition and Examples..................................................1
1.2 Diagrams................................................................................3
1.3 Categories out of Categories .........................................................4
1.4 Monic, Epic, and Principal Morphisms ............................................5
1.5 Subobjects .............................................................................8

CONSTRUCTIONS.............................................................................. 10
2.1 Initial and Terminal Objects ........................................................ 10
2.2 Products and Coproducts........................................................... 12
2.3 Exponentials.......................................................................... 15
2.4 Examples of CCC•s ................................................................. 20
2.4.1 Scott Domains ............................................................ 20
2.4.2 Coherent Domains........................................................ 24
2.5 Equalizers and Pullbacks ........................................................... 27
2.6 Partial Morphisms and Complete Objects........................................ 31
2.7 Subobject Classifiers and Topoi ................................................... 35

FUNCTORS AND NATURAL TRANSFORMATIONS ................................... 40
3.1 Functors .............................................................................. 40
3.2 Natural Transformations............................................................ 45
3.3 Cartesian and Cartesian Closed Categories Revisited ........................... 51
3.4 More Examples of CCC•s .......................................................... 54
3.4.1 Partial Equivalence Relations ........................................... 54
3.4.2 Limit and Filter Spaces .................................................. 55
3.5 Yoneda's Lemma .................................................................... 58
3.6 Presheaves............................................................................ 60

CATEGORIES DERIVED FROM FUNCTORS AND
NATURAL TRANSFORMATIONS........................................................... 63
4.1 Algebras Derived from Functors................................................... 63



V
4.2 From monoids to monads .......................................................... 67
4.3 Monoidal and monoidal closed categories ........................................ 72
4.4 Monoidal Categories and Linear Logic............................................ 79

UNIVERSAL ARROWS AND ADJUNCTIONS ............................................ 88
5.1 Universal arrows .................................................................... 89
5.2 From Universal Arrows toward Adjunctions .................................... 93
5.3 Adjunctions........................................................................... 97
5.4 Adjunctions and Monads ..........................................................104
5.5 More on Linear Logic ..............................................................110


CONES AND LIMITS ..........................................................................120
6.1 Limits and Colimits.................................................................120
6.2 Some Constructions Revisited ....................................................123
6.3 Existence of limits ..................................................................125
6.4 Preservation and Creation of Limits..............................................127
6.5 w-limits ..............................................................................130


INDEXED AND INTERNAL CATEGORIES...............................................132
7.1 Indexed Categories .................................................................132
7.2 Internal Category Theory ..........................................................136
7.3 Internal Presheaves.................................................................143
7.4 Externalization ......................................................................150
7.5 Internalization .......................................................................156
Appendix .................................................................................158



PART II: Types as Objects

FORMULAE, TYPES, AND OBJECTS .....................................................166
8.1 l-Notation...........................................................................167
8.2 The Typed l-Calculus with Explicit Pairs (lbhpt) ............................168
8.3 The Intuitionistic Calculus of Sequents ..........................................171
8.4 The Cut-Elimination Theorem.....................................................176
8.5 Categorical Semantics of Derivations ............................................185
8.6 The Cut-Elimination Theorem Revisited .........................................187
8.7 Categorical Semantics of the Simply Typed Lambda Calculus................191
8.8 Fixpoint Operators and CCCs.....................................................197



VI
REFLEXIVE OBJECTS AND
THE TYPE-FREE LAMBDA CALCULUS..................................................204
9.1 Combinatory Logic.................................................................206
9.2 From Categories to Functionally Complete Applicative Structures ...........208
9.3 Categorical Semantics of the l-Calculus.........................................214
9.4 The Categorical Abstract Machine ................................................217
9.5 From Applicative Structures to Categories ......................................220
9.6 Typed and Applicative Structures: Applications and Examples ...............225
Part 1: Provable isomorphisms of types .....................................226
Part 2: Higher type objects as models of the type-free l-calculus .........234


RECURSIVE DOMAIN EQUATIONS.......................................................241
10.1 The Problem of Contravariant Functors........................................242
10.2 0-Categories .......................................................................245


SECOND ORDER LAMBDA CALCULUS..................................................251
11.1 Syntax ..............................................................................252
11.2 The External Model ...............................................................254
11.3 The External Interpretation.......................................................257
11.4 The Internal Model................................................................258
11.5 The Internal Interpretation........................................................261
11.6 Relating Models ...................................................................263

EXAMPLES OF INTERNAL MODELS .....................................................272
12.1 Provable Retractions..............................................................272
12.2 PER inside w -Set..................................................................275
12.3 PL-Categories Inside Their Groethendiek Completion .......................277


BIBLIOGRAPHY ...............................................................................283




VII
1. Categories


Chapter 1


CATEGORIES

Category Theory studies ’objects“ and ’morphisms“ between them. These concepts are both
primitive in Category Theory: objects are not collections of ’elements,“ and morphisms do not need
to be functions between sets (thus morphisms cannot be applied to ’elements“ but only composed
with other morphisms). Any immediate access to the internal structure of objects is prevented: all
properties of objects must be specified by properties of morphisms (existence of particular
morphisms, their unicity, validity of some equations among them, and so on). This is quite similar to
considering objects as ’abstract data types,“ that is, data specifications that are independent of any
particular implementation. The relevance of Category Theory for programming languages comes
from the previous consideration: it offers a highly formalized language especially suited for stating
abstract properties of structures. Thus, it relates to widely used programming methodologies and
provides as well a formal setting for the mathematical investigation of the semantics of programming
languages.




1.1 Category: Definition and Examples
As we have mentioned, Category Theory is a theory of functions, and the only basic operation is
composition. The concept of Category embodies some abstract properties of the composition
operator ’»“ for functions that ’reasonably“ must be guaranteed. In particular, if g: a®b and h:
b®c, then there exist h » g: a®c; moreover, composition must be associative and an identity must
exist for all objects.
This is the formal definition:


1.1.1 Definition A category C is
- a collection ObC of objects, denoted by a, b . . . A, B . . .
- a collection MorC of morphisms (arrows), denoted by f, g . . . ,
- two operations dom, cod assigning to each arrow f two objects respectively called domain
(source) and codomain (target) of f
- an operation id assigning to each object b a morphism idb (the identity of b) such that
dom(idb) = cod(idb) = b
- an operation ’ » “ (composition) assigning to each pair f, g of arrows with dom(f) = cod(g) an
arrow f » g such that dom( f » g ) = dom(g), cod( f » g ) = cod(f)
- identity and composition, moreover, must satisfy the following conditions:



1
1. Categories


identity law: for any arrows f, g such that cod(f) = b = dom(g)
idb » f = f
g » idb = g
associative law: for any arrows f, g, h such that dom(f) = cod(g) and dom(g) = cod(h)
(f»g)»h=f»(g»h)


We write f: a ® b to denote a morphism whose source and target are respectively a and b. Given
two objects a and b, the collection of all morphisms f such that f: a ® b is denoted by C[a,b]; the
writing fÎC[a,b] is thus a third way to express the fact that dom(f) = a, and cod(f) = b. For the
moment we shall use one notation or the other indifferently
The following table lists some common categories by specifying their objects and arrows, letting
the definition of their operators as an exercise for the reader:


Category Objects Morphisms

Set sets functions
Top topological spaces continuous functions
Vect vector spaces linear transformations
Grp groups group homomorphisms
PO partially ordered sets monotone functions


The intuition of the notion of ’category“ suggested by the previous examples is to consider the
objects as a collection of ’structured“ sets and the morphisms as the ’associated“ or ’acceptable“
functions with respect to the structure. This is too restrictive, though, since no requirement is made in
the definition which may force the morphisms to be ’single valued“ or to be functions in extenso: a
simple example is the category Rel with sets as objects and relations as morphisms.
The simplest category has only one object and one arrow (the identity for that object): this
category is usually called 1. Note that, by definition, if C is a category, then every object b of C
has an identity idb: b®b. The identity is unique, since if idb' is another identity for b, then for
the identity law, idb' = idb ° idb' = idb . A category is called discrete if every arrow is the identity
of some object: in this case a category is fully determined by the collection of its objects. 1 is a
discrete category.
A category is called a preorder if for every pair of objects a, b there is at most one morphism
f: a®b. The reason for the name is that a preorder category is fully determined by a preordering
relation among its objects. Indeed, in a preorder C, there is only one way that composition may be
defined; thus C is known when the collection of morphisms MorC and the operations dom and cod
are known. But every arrow f: a®b may be identified with the pair (a,b), since once the source and



2
1. Categories


target are known there is no choice about what the arrow is to be; thus, all the information about the
category C is given by the relation RC = {(a,b) / there is an arrow fÎC[a,b]}, that is, by a preorder
relation.(Exercise: prove that the relation RC is a preorder for every category C ).
Every discrete category is a preorder. The simplest nondiscrete category which is a preorder is
the category 2, which has two objects, let us call them 0 and 1, and three arrows: the two identities
id0 , id1 and an arrow (0,1): 0®1. In a similar way we can define for each natural number n a
preorder category n, from the usual ordering on the set {0,1, . . . n-1}. Preorder categories have a
common property: they may have plenty of objects, but given two objects, there exists at most one
morphism between them.
A dual situation is given by monoids, viewed as categories. A monoid is a set having an
associative binary operation and an identity element. A category with just one object yields a monoid,
where composition of morphisms is the binary operation. Conversely, any monoid (A, . ) is a
category with just one object. For example, the category with the set of natural numbers as unique
object and the recursive functions as morphisms yields the monoid of the recursive functions.
As well as preorders, another example where objects are not necessarily understood as
’structured sets“ is given by deductive systems as categories. In these categories propositions are
objects and each morphism f : a®b corresponds to (a suitable equivalence class of) a proof of a |-
b (a entails b). Observe that a category is obtained easily in the presence of the identical entailment
ia : a®a and the associative composition of proofs
f : a®b g : b®c
________________
g ° f : a®c
This approach to deduction is very relevant in the categorical understanding of logics of a
constructive nature, such as Intuitionistic Logic, where the intended interpretation of proofs is given
by (effective) operations. It will be the main paradigm for understanding the relation between types
and objects investigated in the second part of this book.




1.2 Diagrams
An important tool in the practice of Category Theory is the use of diagrams for representing
equations. In a diagram a morphism fÎC[a,b] is drawn as an arrow from a to b labeled f. A diagram
commutes if the composition of the morphism along any path between two fixed objects is equal.
For example, the associative and identity laws of the definition of ’category“ may be nicely visualized
by the following commuting diagrams:




3
1. Categories




Diagrams are a typical way, in Category Theory, to describe equational reasoning and turn out to
be particularly effective when dealing with several equations at a time. In particular, assertions such
as ’if diagram 1 and . . . diagram n commute, then diagram commutes“ express conditional
statements about equalities.
We hope that the reader, while using this book, will acquire some familiarity with diagrams and
will learn how to go back and forth from diagrams to equations. Our extended use of equations in
this book comes from our desire to stress the ’computational“ nature of most categorical reasoning.




1.3 Categories out of Categories
A main feature of Category Theory is the facility to define new, more structured categories out of
simpler ones. In this section we consider only a few simple constructions; a number of other
examples occur throughout the book.


1.3.1 Definition A category D is a subcategory of a category C, if
1. ObD Í ObC;
2. for all a, b in ObD, D[a,b] Í C[a,b];
3. composition and identities in D coincide with those of C.
A subcategory is full if for all a, b in ObD D[a,b] = C[a,b].


A full subcategory is fully determined by its collection of objects.


1.3.2 Definition The dual category C op of a category C has the same objects and the same
morphisms of C, idopb = idb, domop(f) = cod(f), codop(f) = dom(f), and f °op g = g ° f.


Note that Cop[b,a] = C[a,b] and (Cop)op = C.

Exercise Setop is a subcategory of Rel, but not of Set. Is it a full subcategory?


Duality is a very powerful technique of Category Theory. If P is a generic proposition expressed
in the language of Category Theory, the dual of P (Pop) is the statement obtained by replacing the




4
1. Categories


word ’dom“ by ’cod,“ ’cod“ by ’dom,“ ’g ° h“ by ’h ° g.“ If P is true in a category C, then Pop
is true in Cop; if P is true in every category, then also Pop is, since every category is the dual of its
dual.
Duality may be applied to diagrams as well: given a diagram in a category C, the dual diagram in
Cop is obtained by simply reverting the arrows; of course, a dual diagram commutes if and only if
the original one does.


1.3.3 Definition Given two Categories C and D, the product category C´ D has for objects
´
the pairs (a,b) where a and b are respectively objects of C and D, and for morphisms pairs (f,g):
(a,b)®(a',b') where f: a®a' and g: b®b' are respectively morphisms of C and D. Finally, id(a,b)
= (ida,idb) and (f,g) ° (f',g') = (f ° f', g ° g').


1.3.4 Definition Given a category C and an object a in ObC , the category C¯a of objects
over a is so defined: ObC¯a = {fÎMor C / cod(f) = a}; given two objects f: b®a, g: c®a, a
morphism with source f and target g is an arrow hÎC[b, c] such that g ° h = f. Identities and
composition in C¯a are inherited from C.


In case C is Set in the above definition, it is useful to think of an object g: B®A in Set¯A as an
A-indexed family of disjoint sets, namely, {g-1(a)}aÎA (these sets are the inverse images of
elements in A under g). Then h: B®B' is a morphism from g: B®A to g': B'®A if and only if
it is consistent with the ’decomposition“ of B and C induced by g and g', i.e., if and only if (iff)
"b bÎg-1(a) Þ h(b)Îg'-1(a).
Since the intended meaning behind the construction of a category C¯I is that to consider an
object g: A®I as a collection {{i}´g -1 (i)} iÎI , it is usual to call C¯I a slice category over I
(denoted C/I). An object g: A®I of the slice category is then called a generalized object of C at
stage I. A section of g: A®I is a function s: I®A such that g ° s = idI; the idea is that s gives,
for each index iÎI, an element s(i)Îg-1(i).


Exercise Define the dual notion, that is, the category C-a of objectsunder a, whose objects are
the arrows with source a.




1.4 Monic, Epic, and Principal Morphisms
A function f between two sets A and B is called ’injective“ when, for all a , a' Î A , if f(a) =
f(a') then a = a'. In particular, given any two functions g, h : C®A, if for all cÎC f(g(c)) =
f(h(c)), then for all cÎC g(c) = h(c) or, also, if f ° g = f ° h then g = h . Thus, every injective
function behaves like a left identity (it is left cancellable). The converse is also true: given f: A®B, if



5
1. Categories


for any pair of functions g, h : C®A , f ° g = f ° h implies g = h , then f is injective. For suppose
otherwise: then there are a and a' such that f(a) = f(a') but a ¹ a' ; define then g and h by g(c)
= a for all cÎ C , and h(c) = a' for all cÎ C; of course f ° g = f ° h but g ¹ h , that is, a
contradiction.
We have proved thus that a function f is injective if and only if f ° g = f ° h implies g = h . In a
similar way it is not difficult to prove that f is surjective if and only if g ° f = h ° f implies g = h.
These considerations motivate the following definitions.

1.4.1 Definition. Let C be a category and a, bÎOb C . Then
i. an arrow hÎC[a,b] is epic (is an epimorphism) iff
g»h=f»h Þ g=f;
ii. an arrow hÎC[a,b] is monic (is a monomorphism) iff
h»g=h»f Þ g=f;
iii. an arrow hÎC[a,b] is iso (is an isomorphism) iff there exists gÎC[b,a] such that
g » h = id and h » g = id .

Two objects a and b are isomorphic (a @ b) if there exists an isomorphism hÎC[a,b]. Clearly,
any isomorphism is monic and epic; the converse, though, does not need to be true (see the example
and the exercises below).
A monic (or epic) hÎC[a,b] (or h'ÎC[a,b]) is split if there exist gÎC[b,a] (or g'ÎC[b,a])
such that g » h = id (h' » g' = id).
Although the intuition of regarding mono- and epimorphisms as injective and surjective maps is
correct for many interesting categories, sometimes it can be misleading. Consider, say, the category
Mon of monoids and the inclusion inc from w, the positive integers, into z, the relative ones. Clearly
mono, inc is also epi, though. As a matter of fact, take g,hÎMon[z,a] for some monoid a, and write
\g(n) for g(-n). Then g » inc = h » inc implies g = h for g(-n) = \g(n) =\h(n) = h(-n) (that is, the
behavior of the monoids• homomorphism g or h on z is entirely determined by their behavior on
w). As a side consequence, we may also conclude that not every arrow that is both monic and epic is
an isomorphism: this is clearly in contrast to the set-theoretic intuition.

Exercises
1. Give an epi which is not surjective in Top.
2. Find a counterexample for the following assertion: let C be a category; if fÎC[a,b] and gÎC[b,a]
are mono, then a is isomorphic to b. (Note that the assertion is true in Set.)
3. Prove that a split monic is an iso.

1.4.2 Definition Let C be a category and a, bÎObC. Then
i. an arrow hÎC[a,b] is a principal morphism iff




6
1. Categories


"fÎC[a,b] $gÎC[a,a] f = h» g ;
ii. a pair of arrows fÎC[a,b] and gÎC[b,a] is a retraction pair iff g » f=id. Then, a is called a
retract of b (a<b) via the retraction pair (f,g).

By diagrams, h is principal iff for all f there is a g such that




Principal morphisms have been inspired by recursion theory; the idea they are based on essentially
corresponds to a classical notion of reducibility (see the category EN in section 2.2 below).

1.4.3 Proposition Let C be a category and a, bÎObC . Then
1. if a<b via (i,h), then h is epi and principal, i is mono;
2. if hÎC[a,b] is principal and there exists an epi kÎC[a,b,], then h is epi;
3. if a<b and fÎC[b,a] is principal, then there exists gÎC[a,b] such that a<b via (g,f).
Proof 1. g»h = f»h Þ g»h»i = f»h»i Þ g = f, for h»i = id.
The proof that h is principal is a simple diagram chase:




That is, "f $g f = h»g. Just take g = i»f; then h»g = h»i»f = f.
Finally, i»g = i»f Þ h»i»g = h»i»f Þ g = f.
2. g»h = f»h Þ g»k = g»h»g' = f»h»g' = f»k (for a suitable g') Þ g = f .
3. Let a<b via (j,i). Since f is principal, $sÎC[b,b] j = f°s. Then, for g = s°i, one has f°g = j°i =
ida. As a diagram,




¨




7
1. Categories


Exercises
1. Characterize retractions in terms of split monos and epis.
2. Show that, given a category C, one can define a category CRet whose objects are the same of C
and whose morphisms are retraction pairs in C, that is FÎCRet[a,b] iff F=(f,g) and a<b via (f,g) in
C.


If (f:a®b, g:b®a) is a retraction pair, then the function h = f ° g: b®b is idempotent, that is, h ° h
= h . Indeed, h ° h = (f ° g) ° (f ° g) = f ° (g ° f) ° g = f ° g = h . This property suggests the following
definition:

1.4.4 Definition Given a category C and an object bÎOb C , the category of idempotents on
b (Retb) is so defined:
ObRetb = { fÎC[b,b] / f ° f = f }
MorRetb = { (f, k, g) / f, gÎObRetb, kÎC[b,b], k = g ° k ° f }
dom( (f, k, g) ) = f, cod( (f, k, g) ) = g
idf = (f, f, f)
(f, k, g) ° (g', k', f) = (g', k ° k', g)


We leave as an exercise for the reader to check the identity and associative laws for the previous
category. Retb will be used in several places because of its relevance to this book.




1.5 Subobjects
The concept of subobject is the categorical version of the set-theoretical subset . The main idea is to
regard a subset A of a given object B as a monomorphism f: D®B (intuitively, a monomorphism
f such that ’f(D) = A“). Of course, many different monic arrows may define the same subset; thus,
it is necessary to introduce a reasonable equivalence relation, and define subobjects up to this
equivalence.
Let C be a category. If f: b®a and g: c®a are two monic arrows with common target a, then
we say f £ g if and only if there exists h: b®c such that g ° h = f. Note that in this case, the unique
h must be monic too, indeed h ° k = h ° k' Þ g ° h ° k = g ° h ° k' Þ f ° k = f ° k' Þ k = k'.


Exercise Prove that the preorder £ is the full subcategory of C¯a determined by monomorphisms
only.




8
1. Categories


When f £ g and g £ f we write f @ g. Then @ is an equivalence relation among the
monomorphisms with common target a (prove it as an exercise); the equivalence classes of this
equivalence relation are called subobjects of a.

1.5.1 Definition Let a be an object of a category C. A subobject [f] of a is an equivalence
class of a monomorphism f: b®a, with respect to the equivalence relation @ defined above.


Very often, we shall make no distinction between equivalence classes and their representatives, and
we shall denote a subobject with a single monomorphism.
It should be clear that the categorical approach to ’subsets“ carries more information than the set-
theoretic one. Monomorphisms, like all morphisms, preserve the structural information of the
category. For example, in the category Grp of groups subobjects are subgroups: (mono)morphisms
must take the identity to the identity and preserve the group operation. Similarly consider the category
of p.o.sets (partially ordered sets) with a bottom element. A subobject of one such p.o.set must be a
structured subset as well, and it must contain an element smaller than all the others.



References: Any book in Category Theory, such as MacLane (1971) Herrlich and Strecker
(1973), Arbib and Manes (1975), Barr and Wells (1985), Rydeheard and Burstall (1988). The
specific notions and categories introduced (such as retractions) will be used later in more structured
settings, with the appropriate references.




9
2. Constructions


Chapter 2


CONSTRUCTIONS

In this chapter we consider some fundamental categorical constructions, i. e., particular objects (and
morphisms) that satisfy a given set of axioms described in the language of Category Theory. Since in
this language there is no way to look at the internal membership structure of objects, all the concepts
must be defined by their relations with other objects, and these relations are established by the
existence and the equality of particular morphisms. This property of the categorical language, if
compared to the traditional set-theoretic jargon, may be well understood by an analogy with computer
science; namely, as we already mentioned, the categorical description corresponds to an abstract data
specification, while the traditional set-theoretic approach is more similar to a concrete implementation.




2.1 Initial and Terminal Objects

2.1.1 Definition Let C be a category. An object 0 is initial iff for any bÎObC there is a unique
fÎC[0,b].

The typical example of an initial object is the empty set Æ in Set; indeed the empty function (i.e., the
function whose graph is empty) is the unique arrow with Æ for source.
A more interesting example is the following. Let S be a signature. The class AlgS of S -algebras
with S-homomorphisms as arrows forms a category. AlgS has an initial object TS which is called S-
word-algebras, or also Herbrand Universe for S . The set TS,s (the carrier of TS of sort s) is just the
set of all well-formed expressions of sort s. If S is derived by a context free grammar (that is: sorts
are nonterminals and operator symbols are productions of the grammar), then TS ,s is the set of all
parse trees for derivations in the grammar from the nonterminal s. In general the initial S-algebra TS
corresponds to the syntax of a language of signature S. Any other S-algebras A in AlgS is a possible
semantic domain; the semantic function (interpretation) is the unique homomorphism from TS to A.
Initiality is the simplest universal notion in Category Theory, since it is given by the existence and
unicity of morphisms satisfying certain properties. This method is used everywhere in Category
Theory.


2.1.2 Proposition If 0 and 0' are two initial objects in a category C, then they are isomorphic.




10
2. Constructions


Proof. Let i: 0®0', j: 0'®0 the morphisms respectively given by the initiality of 0 and 0'. Then
j ° i: 0®0, but also id0: 0®0, and since by initiality of 0, there is exactly one morphism in C[0,0],
then j ° i = id0; in the same way, by initiality of 0' we have i ° j = id0'.¨

We will now show how duality can be used to define new concepts and to prove new assertions.
Let P(c) be the property ’for any bÎObC there is a unique f, such that dom(f) = c, cod(f) = b.“ By
definition c is initial iff P(c) holds; that is, P defines initiality. The dual statement of P is Pop(c) =
’for any bÎObC there is a unique f, such that cod(f) = c, dom(f) = b.“ Usually the dual Qop of a
property Q defines a concept named by prefixing ’co-“ to the name of the property Q. In our case, we
say that Pop defines coinitiality. An object c such that Pop(c) holds, is called co-initial. Anyway it
is common practice to assign to every coentity an independent name which better expresses its
properties; for example, a coinitial object is known as terminal object. Note that an initial object is
coterminal.
Terminal objects are usually represented with the number 1 or with the letter t. The unique
morphism from an object a to the terminal object t is usually written !a: a®t.
Any singleton set is terminal in Set. In the category 2 one object is initial and the other one is
terminal. If c is initial in C, then it is terminal in the dual category Cop.
Consider now the statement P1 = ’If 0 and 0' are two initial objects, then they are isomorphic.“
Its dual is: P1op = ’If 0 and 0' are two terminal objects, then they are isomorphic.“ (the property
to be an isomorphism is the dual of itself: prove it as an exercise.) By our discussion of duality in
chapter 1 and, since by proposition 2.1.2 P1 holds in every category, P1op also does. We conclude
the following:

2.1.3 Proposition If 0 and 0' are two terminal objects in a category C, then they are
isomorphic.
Proof By duality and by proposition 2.1.2.¨


An object c in a category C may be both initial and terminal. An example is the unit group in Grp;
in this case, it is called a zero object.
In Set, a morphism from the singleton {*} to a set A defines an element of A. For this reason an
arrow from a terminal object t to an object a in a generic category C is usually called an element
or a point of a. In this case, however, the set-theoretic intuition must be used very carefully, because
it is quite common to work in categories where the categorical notion does not reflect the behavior of
elements in Set. For example the set-theoretic intuition would suggest that every non-initial object
must have at least one element: but consider the partial order category 3 which has three object 0 £
1 £ 2; clearly 0 is initial and 2 is terminal, 1 is non-initial but has no elements. Similarly, in Set
two arrows are equal iff they coincide on all points, or, more formally, given functions f and g,



11
2. Constructions


one has f ¹ g iff there is an element x of their domain such that f ° x ¹ g ° x. However, in a
generic category C with terminal object t, this is not necessarily true.


2.1.4 Definition. Let C be a category. tÎOb C is a generator iff for all a,bÎOb C and all
f,gÎC[a,b], one has: f ¹ g Þ $hÎC[t,a] f°h ¹ g°h .
C has enough points (or is well pointed), if there exists a generator t that is terminal in the
given category.


In short, a category has enough points when the arrows from the terminal object allow to discriminate
between morphisms, similarly as for elements over Set. Of course, it is not a surprise that the set-
theoretic notions of ’element“ and of ’extensionality“ are somewhat awkward to deal with in the
language of Category Theory.




2.2 Products and Coproducts
The categorical product is merely a ’structural“ generalization of the notion of Cartesian product of
sets. Given two sets A and B, their cartesian product is:
A´B = {<x,y> / xÎA, yÎB}
Associated with this set there are two special maps pA: A´B®A , pB: A´B®B called projections,
such that for every <x,y> in A´B pA(<x,y>) = x, pB(<x,y>) = y. Note that for every c in A´B,
<pA(c), pB(c)> = c.
Let C be another set, and f: C®A, g: C®B. Define <f,g>: C®A´B by <f,g>(c) = <f(c),g(c)>
for every cÎC. Then, for every cÎC, pA( <f,g>(c) ) = pA( <f(c),g(c)> ) = f(c), that is, pA ° <f,g>
= f. In the same way, we obtain pB ° <f,g> = g. Conversely, let h: C®A´B. Then for every cÎC,
<pA ° h, pB ° h >(c) = <pA(h(c)), pB(h(c))> = h(c), that is, <pA ° h, pB ° h > = h.
The previous consideration suggests the following definition:

2.2.1 Definition Let C be a category, and a,bÎOb C . The categorical product of a and b is
an object a´b together with two morphisms pa: a´b®a, pb: a´b®b, and for every object c an
operation < , >c : C[c,a]´C[c,b]®C[c,a´b] such that for all morphisms f: c®a, g: c®b, h:
c®a´b, the following equations hold:
ia. pa ° <f,g>c = f ;
ib. pb ° <f,g>c = g ;
ii. <pa ° h, pb ° h >c = h .


It is common practice to omit the subscript c in < , >c when its meaning is clear from the context.




12
2. Constructions


The operation < , > : C[c,a]´C[c,b]®C[c,a´b] of a categorical product is a bijection: its inverse
is the operation that takes every arrow hÎC[c,a´b] to the pair (pa ° h, pb ° h )ÎC[c,a]´C[c,b].
The proof that these operations are inverse of each other is stated above in definition 2.2.1.
Conversely, given a bijective operation < , > : C[c,a]´C[c,b]®C[c,a´b] which satisfies (ia) and
(ib), then (ii) is necessarily true. Indeed, let hÎC[c,a´b]. Then, since < , > is bijective, there is a
pair (f,g)ÎC[c,a]´C[c,b] such that h = <f,g>; but f = pa ° <f,g> = pa ° h and analogously, g = pb °
<f,g> = pb ° h; thus, h = <pa ° h, pb ° h >.
The last consideration leads us to a more compact but equivalent definition of a categorical
product.

2.2.2 Definition Let C be a category, and a,bÎOb C . The categorical product of a and b is
an object a´b together with two morphisms pa: a´b®a , pb: a´b®b, such that, for any fÎC[c,a]
and gÎC[c,b], there exists exactly one hÎC[c,a´b] such that the following diagram commutes




2.2.3 Definition For fÎC[a,c] and gÎC[b,d], set f´g = <f»pa,g»pb> : a´b® c´d.


Exercise Prove that for all arrows h: e®a and k: e®b, f´g»<h,k> = <f»h,g»k>.


2.2.4 Proposition In a category, the product is unique (up to isomorphisms), if it exists.
Proof Let a„b be an alternative product with projections qa and qb.
Then <qa,qb> » <pa,pb> is the unique morphism such that the following diagram commutes:




13
2. Constructions


Since ida´b also does the same job, ida´b = <pa,pb>»<qa,qb>.
By symmetry, one also has <pa,pb> » <qa,qb> = ida’„b .¨

Exercise. Prove the following facts:
1. a @ a' and b @ b' imply a´b @ a'´b'.
2. a´b @ b´a.

2.2.5 Definition A category C is Cartesian (C is a CC) iff
i. it contains a terminal object t;
ii. every pair a,bÎObC has a categorical product (a´b, pa,b,1: a´b®a, pa,b,2: a´b®b)

Exercises
1. Generalize the definition of a product of two objects to arbitrary products.
2. Prove that a Cartesian category C always contains all finite products.
3. Let C be a CC and let t be its terminal object. Prove that for all b in ObC, b @ t´b @ b´t .

Examples The categories Set, Top, Grp are all Cartesian.
An interesting Cartesian category in Computability Theory is the category EN of numbered sets.
Objects in EN are pairs a = (a,ea), where a is a countable set and ea: w®a is an onto map (an
enumeration of a). fÎEN[a,b] iff for some total recursive f' the following diagram commutes:




We say that f' represents f. The product is easily obtained by using any effective pairing of w2,
[,]: w´w®w.
A typical numbered set which is worth studying is PR = (PR,f), the partial recursive functions
with a Goedel numbering f: w®PR. Then EN[PR,PR ] are exactly the type two recursive
functionals. Of course, this is also a countable set. It is not trivial, though, to construct an
’acceptable“ enumeration of it. This will be an important issue in the sequel.

Exercises
1. Let w = (w,id) in EN. Then fÎEN[w,PR] iff $f'ÎPR f'([x,y]) = f(x)(y). Moreover, gÎ
EN[w,PR] is principal iff g is an acceptable Goedel numbering of PR, in the sense of classical
recursion theory.



14
2. Constructions


2. Let C be a CC, and V be an object such that V´V<V. Then the category of retractions on V (see
definition 1.4.4 ) is a CC.


The dual of the notion of a product is the coproduct a+b with embeddings q1, q2.

2.2.6 Definition. Let C be a category, and a,bÎOb C . The coproduct of a and b is an object
a+b together with two morphisms qa: a®a+b, qb: b®a+b such that, for any fÎC[a,c] and
gÎC[b,c], there exists exactly one hÎC[a+b,c] such that the following diagram commutes




By duality, the coproduct is unique (up to isomorphisms).


Examples
1. In Set the coproduct is the disjoint union.
2. In a preorder P the product is the greatest lower bound, if it exists. The coproduct is the least
upper bound, if it exists.
3. Let CPO be the category of complete partial orders with continuous functions with respect to the
order or Scott topology. CPOS is the subcategory with only strict functions, i.e., morphisms always
take the least element ^ to the least element of the target space. It is easy to see that both categories
are Cartesian. The coproduct in CPOS is given by the coalesced sum, i.e., the disjoint union except
for the identification of the two least elements. On the other hand, there is no coproduct in CPO.
This may be seen by observing that in CPO one may have f( ^ ) ¹ g( ^ ), by which the coalesced
sum fails to give a coproduct; an extra common least element (disjoint sum) may give more than one
extension of the required <f,g>op.




2.3 Exponentials
In the connection we mentioned between Category Theory and Computation Theory, as ’theories of
functions,“ a fundamental aspect still has to be taken care of. In either case, we may be interested in
computing with procedures as arguments. That is, we may need to describe higher type functions.
So far we have only become familiar with Cartesian categories, where the object a´b, representing
the product, is defined. Thus, the notion of morphism taking morphisms as arguments doesn't yet
make sense. What we first need, then, is a further closure property, namely, the existence within the



15
2. Constructions


category of an object ba which suitably represents the set of morphisms from b to a. With an
informal reference to typing in programming, the key property of the objects, which represent the
sets of morphisms, provides an interpretation to a common construct in actual programming, namely,
the identification of types such as A´B®C and A®(B®C). This corresponds to the following
important uniformity property of programs of several arguments, which is directly inherited from
classical Recursion Theory.
Let {fi}iÎw = PR be an acceptable Gšdel numbering of the partial recursive functions and [,]:
w´w®w be an effective pairing. Define then, as usual, f: w´w®w is a binary partial recursive
function iff $f'ÎPR f(x,y) = f'([x,y]) (similarly, for n-ary functions, n ³ 2). By this and by the
s-m-n iteration theorem one immediately has f: w´w®w is partial recursive iff $sÎR fs(x)(y) =
f(x,y).
Thus, a two-(or more) argument function f is computable iff it is computable in each argument
and the function x |_ f(x,_) is also ’computable,“ i.e., $sÎR fs(x) = f(x,_). In other words, in
computability theory, f is in w´w®w iff x |_ f(x,_) is in w®(w®w). Similarly, the category-
theoretic closure property we need concerns the existence, for any f: c´a®b, of a morphism within
the category, which does the same job as s or x |_ f(x,_) in recursion theory. We will call it L(f).


Exercise For n ³ 2, not every n-ary function which is computable in each argument needs to be
computable. (Hint: take g total nonrecursive and set f(x,y) = g(min{x,y}) ).

2.3.1 Definition Let C be a Cartesian category, and a,bÎOb C . The exponent of a and b is
an object ba together with a morphism evala,b: ba´a®b (evaluation map), and for every object c an
operation Lc : C[c´a,b]®C[c,ba] such that for all morphisms f: c´a®b, h: c®ba, the following
equations hold:
b). evala,b ° (L(f)´ida) = f ;
h) . Lc(evala,b ° (h´ida)) = h .
(We may omit the indices when unambiguous, as usual.)


In Set the exponent set of A and B is BA = {f / f is a function from A to B}, thus BA =
Set[A,B]. The function eval: BA´A®B is given by the rule: eval(<f,x>) = f(x) .
L: Set[C´A,B]®Set[C,BA ] takes every function f: C´A®B to the function L(f): C®B A
defined by L(f)(c) = la.f(c,a), where la.f(c,a)ÎBA=Set[A,B] is the function which takes aÎA to
f(c,a)ÎB. The proof of (b) and (h) is almost immediate.
As in the case of the product, observe that in general the operation L: C[c´a,b]®C[c,ba] in
definition 2.3.1 is a bijection. Indeed, by (b) and (h), L -1 is the operation which takes every
hÎC[c,ba] to evala,b ° (h´ida)ÎC[c´a,b].




16
2. Constructions


Conversely, if L : C[c´a,b]®C[c,ba] is a bijection and (b) holds, then (h) is necessarily true.
Indeed, let hÎC[c,b a ] and take fÎC[c´a,b] such that h = L(f); then L(eval a,b ° (h´id a )) =
L(evala,b ° (L(f)´ida)) = L(f) = h .
The following is thus an equivalent definition of ’exponent“:

2.3.2 Definition Let C be a Cartesian category and a,bÎObC. The exponent of a and b is an
object ba together with a morphism evala,b: ba´a®b, such that for all morphisms f: c´a®b, there
exists one and only one h: c®ba such that the following diagram commutes:




Exercise By setting L(f) = h, give the details of the equivalence proof between the two definitions.


The previous diagram should suggest in which sense ba ’represents“ C[a,b]. The eval morphism
generalizes the set-theoretic evaluation function eval(f,x) = f(x). Moreover, take c = t, the terminal
object. Then C[t,ba] @ C[t´a,b] @ C[a,b] as sets. This is particularly significant if C has enough
points (why?).


2.3.3 Definition. C is a Cartesian closed category (CCC) iff
1. C is cartesian,
2. for every pair a,bÎObC, there is an exponent.

Set is a CCC: the previous definition of exponents in Set clearly holds for every pair of sets.
Another simple CCC is CPO, the category of complete partial orders and continuous maps. As well-
known, given c.p.o.•s a and b, CPO[a,b] is also a c.p.o., with respect to the pointwise ordering.
Moreover, both eval and L(f), defined as for Set by using continuous functions, are continuous
and satisfy the required conditions. Note that the proof uses the well-known fact that in CPO a
function is continuous iff it is so in each argument and the map x |_ ly.f(x,y) is continuous.
Actually, even L is continuous.
Among the various examples of categories mentioned in these notes, an important one does not
satisfy Cartesian closedness: the category EN in section.2.2. Consider, say, w = (w,id). Then
EN[w,w] (= R, the recursive functions) is surely countable. However, if a numbered set (ww,j) and




17
2. Constructions


a morphism eval with the above properties existed, then u(x,y) = eval(j(x),y) would be a universal
function for R.
Also, the w-algebraic c.p.o.•s, that is, the c.p.o.•s with a countable collection of compact elements
approximating all the others (see Scott domains below) and continuous maps as morphisms do not
form a CCC. They contain, though, some fundamental subCCC's for the purposes of denotational
semantics of programming languages and higher type Recursion Theory. They will be explored in the
examples below.
Given a CCC D, it may be interesting to consider specific "structures of types" in it. That is, for a
collection A of objects in D, let DA be the full sub CCC generated by A in D, i.e., the least full
sub category such that AÍDA and a,bÎDA Þ a´b,abÎDA.


Exercise Prove that in any CCC one has ab´c @ (ab)c.


In definition 1.4.2, we introduced the notion of ’retract“: in a category C, a<b via the retraction
(i,j) iff j » i = ida. In these assumptions, i turns out to be mono and j epic. Thus, a retract a of
b is a subobject of b in the sense of section 1.5. In the case of Set, nonempty subsets and retracts
happen to coincide, as surjections from a set to a subset are always possible. In more structured
categories this reinforcement of the idea of subset, given by retractions, turns out to be very
informative. In particular, we will discuss categories with nontrivial objects a such that aa<a. This
is clearly impossible in Set because, by Cantor•s theorem, the cardinality of the exponent aa , when
a is not a singleton, is strictly bigger than the cardinality of a. In short, we will put together retracts
and exponents, in a nontrivial way, in order to discuss one of the early relevant applications of
categorical notions to computer science, namely the invention of mathematical (categorical, to be
precise) models of type-free languages. In these languages, programs are viewed as data or,
semantically, exponents may be retracted into (source and target) objects. It is convenient to prove, in
general, some basic properties of exponents and retractions for their relevance and simplicity as well
as for some preliminary training on equational reasononing, which will turn out to be useful to the
reader in the sequel.


2.3.4 Proposition Let C be a CCC. If a<a' (via ina : a®a', outa : a'®a), and b<b' (via inb :
b®b', outb: b'®b), then ba<b'a', via L(inb°eval°(id´outa)): ba®b'a', L(outb°eval°(id´ina)):
b'a'®ba.
Proof. L(outb°eval°(id´ina)) ° L(inb°eval°(id´outa)) =
= L(outb°eval°(id´ina)°L(inb°eval°(id´outa))´id )
= L(outb°eval°L(inb°eval°(id´outa))´id°(id´ina) )
= L(outb°(inb°eval° id´outa )°(id´ina) )
= L(eval ° id´(outa°ina) )



18
2. Constructions


= L(eval ° id´id)
= id. ¨


2.3.5 Definition Let C be a CCC. An object V of C is reflexive iff VV <V.

Before we get to see some reflexive objects in relevant CCC's in the following sections, it is worth
proving two simple, but general, properties of reflexive objects (see chap.8 for applications).


2.3.6 Proposition Let C be a CCC, and V a reflexive object. Then t < V and V´V < V .
Proof. Let (in: VV®V, out: V®VV) the retraction pair between VV and V. In order to prove that
t<V we must only prove the existence of a morphism from t to V (why?). Let then p1: t´V®V be
the projection; L(p1): t®VV, and thus in ° L(p1): t®V.
The proof that V´V<V is much more complex; we prove that V´V<VV; then V´V<V follows by
composition.
Let app = eval°(out´idV ): V´V®V, and let a a,b,c be the isomorphism a a,b,c: (b´c)´a®
(a´b)´c. Then: app ° (app´id) ° aV,V,V : (V´V)´V®V
in1 = L( app ° (app´id) ° a ) : (V´V)®VV.
and
By proposition 2.3.4 one has (VV)V<VV via
in2 = L( in ° eval ° (id´id) ) : (VV)V®VV
out2 = L( out ° eval ° (id´id) ) : VV®(VV)V.
Let p2: t´V®V and pr1:V´V®V, pr2: V´V®V be the projections respectively associated with the
products t´V and V´V. Then, for i =1,2, L(pr i): V® V V and, thus, for L(L(pr i ) ° p 2 ) :
t®(VV)V, pi = in ° in2 ° L(L(pri ) ° p2) : t®V.
Define, then, out1 = < eval ° <id, p1 ° !VV> , eval ° <id, p2 ° !VV> > : VV®V´V.
We must prove that out1 ° in1 = idV´V , or equivalently that for i = 1,2, pri ° out1 ° in1 =
pri .
pri ° out1 ° in1 = eval ° <id, pi ° !VV> ° in1
= eval ° < L( app ° (app´id) ° a ), pi ° !V´V>
= app ° (app´id) ° a ° < idV´V, pi ° !V´V>
= app ° < app ° < pi ° !V´V, pr1> , pr2>
= app ° < eval°(out´idV) ° < in°in2°L( L(pri ) ° p2 ) ° !V´V, pr1>, pr2>
= app ° < eval°<in2°L( L(pri ) ° p2 ) ° !V´V, pr1>, pr2>
= app ° < eval°< L(in°eval°(id´id))°L( L(pri ) ° p2 ) ° !V´V, pr1>, pr2>
= app ° < eval°< L(in°eval°(L( L(pri ) ° p2 )´id))° !V´V, pr1>, pr2>
= app ° < eval°< L(in ° L(pri ) ° p2 )° !V´V, pr1>, pr2>
= app ° < in ° L(pri ) ° pr1, pr2>
= eval°(out´idV) ° (in ° L(pri ))´idV



19
2. Constructions


= eval° (L(pri )´idV)
= pri . ¨


Exercises For the following exercises, assume that C is a CCC.
1. Let V be a reflexive object of C. Prove that the collection RetV of all retracts of V in C is a CCC.
2. (Difficult, see section 8.8) Let b be an object of C. A fixpoint operator for b is a morphism
Fixb: bb®b such that Fixb = evalb,b° <id,Fixb>. Let VV<V via (in,out). Let also
F = eval ° <id, in> : VV®V ;
H = L( eval ° (id´(F°out)) ) : VV®VV.
Prove that F°H is a fixpoint operator for V. Define a fixpoint operator for all objects in RetV.
3. Let C be a CCC and suppose that for all a, b in ObC there exists the coproduct a+b (with
embedding ina: a®a+b , inb: b®a+b ). Prove that, for all c in ObC, (a´c)+(b´c) is isomorphic to
(a+b)´c, and define explicitly the isomorphism.
Result: (a´c)+(b´c) @ (a+b)´c via
i1 = (ina´idc)+(ina´idc): (a´c)+(b´c) ® (a+b)´c
i2 = L-1( L(ina´c)+L(inb´c) ): (a+b)´c ® (a´c)+(b´c)
Proving i2°i1=id is easy. For i1°i2 = id, note first that g°L-1(f) = L-1(L(g°eval)°f).
Then, in a few steps, one obtains
i1°i2 = L-1( L(ina´idc)+L(inb´idc) )
= L-1( L(id)°ina+L(id)°inb )
= L-1( L(id) )
= id




2.4 Examples of CCC•s

2.4.1 Scott Domains
In this section and in the following one we introduced two fundamental examples of CCC's, namely,
Scott domains and coherent domains. We define only the exponent object and the eval function and
check that they are respectively an object and an arrow of the category. We leave the problem of
defining the isomorphism L and checking (bcat) and (hcat) as an (easy) exercise for the reader.


2.4.1.1 Definition Let (X,£) be a partiallly ordered set (po-set).
D Í X is directed iff it is nonempty and, for any i,jÎD, there is kÎD such that i £ k, j £ k. A
p.o.set (X,£) is complete (is a CPO) iff every directed subset DÍX has a least upper bound ÈD
(the least element ^ is the least upper bound of the empty directed set).




20
2. Constructions


A point xÎX is compact (finite) if for every directed D such that x £ ÈD , there is an element
yÎD such that x £ y. Let X0 denote the collection of compact elements of X.
The c.p.o. (X, £) is algebraic if for every xÎX the set x¯ = {x 0 ÎX 0 | x0 £ x}is directed and
È(x¯) = x.
A c.p.o. (X,£) is bounded complete if every bounded subset of X has a least upper bound. A
Scott Domain is a bounded complete algebraic c.p.o..


Exercises
1. Check that {{y | x0 £ y} | x0ÎX0} is a basis for a T0 topology on a Scott Domain. This topology
is usually called Scott topology.
2. Prove that the least upper bound of a finite set of finite elements is always finite, if it exists.
3. (Nontrivial) Find counterexamples for the following assertions:
i. if x0 is compact then the set {y | y £ x0} is finite;
ii. if x0 is compact and y £ x0 then y is compact.

2.4.1.2 Definition Let (X,£X ), (Y, £Y ) be c.p.o.•s. A function f: X® Y is monotonic if it
is order preserving, i.e., i £X j implies f(i) £Y f(j) . (We will often omit the subscript X in £X.)
A function f: X®Y is continuous if for every directed DÍX, f(ÈD) = ÈdÎDf(d).

Exercise Let (X,£X), (Y, £Y) be Scott domains. Prove that a function f: X®Y is continuous
according to the previous definition iff it is continuos with respect to the Scott topology.


2.4.1.3 Definition The category D has Scott domains for objects and continuous functions for
morphisms. Let X, Y be objects of D. YX is just the collection of the continuous functions from
X to Y ordered pointwise.


Of course YX is a c.p.o.. We have to prove that it is bounded complete and algebraic.
In order to show that YX is bounded complete, assume that {fi} iÎI has an upper bound g.
Define then h by h(x) = È iÎI{fi(x)}. The function h is well defined since the set {fi(x)}iÎI is
bounded by g(x) and, thus, it has a least upper bound in Y. Moreover, h is continuous because for
every directed set D in X one has:
h(ÈD) = È iÎI{fi(ÈD)}
= È iÎI È xÎD {fi(x)} by the continuity of fi
= È xÎD È iÎI {fi(x)}
= È xÎD {h(x)}
It easy to check that h is a least upper bound for {fi}iÎI.
To show that YX is algebraic, we explicitly define the set (YX)0 of its compact elements.



21
2. Constructions




2.4.1.4 Definition A step funcion from X to Y is a function step-a,b where aÎX 0 , bÎY 0 ,
defined by: step-a,b (x) = if a £ x then b else ^ .

We claim that the compact element of YX are exactly the least upper bound of finite bounded sets of
step functions. In other words, for every f0Î(YX)0, (*) f0 = ÈiÎI{step-ai,bi} for some finite I.
Let us prove first that every function f = È iÎI {step-a i,b i} is compact, when I is finite and
È iÎI{step-ai,bi} exists, i.e., when for all subset J of I, aJ = È iÎJ{ai} exists Þ bJ = È iÎJ{bi}
exists (We then say that I is a compatible set of indices.)
Then, let {gh}hÎD be a directed family in YX such that f £ ÈhÎD{gh}. In particular, for every
J in I as above, f(aJ ) = bJ £ (È hÎD {g h })(a J ) = È hÎD {gh (a J )}. Clearly, for each J, bJ is
compact and {gh(aJ)}hÎD is directed. Let then bJ £ gh(J)(aJ) for some h(J)ÎD. Since I is finite
and {gh}hÎD is directed, let gk , for kÎD , be such that gk ³ gh(J) for all J in I. Clearly f £
gk and we are done.
Prove now for exercise that for every continuous function f: X®Y, one has
i. the set F = { ÈiÎI{step-ai,bi}| I finite, and bi £ f(ai) } is directed
ii. f = ÈF
Suppose then that f is compact. We need to prove that f = È iÎI {step-a i,bi} for some finite
compatible I. By the exercise, f = ÈF, for F directed; thus, there exists I such that È iÎI{step-
ai,bi}ÎF and È iÎI{step-ai,bi} ³ f = ÈF ³ È iÎI{step-ai,bi}. In conclusion f = È iÎI{step-ai,bi};
that is, every finite element in XY has the form (*) and, in particular, XY is a Scott domain.
The function evalX,Y: YX´X®Y is defined by evalX,Y(f,x) = f(x). The proof that eval is
continuous is straightforward.

Interesting examples of Scott Domains may be found everywhere in the literature of denotational
semantics. Indeed, the Cartesian closedness of the category allows you to construct plenty of them as
products and exponents over commonly used ground types. That is, consider your preferred types
of data (integers, booleans, strings,etc.). Organize them as flat p.o.sets, i.e., add a least element ^
and set x £ x' iff x = ^ or x = x'. These are clearly objects of D as well as their products and
exponents.
Other relevant examples are given, for example, by the p.o.sets P of the partial maps from w to
w, the natural numbers, and Pw, the powerset of w. The partial order, in these cases, is given by set
inclusion, which on P means graph inclusion of functions, i.e., f £ g iff "n (f(n)¯ Þ g(n) =
f(n)). As an exercise, the reader may check that both P and Pw live in D.
Interestingly enough, these two familar structures are also reflexive objects in D . We sketch the
proof of this for Pw , see section 9.6-2 for more on P.




22
2. Constructions


Let {en}nÎw be a canonical (bijective and effective) enumeration of the finite subsets of w and let
< , > : w´w®w be a canonical coding of pairs. Define then graph: D[Pw,Pw]®Pw by graph(f) =
{<n,m> | mÎf(en)} and fun: Pw®D[Pw,Pw] by fun(a)(b) = {m | $en Í b <n,m>Îa}. It is a
simple exercise to check that graph and fun are morphisms in D. Moreover, fun » graph = id and,
thus, PwPw<Pw.
This example, which played a relevant role in denotational semantics, has been directly inspired by
Recursion Theory (see the references). Indeed, the work carried on so far can be naturally
’effectivized.“

2.4.1.5 Definition A Scott domain X = (X,£) is effectively given if $e 0 : w®X 0 bijective
and 1. $zÎX e0(n), e0(m) £ z is decidable in n, m
2. $gÎR ($zÎX e0(n), e0(m) £ z Þ e0(g(n,m)) = sup{e0(n),e0(m)}).


Call ED the category of effectively given Scott domains and continuous functions. ED is a CCC. As
a matter of fact, the effectiveness properties are easily inherited at higher types.
Observe that, instead of taking the least upper bounds (l.u.b.•s) of all directed sets, as required in
the definition of ED, one may take only the computable l.u.b.'s, i.e. the l.u.b.'s of directed sets or
ideals in (X0,e0) that are indexed over recursively enumerable (r.e.) sets. (One may independently
choose directed sets or ideals and obtain the same collection of computable elements.)
These limits are computable in a very sound sense. For example, (Pw, {en}nÎw, Í) is in ED
and its computable elements are exactly the r.e. sets.


Exercise Prove a similar fact for the set P of partial maps from w to w .

Call constructive domain a domain whose elements are the computable elements in an
effectively given domain. Since ED is Cartesian closed, this may be done in any (higher) type. In
particular, given the constructive domains Xc, Yc obtained from X and Y , one may consider the
constructive domain YXc of the computable elements of YX . Define then the following


2.4.1.6 CD is the category of constructive domains and continuous and computable morphisms.

Exercise One clearly has to check that, for fÎYXc, "xÎXc f(x)ÎYc.


By the Cartesian closedness of ED, CD also is a CCC. Observe that each Xc is countable and that it
can be effectively enumerated by using an acceptable enumeration of the r.e. sets. Typical objects in
CD are RE, the recursively enumerable sets, and PR (= Pc), the partial recursive functions (see the
exercise above).



23
2. Constructions


Thus, in a rather indirect way, that is by topological and order properties, we obtained a CCC of
countable (and numbered) sets. The proof that CD is a full sub-CCC of EN requires an important
generalization, in higher types, of the classical Myhill-Shepherdson theorem for enumeration
operators. The main application of CD is the characterization of the partial (continuous) and
computable functionals as the sub-CCC of CD generated by PR, i.e., taking PR and constructing all
higher types within CD (see also section 8.4-I). Moreover, one can give a countable and effective
interpretation to the recursive definitions of programs and data types within CD (by a constructive
version of the ’limit constructions“ in chapter 10).

Exercise Prove that RE is reflexive in CD (use the full and faithful embedding of CD in EN).



2.4.2 Coherent Domains

2.4.2.1 Definition A coherent structure is a pair (|X|,-), where |X| is a set and - is a
binary, reflexive, symmetric relation on |X|. The elements of |X| are called points, and the relation
- is called coherence.
The coherent domain associated with (|X|,-) is the collection X of subsets of P(|X|) whose
points are pairwise coherent. The elements of X are ordered by set-inclusion.
Coherence is extended to X in the obvious way, that is: A - B iff AÈBÎX.


Exercise Prove, when X is a coherent domain, that
1. ÆÎX
2. X is closed under directed union
3. (AÎX and B Í A) Þ BÎX


2.4.2.2 Definition Let X, Y be two coherent domains. A function F: X ® Y is stable iff
i). F is continuous
ii."A, BÎX A - B Þ F(AÇB) = F(A)ÇF(B)

2.4.2.3 Definition The category Stab has coherent domains as objects and stable functions as
morphisms.


Given two coherent domains X and Y, their product X´Y is defined by:
i |X´Y| = {(0,z) / zÎ|X| } È {(1,z) / zÎ|Y| }
ii. (a,z)-(a',z') [mod X´Y] iff a = a' Þ z - z' [mod D(a)], where D(0) = X and D(1) = Y.




24
2. Constructions


Exercise Define the projections and check that they are stable, i.e., prove that Stab is Cartesian.

There is simple way to obtain stable functions over coherent domains.

2.4.2.4 Definition Let X,Y be coherent domains. Let also f be an injective function from |X|
to |Y| such that, for all x,x'Î|X|, one has {x, x'}ÎX Û {f(x), f(x')}ÎY. Define then f+ :X®Y
and f -: Y®X by
i. f+(a) = {f(z) / zÎa }
ii. f -(b) = {z / f(z)Îb }

It is a matter of a simple exercise to prove that both f+ and f- are stable functions.
We need to construct next an exponent object out of the set of stable maps over coherent domains.


2.4.2.5 Definition Let F: X®Y be a stable function. The Trace of F is Tr(F) = {(a,z) / aÎX,
a is finite, zÎ|Y|, zÎF(a), ("a'Í a , zÎF(a') Þ a = a')}.


F is completely determined by its trace by means of the following equation: F(A) = {zÎ|Y| / $a Í A
(a,z)ÎTr(F)}.

Exercise Prove that the correspondence between stable functions and their traces is bijective.


Notation The symbol -- is used to represent strict coherence, i.e., A--B iff A-B and A¹B.

2.4.2.6 Definition Let |YX | = {(a,z) / aÎX, a is finite, zÎ|Y| }. Moreover, let (a,z) - (a',z')
iff
i. a -- a' [mod X] Þ z -- z' [mod Y] and
ii. a - a' [mod X] Þ z - z' [mod Y].
Then YX is the arrow domain (exponent object).


Exercises
1. Prove that conditions (i) and (ii) may be stated equivalently as
(a,z) = (a',z') or z--z' or not a-a'.
2. Prove that every element of YX is a trace of some stable function from X to Y , and conversely
that if F: X®Y is stable then tr(F)ÎYX.
3. Let f,g : X ® Y be two stable functions.
Define f £B g (Berry's order) iff "x,yÎX x Í y Þ f(x) = f(y)Çg(x)
Prove that f £B g if and only if Tr(f) Í Tr(g). Let moreover £p be the pointwise order. Prove that:



25
2. Constructions


i. f £B g Þ f £p g
ii. f-g Þ (f £Bg Û f £p g)
4. Let X,Y be coherent domains. A stable function f: X®Y is linear iff :
i. a È bÎX Þ f(a È b) = f(a) È f(b)
ii. f(Æ) = Æ
Prove that f: X®Y is linear iff its trace is formed of pairs (a,z), where the component a is a
singleton. Observe that the maps f+ and f- in 2.4.2.4 are actually linear. Call Lin the category of
coherent domains and linear maps.
5. Let f: X®Y, g: X®Y be two linear functions. Prove that Tr(f) Í Tr(g) if and only if for all x
in X f(x) £ g(x). Deduce as a corollary that on linear functions between coherent domains the order
of Berry coincides with the pointwise order.


2.4.2.7 Definition The function eval X,Y : YX ´X®Y is defined by the following equation:
"AÎY X , "BÎX evalX,Y (A,B) = {y / $(b,y)ÎA, b Í B}.

We prove that evalX,Y is stable. Continuity is trivial. We must only check that if (A,B)-(A',B')
[mod YX] then evalX,Y( (A,B)Ç(A',B') ) = evalX,Y( (A,B) ) Ç evalX,Y( (A',B') ). The inclusion
Í is immediate by continuity.
Take then z in evalX,Y ( (A,B) ) Ç eval X,Y ( (A',B') ). This implies $(b,z)ÎA, b Í B and
$(b',z)Î A', b' Í B'. Note that B-B' by hypothesis and, thus, b-b'. Moreover, also by
hypothesis, A-A' and then, by definition of consistency mod YX , one has b = b'. This implies
(b,z)ÎAÇA',b Í BÇB' Û zÎevalX,Y( (AÇA'),(BÇB') ) Û zÎevalX,Y( (A,B) Ç (A',B') ).
In conclusion, the category Stab of coherent domains and stable functions is a CCC.

Exercise Let f+ and f- be defined as in 2.4.2.4, over coherent domains X and Y. Prove that f-

. 1
( 10)



>>