By this technique and the following construction, one can easily construct, in each cardinal, a

coherent domain of which all other coherent domains of the same cardinality are retracts. In

particular, it will be so also its own function space.

2.4.2.8 Definition If X is a coherent domain, then !X (read of course X) is the coherent

domain defined by

i. |!X| = {a / aÎX, a finite}

ii. a - b [mod !X] iff a È b ÎX .

26

2. Constructions

Let T be the three-element truth value poset {^,true, false}, i.e., the ’lifting“ of {true, false}. For

simplicity, we look at the cardinal w. Consider then the w-power Tw of T. That is, take all the

functions from w to T. When T is partially ordered in the usual way, with ^ least and true and

false incomparable, then Tw is clearly a coherent domain. One may also understand Tw as the set

of disjoint subsets of w. Of course, !Tw is aslo in Stab by the definition just given.

2.4.2.9 Theorem Let D be a coherent domain with a countable |D|, and let e: w®|D| be a

bijective map. Then there exist an injective function f from |X| to |!Tw| such that, for all x,x'Î|X|,

one has {x, x'}ÎX Û {f(x), f(x')}Î!T w .

Proof Let f: |D| ® |!Tw| be defined in the following way:

f(e(i)) = < {i}, {j / j £ i and not e(i)-e(j)} >

Obviously f is injective. It is also trivial that {e(i),e(j)}ÎD implies {f(e(i)),f(e(j))}Î!Tw. Conversely

suppose not e(i)-e(j) [mod D] , and let i £ j (the other case is analogous). This implies that

iÎf(e(j))1 and then not f(e(i))-f(e(j)) [mod !Tw].

2.4.2.10 Corollary Let f+ and f- be as in 2.4.2.4, for f: |D|®|!T w |. Then, for any coherent

domain D with a countable |D|, one has D<!Tw via (f+,f-).

The proof easily follows from the exercise above. Note now that, if D is countably based, so is

DD, in Stab (check this for exercise). Since, in particular, |!Tw| is countable, then !Tw turns ou to

be a reflexive object, as !Tw!Tw< !Tw.

2.5 Equalizers and Pullbacks

Let f,g: A®B a pair of ’parallel“ functions in Set, i.e. f, g have the same source and target. The

subset E of A on which f and g agree, i.e., E = {x / xÎA, and f(x) = g(x)} is called an

equalizer of f and g. We try now to give a categorical characterization of previous set-theoretic

notion. The starting point is that E being a subset of A it must be represented as a subobject, that

is, as a mono i: E®A; moreover, i must enjoy the property f ° i = g ° i. But E is the maximal

subset of A on which f and g agree, and in order to guarantee this condition we require that if h:

C®A is any other function such that f ° h = g ° h, then h ’factors“ uniquely through i , that is,

there exist a unique k: C®E such that h = i ° k. We now prove that the previous condition is

enough to ensure, in Set, that i(E) contains all the xÎA, such that f(x) = g(x).

Suppose not, then there exist aÎA, aÏi(E) such that f(a) = g(a). Consider the function l:

EÈ{a}®A defined by l(e) = i(e) if eÎE, l(a) = a. Of course f ° l = g ° l, and therefore a morphism

k: EÈ{a}®E must exists such that l = i ° k. But then a = l(a) = i(k(a))Îi(E); this is a contradiction.

27

2. Constructions

Since this condition of unique factorization also implies that i is mono (see proposition 2.5.2

below) we are led to the following definition:

2.5.1 Definition Given a pair of morphisms f,gÎC[a,b], an equalizer of f and g is a pair (e,

iÎC[e,a]) such that :

i. f° i = g° i

ii. for all hÎC[c,a], f° h'= g° h' implies $! kÎ C[c,e] i ° k = h.

Coequalizers are defined dually, that is a coequalizer of f,g is a pair (e, iÎC[b,e]) such that:

i. i ° f = i ° g

ii. for all hÎC[b,c], h ° f = h ° g implies $! kÎC[e,c] k ° i = h.

2.5.2 Proposition Every equalizer is monic.

Proof Let i: e®a be the equalizer of f, g: a®b. Let j, l : c®e, such that i ° j = i ° l .

Since f ° (i ° j) = (f ° i) ° j = (g° i ) ° j = g ° (i ° j) there exists a unique h: c®e such that (i ° j) = i ° h,

hence j = h = l. ¨

2.5.3 Proposition Every epic equalizer is iso.

Proof Let i: e®a be the equalizer of f, g: a®b. Since i is epic, and f ° i = g ° i, it follows that f =

g. The identity ida equalizes f and g, and there is a unique morphism h: a®e such that ida = i ° h.

Moreover i ° h ° i = ida ° i = i ° ida, and since i is monic (by proposition 2.5.2), then h ° i = ida . ¨

We now introduce one of the most powerful notions of Category Theory: the pullback. In a sense,

pullbacks generalize equalizers to pairs of morphisms with different sources.

2.5.4 Definition Given two arrows f: b®a and g: c®a with common target a, the pullback

of (f,g) is an object b´ac and two arrows p: b´ac®b, q: b´ac®c , such that

1. f » p = g » q: b´ac®a

2. for every other triple (d, h: d®b, k: d®c) such that g» k = f» h, there exists a unique arrow

<h,k>a: d®b´ac such that p » <h,k>a = h, and q » <h,k>a = k.

The dual notion is called pushout.

28

2. Constructions

A typical pullback diagram is as follows:

The lower ’square“ is also called ’pullback square.“ Note that the notation used for pullbacks is quite

similar to the one used for products; indeed, they behave similarly (products are just a particular case

of pullbacks, see proposition. 2.5.5 below). Note also that the subscript a is meant to express the

dependency of b´ac and <h,k>a on f and g, but b´f,gc and <h,k>f,g, is too heavy a notation:

the subscript must be considered essentially as a warning that we are dealing with a pullback, not just

a product. Usually this omission of information is harmless, because the particular pullback we are

considering is clear from the context.

Example In Set the pullback of (f: B®A, g: C®A) is as follows:

({<x,y> / xÎB, yÎC, f(x) = g(y) }, p1, p2) where p1(<x,y>) = x and p2(<x,y>) = y.

2.6.5 Proposition Let C be a category with a terminal object t. For any object a of C, let !a be

the unique morphism in C[a,t]. If C has pullbacks for every pair of arrows, then it also has products

for every pair of objects.

Proof Hint. Given a,b in C, let (a´b, p1: a´b®a, p2: a´b®b) be the pullback of (!a: a®t, !b:

b®t). It is easy to verify that this is a product. ¨

2.6.6 Proposition If a category C has pullbacks for every pair of arrows and it has terminal

object, then it has an equalizer for every pair of arrows.

Proof Let f,g: a®b. Let (c, fst:c®a, snd:c®a) be the pullback of (<f,ida>: a®b´a, <g,ida>:

a®b´a). Then the equalizer of f,g is (c, fst = snd). Indeed, f » fst = p1» <f»fst,fst> = p1» <f, ida> »

fst = p2 » <g,ida> » snd = p2 » <g»snd,snd> = g » snd. Moreover, for any (c', h:c'®a) such that f

» h = g » h , also <f,ida> » h = <g,ida> » h; by definition of pullback, there exists a unque k: c'®c

such that fst » k = h. ¨

29

2. Constructions

2.6.7 Pullback Lemma (PBL) If a diagram of the form

commutes, then

i. if the two small squares are pullbacks, then the outer rectangle is a pullback;

ii. if the outer rectangle and the right-hand square are pullbacks, then the left-hand square is a

pullback.

Proof Exercise. ¨

2.6.8 Proposition If the square

is a pullback and g is monic, then p is monic as well.

Proof: Exercise. ¨

The previous property suggests an interesting generalization of a common set-theoretic construction.

If f is a function from a set A to a set B, and C is a subset of B, then the inverse image of C

under f, denoted f-1(C) is that subset of A defined by f-1(C) = {x/ xÎA, f(x)ÎC }.

It is easy to show that the diagram

is a pullback square in Set.

30

2. Constructions

In general, given a monic g: c•®b and a morphism f: a®b, the inverse image of g under f

is the subobject of a (if it exists) obtained by pulling back g along f.

2.6 Partial Morphisms and Complete Objects

As mentioned in the introduction, the common perspective of Programming Language Theory and

Category Theory is due to the priority given to ’functions“ with respect to ’sets.“ The latter notion,

when required, is a derived notion of the former, in a sense.

There is an other aspect, though, that should be considered. In Computation Theory, as well as in

actual programming, diverging computations cannot be avoided unless a restriction is made to a

subclass of the computable functions.

The notion of partiality has a natural interpretation over sets. Let f: A®B be a partial function; the

domain of convergence of f, call it f¯, is just a subset of its ’domain“ A in the broader sense;

moreover the restriction of f to f¯ is a total map f|(f¯): f¯®B. Thus a partial map f may be

represented by a pair of total functions (i: D®A, h: D®B), where DÍA is the domain of

convergence of f, h is the restriction of f to D, and i: D®A is the canonical injection .

If we try to simulate the previous definition in categorical language, it is natural to define a partial

map f between two objects a and b in a category C as a pair (m: d®a , h: d®b), where m is

monic. However, as in the case of subobjects, we have no way to choose d in a canonical way, so

we are forced to identify partial morphisms up to isomorphic variations of d (see section 1.5.)

2.6.1 Definition Given a category C and two objects a and b, a partial map [m, h]: a®b is an

equivalence class of pairs (m: d®a, h: d®b), where m is monic, with respect to the following

relation R: (m: d®a, h: d®b) R (m': d'®a, h': d'®b) iff $k: d®d', k iso, m' = m ° k , h' = h ° k.

With a little abuse of language, we will often speak about a particular pair (m: d®a, h: d®b) when

we actually mean [(m: d®a, h: d®b)]R.

Our next aim is to define a category pC of partial maps on C. The main problem is in defining

composition. If C has pullbacks for every pair of arrows, then the problem is resolved in the

following way.

Given (n: e®b, k: e®c) and (m: d®a, h: d®b), define [n, k] ° [m, h]: a®b as the equivalence

class determined by the outermost sides in the following diagram, i.e., (m»n': d´ b e®a, k»h':

d´be®c) :

31

2. Constructions

where the square is a pullback. Note that by proposition 2.5.8, since n is monic, n' is monic, too.

Let us see how the previous definition works in Set. For the equivalence relation defined on

partial morphisms, we suppose dÍa, eÍb and take m: d®a, n: e®b as canonical injections. Then

d´ b e = {(x,y) / xÎd, yÎe, h(x) = n(y) } = {(x,y) / xÎd, yÎe , h(x) = y } @ {x / xÎd, h(x)Îe },

that is, the expected domain of convergence of the composed function. The projections h' and n'

associated with the pullback {x / xÎd, h(x)Îe} are respectively h|{x / xÎd, h(x)Îe} and the

canonical injection i: {x / xÎd, h(x)Îe}®d. In conclusion, for all xÎ{x / xÎd, h(x)Îe }, one has

k(h'(x)) = k(h(x)) , as we wanted.

Every arrow fÎC[a,b] has a natural associated arrow in pC, that is (id: a®a, f: a®b). We say

that a map in pC is total iff it has the above form (up to equivalences). (pC)t is the subcategory of

pC of total maps. As will become clearer in the next chapter, C is ’isomorphic“ to (pC)t.

Exercise Prove the following assertions:

1. id is total;

2. f,g total Þ f°g total;

3. f°g total Þ g total;

Example pSet is the category of sets with partial maps as morphisms. pR = PR is the monoid of

the partial recursive functions. pEN is defined by using partial recursive functions in the diagram

that defines the morphisms, instead of the total ones (see section 2.2). Observe that the diagrams

commutes iff eb°f' = f°ea for f'ÎPR and, hence, ea(n) = ea(m) and f'(n)¯ Þ f'(m)¯. Clearly,

(pSet)t = Set, PR t = R and (pEN)t = EN.

Remark Sometimes, in the construction of the category pC from C, it may be intersting to restrict

our attention to only a subset of the class of monics of C. Consider, for example, the category PO of

p.o.sets: an interesting definition of a partial map f between two p.o.sets would also require f to be

defined in an upward closed subset. Let C be a category with pullbacks for every pair of arrows. An

32

2. Constructions

admissible family M of monics of C , is a family of monics closed under identities,

compositions, and pullbacks. Every admissible M on a category C gives rise to a different category

(M)(pC) of partial maps.

As already recalled, diverging computations play an essential role in the theory of computation.

They also have an obvious interpretation in Set Theory. However, the set-theoretic understanding of

computations may not suffice. Type-free languages and many typed ones, as we shall see later,

escape a ’naive“ interpretation as sets and functions.

As a matter of fact, since the early days of denotational semantics of programming languages, the

need to give meaning to (possibly) diverging computations over nontrivial mathematical structures

suggested the introduction of various categories of p.o.sets with least elements. The naive

understanding of this is immediate: add to all required data types, as sets, an extra element and give

them a p.o.set structure as flat p.o.sets (i.e., ^ is the least element and all others are incomparable).

We already dealt with this in practice, when presenting various categories of p.o.sets as examples of

CCC's. In a sense, the bottom element ^ provides the first hint of the introduction of approximation

and continuity notions to the mathematical semantics of programs.

As we have demonstrated, this concept is very clear matematically, at least in several specific

categories, such as continuous or algebraic lattices, c.p.o•s, and Scott domains. It is not so simple in

interesting categories for computations such as EN, though. In order to understand it in a general

setting and avoid any abuse of this simple concept, a category-theoretic perspective may provide a

sound mathematical frame.

Notation In the rest of this section, C is a category of partial maps, i.e., C = pD for some

category D with pullbacks for every pair of arrows. Ct is the associated category of total maps. Since

Ct is a subcategory of C, we compose total and partial morphisms by using the same operation of

composition. For typographical reasons, we write a° instead of a^.

The set-theoretic idea we try to formalize categorically is that, when an object a is ’lifted“ to a° by

adding an extra least element, then any hom-set of total maps with target a° is isomorphic to the

corresponding hom-set with target a .

2.6.2 Definition. The lifting of aÎOb C is an object a°ÎOb C t together with a morphism

exaÎC[a°,a] and for every cÎObC an operation tc: C[c,a]®Ct[c,a°] such that, for every fÎC[c,a]

and for every gÎCt[c,a°] one has

1. exa ° tc(f) =f

2. tc( exa ° g ) = g.

33

2. Constructions

The operation t c : C[c,a]®C t [c,a°] is bijective, as t c -1 is defined by t c -1 (g) = exa ° (g).

Conversely, if tc is bijective and (1) holds, then also (2) does. Indeed, let gÎCt[c,a°]; since tc is

surjective, then there is fÎC[c,a] such that tc(f) = g. That is, tc(exa ° g) = tc(exa ° tc(f)) = tc(f) =

h Thus, the following is an equivalent definition of the lifting object:

2.6.3 Definition. The lifting of aÎOb C is an object a°ÎOb C together with a morphism exa Î

C[a°,a] such that, for every fÎC[c,a], there exists one and only one gÎC t[c,a°] satisfying the

equation: exa ° g = f.

Thus, as we wanted, for all b, C[b,a] and C t[b,a°] are isomorphic, since any partial morphism

fÎC[b,a] may be uniquely extended to a total one when the target object is lifted (and the lifting

exists).

Exercise Prove that the lifting a° of an object a is unique, if it exists.

2.6.4 Proposition. Let a° be the lifting of a and set ina = t a(ida) . Then a is a retract of a° in

C (notation: a <p a°) via (ina ,exa).

exa° ina = (t a°)-1(id) ° ina by definition of (t a°)-1

Proof.

= (t a)-1(id ° ina)

= (t a)-1(ta(id))

= id. ¨

2.6.5 Definition. An object aÎOb C is a complete object iff a < a° in C t.

The intuition should be clear. An object is complete when it ’already contains,“ in a sense, the extra

^ . Think of an object d of pCPO and take its lifting d° , i.e., add a least element ^ to d. Then

d is complete, that is, d < d° via (i,j), iff d already contained a least element, j(^) to be precise. It

is actually easy to show that the complete objects in pPO, and likewise in pCPO, are exactly the

partial ordered sets with a least element.

Note that in contrast to the partial retraction a <p a° via (in,ex) in definition 2.6.4, which may be

always given, only complete objects yield total retractions a < a°.

2.6.6 Lemma. If a < a° via (i,j) (in Ct), then $outÎCt[a°,a] a < a° via (ta(ida),out).

Proof Set out = j ° t(exa°i°exa). Then

out ° ta(ida) = j ° t(exa°i°exa) ° ta(ida)

= j ° t(exa°t(exa°i°exa) ° ta(ida) ) by (2) in def. 2.6.2

= j ° t(exa ° i ° exa ° ta(ida) ) by (1)

34

2. Constructions

= j ° t(exa ° i) by (1)

=j°i by (2)

= ida. ¨

Thus we may then assume that, if a is complete, a < a° via (in=ta(ida),out).

The following fact gives the main motivation for the invention of complete objects: exactly on

complete objects as targets all partial morphisms may be extended to total ones, with the same target.

2.6.7 Definition fÎC t[b,a] extends fÎC[b,a] iff "cÎOb C , "hÎC t[c,b], (f ° h)ÎC t[c,a]

Þ f ° h = f ° h.

2.6.8 Theorem. Let a° be the lifting of aÎObC. Then a < a° Û "b, "fÎC[b,a], $fÎCt[b,a]

such that f extends f.

Proof.(Þ) Set f = out ° tb(f). Then, for every hÎCt[c,b], such that (f ° h)ÎCt[c,a] ,

f°h = out°tb(f)°h

= out°tc(exa°tb(f)°h ) by (2) in def. 2.6.2

= out°tc(f°h) by (1)

= out°tc( exa°ta(ida)°f°h ) by (1)

= out°ta(ida)°f°h by (2)

= f°h

(Ü) just take ex ÎCt[a°,a]. ¨

Exercises Prove the following facts:

1. a° < a°°.

2. b < a < a° Þ b < b°. (Hint: let b < a via (i,j). For any fÎC[c,b] consider the extension

i°fÎCt[c,a] of i°fÎC[c,a]. Then j°i°fÎCt[c,b] and "h into dom(f) j°i°f°h = j°(i°f°h) = f°h.)

2.7 Subobject Classifiers and Topoi

Subobjects and partial morphisms already forced some typical set-theoretic notions into the realm of

categories. Let us take now a further step and categorically reconstruct power-sets and related

constructions. By this, it will be possible to relativize these notions to structured sets. As for

subobjects, the categorical version carries the structural information of the intended category.

In Set there is a one-to-one correspondence between subset of a set A and functions from A to

2={true, false}. The isomorphism takes every BÍA to its characteristic function c B :A®2,

defined by the following: cB(a) = true if aÎB, cB(a) = false if aÏB. This isomorphism may be

expressed in the categorical language by means of a pullback diagram

35

2. Constructions

where inB: B®A is the subset inclusion, and true: {*}®{true, false} takes * to ’true.“

The above diagram suggests the following definition in Category Theory:

2.7.1 Definition Let C be a category with a terminal object t. A subobject classifier is an

object W together with a morphism true: t®W such that for every monic i: b®a there is a unique

arrow cb: a®W such that the following diagram is a pullback diagram:

Exercise A subobject classifier, when it exists in C, is unique up to isomorphisms.

The subobject classifier W plays a central role in the translation of Set Theory into Category Theory.

It allows the simulation into the categorical language of concepts like intersection, union, and

complement, by the definition of a Heyting algebra of truth-morphisms over W.

2.7.2 Definition A topos is a category C with a terminal object, a subobject classifier, pullbacks

for every pairs of arrows, and exponents for all pairs of objects.

It will turn out that a topos is a ’universe“ where we can carry out constructions with almost the same

confidence as we do in Set. Of course, Set itself is a topos.

Exercises

1. Prove that if C is a topos, then C is a CCC.

2. In a topos C, what is the arrow eval: Wa´a® W ?

36

2. Constructions

In the spirit of a categorical description of set-theoretic concepts, one may also talk in topoi of

’relations“, ’powersets“, and so forth. Quite generally, given objects a and b, a relation on a and

b, is simply a monic r: d®a´b. In particular, then, one may consider power-objects P(a) as given

by a relation Îa: d®a´P(a) with the following universal property:

2.7.3 Definition Let C be a cartesian category and aÎOb C . The power-object P(a) is an

object of C together with an object d and a monic Î a : d®a´P(a) (a membership-relation)

which is universal in the sense that, for any object b and monic m : e®a´b, there is a unique map

r: b®P(a) and a (forcedly unique) map g: e®d to make the following square a pullback:

As W is the truth value object, the set-theoretic intuition suggests that, in a topos, the object Wa

should represent exactly the power-object of a.

2.7.4 Proposition In a topos C every object a has a power-object Wa.

Proof. Let Îa: d®a´P(a) be defined by the following pullback square:

Then the required universality of Îa is given by the properties

1. of the subobject classifier, i.e. the existence of the characteristic map ce of m;

2. of the map eval , i.e. the existence and unicity of L(ce);

3. of the above pullback ;

an by an application of the pullback lemma 2.5.7. All this is described by the following commuting

diagram, where the squares are pullbacks:

37

2. Constructions

¨

The reader who has completed exercise (2) above may easily understand the intuitive meaning of

the construction in 2.7.3 and compare it to his set-theoretic understanding. In particular, eval says

whether ’an element of a is in a given subset of a .“

Exercises

1. Prove that any topos has lifting.

2. Prove that a category C is a topos if and only if it has a terminal objects, and all pullbacks and

powerobjects.

References The general notions can be found in the texts mentioned at the end of chapter 1,

though their presentation and notation may be different. For example, in the case of CCC's, this is so

also because these categories play a greater role in the categorical approach to Type Theory, or to

denotational semantics, than in other applications of Category Theory. Notice that Grp and Top are

not CCC's and consider that the origin of Category Theory is largerly indebted to algebraic geometry.

Applications of universal concepts from Category Theory to Programming Language Theory have

been developed by several authors, in particular for program specification. For instance, the work by

the ADJ group is explicitly based on universal conditions for specification (initial algebras of abstract

data types; see Goguen et al. (1973/78) ). An early insight in the connections between programs and

categories may be found in Burstall and Thatcher (1974). All these aspects go beyond the limited

aims of this book, which privileges ’theories of functions“ over ’algebraic theories.“ Some more

notions with an algebraic flavor may be found in chapter 4.

As for the examples we have provided, they originated entire areas of research. In particular, the

category EN was first introduced by Malcev, as a general setting of Recursion Theory, and widely

used in Ershov (1973/75). Scott domains and related categories are broadly treated in several places,

38

2. Constructions

e.g. Scott (1981/82), Scott and Gunter (1989) or many books in denotational semantics. Scott (1976)

presents Pw as a reflexive object and discusses categories of retractions. The (generalized) Myhill-

Shepherdson theorem and related matters may be found in Scott (1976), Giannini and Longo (1984),

Berger (1986), Rosolini (1986), and Longo (1988a), among others.

Coherent domains are given in Berry (1978) and used in Girard (1986), where linear maps are

introduced (with some relevant consequences, see section 4.4).

There is a broad literature on categories with partial maps. We partly followed the approach in

DiPaola and Heller (1984), and in Longo and Moggi (1984), where the notions of ’complete object“

and partial Cartesian Closed Category were introduced (and applied in Asperti and Longo (1987) ).

The properties of complete objects carry on also when using a more topos-theoretic perspective, as

shown in Moggi (1988), which is devoted to a deeper insight into the concepts just sketched here.

New results and surveys on categories with partial morphisms may be also found in Rosolini (1986),

Moggi (1988a), Robinson and Rosolini (1988) and Curien and Obtulowicz (1988). Independently of

the category-theoretic approach, Plotkin (1984) used the category pCPO for the purposes of

denotational semantics.

Toposes originated by works of Lawvere and Tierney. A (difficult) introduction to Topos Theory

may be found in Johnstone (1977). The reader may also consult Goldblatt (1979) or Barr and Wells

(1985) on this subject.

39

3. Functors and Natural Transformations

Chapter 3

FUNCTORS AND NATURAL TRANSFORMATIONS

The starting point of Category Theory is the premise that every kind of mathematically structured

object comes equipped with a notion of ’acceptable“ transformation or construction, that is, a

morphism that preserves the structure of the object. This premise holds for categories themselves: a

functor is the ’natural“ notion of morphisms between categories. By a further step, the question

about what a morphism between functors should look like suggests the notion of natural

transformation.

Of course, this is not a matter of arbitrary generalizations: it is a habit of mathematics to build

constructions on top of constructions, since one may understand in this way, by the uniformity of

methods and language, the reasonableness of specific constructions. And this theoretical unification,

suggesting power and intellectual unity, is one of the major merits of Category Theory and its

applications.

Moreover, as we shall see in several examples, there are notions which are clarified in an

essential way or even suggeted by the categorical language of functors and natural transformations.

Indeed, there are even too many examples for our purposes, and we will be able to mention only a

few that are easily met in computer science.

3.1 Functors

If a transformation F between two categories C and D must map the categorical structure of C to that

of D, it must take objects and morphisms of C to objects and morphisms of D; moreover, it must

preserve source, target, identities and composition. Such a transformation F: C®D is called a

functor.

3.1.1 Definition Let C and D be categories. A (covariant) functor F : C ® D is a pair of

operations Fob: ObC ® ObD , Fmor: MorC ® MorD such that, for each f: a®b , g: b®c in C,

- Fmor(f) : Fob(a)® Fob(b)

- Fmor(g ° f) = Fmor(g) ° Fmor(f)

- Fmor(ida) = idFob(a).

It is usual practice to omit the subscripts ’ob“ and ’mor“ as it is always clear from the context

whether the functor is meant to operate on objects or on morphisms.

40

3. Functors and Natural Transformations

1.2 Examples

1. If C and D are preorders, then a functor F: C®D is just a monotone function from the objects of

C to the objects of D, indeed a <C b Û $“fÎC[a,b] Þ F(f)ÎD[F(a),F(b)] Û F(a) <D F(b).

Conversely, given a monotone function f between two partial orders C and D, there is of course

only one way to extend f to a functor among the categories associated with C and D.

2. The identity functor I: C®C is defined by a pair of identity operations both on objects and on

morphisms of C. Similarly, we define the inclusion functor Inc: C®D when C is a subcategory

of D.

3. If C is a Cartesian category define ´ : C´ C®C as the pair of operations that take (a,b)ÎObC´ C

´

to ´ (a,b) = a´bÎObC, and (f,g)ÎC´ C[(a,b),(c,d)] to ´ (f,g) = f´g = <f»p1,g»p2>ÎC[a´b,c´d]. ´

´

is a functor. Indeed ´ preserves sources and targets and, moreover,

´ (ida,idb) = ida´idb = <pa,pb> = ida´b = id´ (a,b)

´( (f,g)°(h,k) ) = ´(f°h,g°k) = (f°h)´(g°k) = (f´g)°(h´k) = ´(f,g) ° ´(h,k)

´ is usually called product functor (since products are only determined up to isomorphisms, we

must assume here a canonical choiche, for each object a, b, of their product a´b).

4. The power-set functor P: Set®Set takes every set A to its power-set P(A) and every function

f: A®B to the function P(f): P(A)®P(B) defined by

"A'ÍA P(f)(A') = {yÎB / $xÎA', y = f(x)}.

Note that the set P(f)(A') is what is usually called f(A').

A functor F: C®D preserves a property P that an arrow f may have in C, if the arrow F(f) has

the same property in D. For example, every functor preserves isomorphisms, or the property of

being a component of a retraction pair, as it is stated in the following proposition:

3.1.3 Proposition Let F: C®D be a functor. If a<b (a @ b) in C, then F(a) <F(b) (F(a) @

F(b)) in D.

Proof. If f»g = id, then F(f)»F(g) = F(f»g) = F(id) = id. ¨

Exercise Does every functor F preserve the property of being monic or epic?

A functor F: C®D is faithful if for all a,bÎObC and for all f,gÎC[a,b], F(f) = F(g) implies f = g;

it is full if for all a,bÎOb C and every hÎD[F(a),F(b)] there is gÎC[a,b] such that h = F(g). A

functor F: C®D is a full embedding iff it is full and faithful, and it is also injective for objects.

A functor that ’forgets“ (part of) the intended structure of the objects is called forgetful: typical

examples are the functors from Grp, Top, or PO to Set which assign to each object its set of

elements and to each arrow the function associated with it. This notion is not a precise one, but it is

41

3. Functors and Natural Transformations

usually clear when a functor can be considered ’forgetful“; note however that a forgetful functor

should always be faithful (and very rarely full).

The definition of functor we have given preserves also the direction of the arrows in C. In some

cases, it is interesting to study transformations among categories that reverse such directions, that is,

by mapping sources to targets and vice versa. A transformation of this kind between two categories

C to D may be considered as a functor from the dual category C op to D, and it is known as

contravariant functor (from C to D). Explicitly, note the following definition

3.1.4 Definition Let C and D be categories. A contravariant functor F: C®D is a pair of

operations Fob: ObC®ObD, Fmor: MorC®MorD such that for each f: a®b , g: b®c in C,

- Fmor(f) : Fob(b)®Fob(a)

- Fmor(g ° f) = Fmor(f) ° Fmor(g)

- Fmor(ida) = idFob(a)

Examples

1. Each functor F: C®D defines a contravariant functor Fop: Cop®D that coincides with F on

objects and such that Fop(f) = F(fop), Fop(g»f) = Fop(f)»Fop(g). Of course, F = (Fop)op.

2. The duality functor ( )op: C®Cop is a contravariant functor such that (a)op = a for aÎObC

and (f)op = f for fÎMorC.

3. The function that takes every set A to its power-set P(A) may be also extended in a natural way to

a contravariant power-set functor P: Set®Set. Just define, for f: A®B, P(f): P(B)®P(A)

as the function that assigns to each B'ÍB the set P(f)(B') = f -1(B') = {xÎA / $yÎB', f(x)=y}.

4. Let C be a category with pullbacks, and let fÎC[a,b]. Then f induces a pullback functor f*:

C¯b®C¯a, whose action is described in the following diagram:

In this diagram, g and h are objects of C¯b, and kÎC¯b[g,h]; f*(g) and f*(h) are the pullbacks

of g and h along f, yielding a unique arrow f*(k) making the above diagram commute. The proof

that f* is a functor is a consequence of elementary properties of pullback, and it is left as an exercise

for the reader.

42

3. Functors and Natural Transformations

5. Let C be a CCC. For every cÎOb C the exponent functor expc: C®C is defined as follows.

For every aÎObC, set expc(a) = ca , and for every fÎC[a,b], expc(f) = L(evalb,c ° id´f) : cb®ca.

As a diagram,

In order to check that expc is actually a contravariant functor, we must take these steps:

expc(id) = L(eval ° id´id) = L(eval) = id

expc(f ° g) = L(eval ° id´( f ° g ) )

= L(eval ° id´f ° id´g )

= L(eval °L(eval ° id´f)´id ° id´g ) by the diagram

= L(eval ° id´g ° L(eval ° id´f)´id )

= L(eval ° id´g ) ° L(eval ° id´f)

= expc(g) ° expc(f). ¨

Note that the composition of two functors is still a functor and that there exists the identity functor

which is right and left invariant w.r.t. composition. Thus, it is sound to define the category Cat

whose objects are categories and whose morphisms are functors. It is worth pointing out that this is a

convenient and unusual algebraic property. The collection of groups is not (naturally) a group;

similarly for topological spaces and so on. The definition of Cat, so similar to the paradoxical ’set of

all sets“ of Set Theory, must be used with some caution, however. It is not our intention to engage in

foundational questions in this book, but it is time to say a few more words about our ’axiomatic“

defintion of Category. So far we have made no assumption at all about the dimension of the classes

ObC and MorC; the word ’class“ itself has been used in an intuitive sense, without any reference to

an underlying Set Theory. From now on, though, the reader may refer to the notions of set and class

as used, say, in Gšdel-Bernays Set Theory, in order to make this distinction clear. From this

perspective, a Category C such that ObC and MorC are sets, is called small. In the sequel, when

we refer to Cat, we mean the category of all small categories; of course, Cat itself is not a small

category, and thus it is not among its own objects.

(Question: which of the categories mentioned so far are small, and which are not?)

If C is a small category, then, for all a,bÎObC , C[a,b] is a set, usually called hom-set of a

and b (some authors use the word ’hom-set“ in an arbitrary category). We say that a category C is

locally small when for all a,bÎOb C , C[a,b] is a set and not a class. If C is a locally small

43

3. Functors and Natural Transformations

category, it is possible to define some functors from C to Set, called hom-functors, that play a

central role in the developments of Category Theory. We shall see later that most of this work may be

done at a more abstract level, taking an arbitrary topos D instead of Set.

3.1.5 Definition Let C be a locally small category. Given aÎOb C , the covariant hom-functor

C[a,_]: C®Set is given by:

i. for every bÎObC C[a,_](b) = C[a,b]ÎObSet;

ii. for every gÎC[b,b'], C[a,_](g): C[a,b]®C[a,b'] is the function that takes fÎC[a,b] to (g°f)

ÎC[a,b'] that is,

The function C[a,_](g) will be denoted in the sequel by ’C[a,g]“ or also by the suggestive ’g ° _“

(some authors use also g*). Note that the drawing above is clearly an implication between diagrams.

Their plain juxtaposition will be used often in the sequel with this meaning, as a special case of the

’conditional equational reasoning“ mentioned earlier in section 1.2.

3.1.6 Definition Let C be a locally small category. Given bÎOb C , the contravariant hom-

functor C[_,b]: C®Set is given by:

i. for every aÎObC C[_,b](a) = C[a,b]ÎObSet

ii. for every hÎC[a',a], C[_,b](h): C[a,b]®C[a',b] is the function that takes fÎC[a,b] to f °

h ÎC[a',b] that is

The function C[_,b](h) will be denoted in the sequel by ’C[h,b]“ or by the suggestive ’_ ° h“

(some authors use also h* .)

3.1.7 Definition Let C be a locally small category. Given bÎObC , the hom-functor C[_,_]:

C opxC®Set is given by:

44

3. Functors and Natural Transformations

i. for every (a,b)ÎObCxC C[_,_](a,b) = C[a,b]ÎObSet

ii. for every hÎC[a',a], gÎC[b,b'], C[_,_](h,g): C[a,b]®C[a',b'] is the function that takes

fÎC[a,b] to g ° f ° h ÎC[a',b']

C[_,_] is contravariant in the first argument and covariant in the second. One may understand how

C[_,_] works on morphisms by the following commutative diagram:

The function C[_,_](h,k) will be denoted by ’C[h,k]“ or by ’g °_ ° h.“

Exercise: prove in details that C[a,_] and C[_,b] are a covariant and a contravariant functor,

respectively.

Exercise A category C has enough points iff the functor C[t, -] is faithful, when t is terminal.

3.2 Natural Transformations

The fact that F is a functor from a category C to a category D may be equivalently expressed by

F(id) = id and, for every f and g in MorC , by the following (implication between) diagrams:

Consider now two functors F, G: C® D. A quite reasonable idea of transformation from F to G

is a ’translation“ as described in the following picture, where the dotted lines should yield

commutative squares

45

3. Functors and Natural Transformations

Thus, the ’translation“ can be defined by assigning to each object aÎOb C an arrow t a :

F(a)®G(a), with the only condition that, for every fÎC[a,b], the following diagram commutes:

The properties described in this diagram are equivalently formalized by the following definition.

3.2.1 Definition. Let F,G : C ® D be functors. Then t : F ® G is a n a t u r a l

transformation from F to G iff:

i. "aÎObC taÎD[F(a),G(a)]

ii. "fÎC[a,b] tb ° F(f) = G(f) ° ta .

3.2.2 Example Let C be a small category, and hÎ C [a',a] . The collection (in Set) of

morphisms {C[h,b] / C[a,b]®C[a',b] }bÎC , defines a natural transformation C[h,_] from the

(contravariant) hom-functor C[a,_] to the (contravariant) hom-functor C[a',_]. Note the following

diagram:

46

3. Functors and Natural Transformations

The same diagram proves that, given kÎ C [b,b'], the collection of morphisms {C [a,k] /

C[a,b]®C[a,b'] }aÎC defines a natural transformation C[_,k] from the hom-functor C[_,b] to

the hom-functor C[_,b'].

It is easy to close up natural transformations under composition by setting (t»b)a = (ta)»(ba). This

composition of natural transformation is usually called vertical, as opposed to the horizontal

composition, defined at the end of this section. Since the identity transformation from a functor F

to itself is defined in the obvious way, we have actually constructed a new category, starting from

any two given categories C and D .

The new category is called the category of functors from C to D, (C®D) = Funct(C,D);

its objects are functors and the morphisms are natural transformations. In particular, if F,G: C®D,

Funct(C,D)[F,G] is the collection of all the natural transformations from F to G; in the following

we shall use the abbreviation Nat(F,G) instead of Funct(C,D)[F,G].

Two functors from C to D are equivalent (or naturally isomorphic) iff they are isomorphic

as objects of Funct(C,D). For example, it is well understood that any set A is isomorphic to A´1,

where 1 is a singleton. For arbitrary cartesian categories, this corresponds to saying that the functor

_´1 and the identity functor Id are naturally isomorphic. If F: C®D is a full embedding, then C

is isomorphic to a full subcategory of D. The next section will present further examples of natural

isomorphisms.

The concept of natural isomorphism of functors also allows us to define a notion of

’equivalence“ between categories, which captures better than the notion of isomorphism the sense

that two categories can be said to be ’essentially the same.“ Two categories C and D are

equivalent if and only if there are two functors F: C®D and G : D®C such that G ° F @ idC

and F ° G @ idD (note that C is isomorphic to D iff G ° F = idC and F ° G = idD).

3.2.3 Proposition Let F,G : C®D be functors and t : F®G be a natural transformation from

F to G. Assume that, for each aÎObC , ta Î D[F(a),G(a)] is an isomorphism. Then t is a

natural isomorphism.

47

3. Functors and Natural Transformations

Proof Define t-1 : G®F by t-1a = (ta)-1. t-1 is natural, since "fÎC[a,b]

t-1b ° G(f) = tb-1 ° G(f) ° ta ° ta-1

= tb-1 ° tb ° F(f) ° ta-1

= G(f) ° t-1a. ¨

Examples A simple example of natural transformation may be given by studying ’liftings“ (see

section 2.6), in various categories. One may actually understand the general notion better, by

completing a little exercise on natural transformations. Indeed, what is hidden behind definition

2.6.2, is the ’naturality“ of tc. When writing this down explicitly, the definition is tidier and more

expressive. Let C be a Category of partial maps, Ct be the associated category of total maps, and

Inc: Ct®C be the obvious inclusion. Thus, 2.6.2 may be simply restated as

The lifting of aÎObC is the object a° such that the functors C[_,a] ° Inc, Ct[_,a°] : Ct®Set

are naturally isomorphic.

Then, by definition of natural transformation and hom-functor, this requires the existence of a

function t such that the following diagram commutes, for any object b and c in C and fÎCt[c,b]

That is, tc(g°f) = tb(g)°f and (tc)-1(h°f) = (tb)-1(h)°f , for any total f, since t is an isomorphism.

With this definition, to prove unicity of liftings is even smoother than in section 2.5. Indeed, let

t be the given natural isomorphism, and let a' and b be an alternative lifting and natural

isomorphism. Set f = t ° b-1. Then Ct[_,a'] and Ct[_,a°] are naturally isomorphic via f and, for

f = fa'(id): a'®a° and g = ( fa° )-1(id): a°®a', one has:

g°f = ( fa° )-1(id)°f

= ( fa' )-1(id°f) by naturality

= ( fa' )-1( fa'(id) )

= id.

Similarly for f°g = id (on a°).

Since we are now familiar with functors, we may look also at lifting as a functor.

48

3. Functors and Natural Transformations

Let C be a pC and assume that for each aÎObC there exists the lifting a°. Then there is a (unique)

extension of the map a |_ a° to a functor _° : C®Ct (the lifting functor).

The reader may check this as an exercise (hint: observe that exa = ( ta°)-1(id): a»®a and use the

naturality of t ) .

As for specific examples, the lifting functor for pSet is obvious. It can be easily guessed also for

the category pPo of p.o.sets and partial monotone functions with upward closed domains: just add a

fresh least element and the rest is easy for the reader who has completed the last exercise. Note, and it

is crucial, that by monotonicity the lifting functor does not exist if one doesn't assume that the

domains are upward closed.

The category pCPO is given by defining complete partial orders under the assumption that

directed sets are not empty. Thus, the objects of pCPO do not need to have a bottom element. As

for morphisms, take the partial continuous functions with open subsets as domains. Clearly, the

lifting functor is defined as it is for pPo.

A more complex example is given by EN, the category of numbered sets in section 2.2. Let

pEN be the partial category of numbered sets in the example before 2.5.2. Given a = (a,e)ÎObpEN,

define a° = (a °,e°) by adding a new element ^ to the set a and by defining e°(n) = if fn(0)

converges then e(f n (0)) else ^ . Clearly, e° : w®a° is surjective. Let now b = (b,e') and

fÎpEN[b,a]. By definition, there exists f'ÎPR such that f° e' =e° f'. We define the extension

fÎEN[b,a°] of f by giving f'ÎR which represents f . That is, set ff'(n)(0) = f(n). Such an f'ÎR

exists by the s-m-n (iteration) theorem. Thus,

f(e'(n)) = e°(f'(n))

= if ff'(n)(0) converges then e( ff'(n)(0)) else ^ .

Therefore, if f(e'(n)) = e(f'(n)) is defined, then f f'(n) (0) converges and, hence, f(e'(n)) =

e(f f'(n) (0)) = f(e'(n)). Finally, set t a b(f) = f . For each a, t a gives the required natural

isomorphism, as "gÎEN[b,a°] $!fÎpEN[b,a] f'(n) = f g'(n) (0). (Exercise: check the due

diagram). By the fact above, this defines the lifting functor in pEN.

Exercise Define the category ER of equivalence relations on w and effective maps (hint: the

objects are quotient sets on w, and the morphisms are induced by total recursive functions similarly

as for EN). Observe that ER and EN are equivalent, but not isomorphic. Indeed, one is small, while

the other is not.

We next discuss ways to derive natural transformations from a given one and, finally, the notion of

horizontal composition.

Let H: A®B, F: B®C, G: B®C, K: C®D be functors, and let t: F®G be a natural

transformation as shown in the following diagram:

49

3. Functors and Natural Transformations

t induces two natural transformations Kt: KF®KG, and tH: FH®GH, respectively defined by

(Kt)b = K(tb) : KF(b)®KG(b);

(tH)a = tH(a) : FH(a)®GH(a)

We have, for every fÎB[b,b'] and every gÎA[a,a'],

(Kt)b'° KF(f) = K(tb) ° K(F(f)) = K(tb° F(f) ) = K(G(f) ° tb) = KG(f) ° Ktb = KG(f) ° (Kt)b

(tH)a'° FH(g) = tH(a') ° F(H(g)) = G(H(g)) ° tH(a) = GH(g) ° (tH)a

that proves the naturality of Kt and tH .

Consider now categories, functors, and natural transformations as described in the following

diagram:

Then, for the naturality of s with respect to the arrow tb, the following diagram (in D ) commutes

for every bÎObB:

50

3. Functors and Natural Transformations

The horizontal composition of s and t is the natural trasformation st: HF®KG defined by,

for every bÎObB, stb = sG(b) ° H(tb) = K(tb) ° sF(b).

We check the naturality of st . Let fÎB[b,b'] , then

stb' ° HF(f) = sG(b') ° H(tb') ° HF(f)

= sG(b') ° H(tb' ° F(f) )

= sG(b) ° H( G(f) ° tb ) by the naturality of t

= sG(b) ° H( G(f) ° tb ) by the diagram

= K(G(f) ° tb) ° sF(b)

= KG(f) ° K(tb) ° sF(b)

= KG(f) ° stb

Note that if we identify the functors K and H with the identity natural transformation idK and

idH, Kt and tH may be understood as particular cases of the horizontal application between natural

transformations (why?).

Exercise Prove the following equality among natural transformations (interchange law):

(n ° m)(t ° s) = (nt) ° ( ms) .

3.3 Cartesian and Cartesian Closed Categories Revisited

By definition, a category C is Cartesian iff it contains a terminal object t , and for every a,bÎObC

there is an object a´b together with two morphisms p1: a´b®a , p2: a´b®b, and for every object c

an isomorphism < , >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:

i. p1 ° <f,g>c = f

ii. p2 ° <f,g>c = g

We want now to show that < , >c is also ’natural in c“, i.e. it satisfies the property:

(nat) for every k: c®c' <f,g>c' ° k = <f ° k, g ° k >c

Indeed, we have <f,g>c' ° k = <p1 ° <f,g>c' ° k, p2 ° <f,g>c' ° k >c by ii)

= < f ° k, g ° k >c by i)

The previous ’naturality“ property suggests that < , > is actually a natural isomorphism. Indeed, let

D: C®C´ C the functor defined by D(c) = (c,c), D(f) = (f,f) (D is called the diagonal functor);

´

then < , > is a natural isomorphism from C´ C[_,(a,b)] ° D to C[_,a´b]. Note that C´ C[_,(a,b)] °

´ ´

D and C[_,a´b]: C®Set are contravariant functors. Conversely suppose to have for all objects a

and b an object a´b and a natural isomorphism t : C´ C[_,(a,b)] ° D @ C[_,a´b]. The naturality

´

of t-1 is expressed by the following commutative diagram:

51

3. Functors and Natural Transformations

Let (q1,q2) = t-1a´b(ida´b) . Note that q1: a´b®a, q2: a´b®b . We want to prove that a´b is a

product with projections q1 and q2. Indeed, let f = tc(h,g): c®a´b in the above diagram, then we

have (q1,q2) ° ( tc(h,g), tc(h,g) ) = t-1c(ida´b ° tc(h,g) ) = (h,g) and, in particular, q1 ° tc(h,g) =

h ; q2 ° tc(h,g) = g .

The previous considerations suggest another characterization of Cartesian Category:

3.3.1 Proposition A category C is Cartesian iff it contains a terminal object t, and for every

a,bÎObC there is an object a´b and a natural isomorphism < , > : C´C[_,(a,b)] ° D ® C[_,a´b].

´

The situation is quite similar, and perhaps even simpler, in the case of exponents. Remember that a

category C is a CCC iff it is Cartesian and has exponents for every pair of objects, i.e. for every a

and b in C there is an object ba together with a morphism evala,b: ba´a®b (evaluation map) and,

for every object c , a function Lc : C[c´a,b]®C[c,ba] such that, for all morphisms f: c´a®b, h:

c®ba, one has

b. evala,b ° (L(f)´ida) = f

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

It turns out that Lc is ’natural in c“, in the sense that for any fÎC[c´a,b], gÎC[d,c]

Lc'(f) ° g = Lc(f ° g´id) ,

In order to check this, recall that (b) corresponds to:

Thus, by twice (Diag.Eval), the following diagram commutes

52

3. Functors and Natural Transformations

Moreover, set L-1 = eval°(_´id).

L-1°L = id

Then by (b)

L°L-1 = id

and by (h).

That is, for each cÎOb C , L c : C[c´a,b]® C[c,b a ] is an isomorphism. Thus L is a natural

isomorphism, by proposition 3.2.3.

Note that, formally, L is a natural transformation from the contravariant functor C[_,b] ° _´a

to the contravariant functor C[_,ba] (where _´a is the product functor defined in the obvious way).

We abbreviate C[_,b] ° _´a as C[_´a,b]. Note also that C[_´a,b], C[_,ba]: C®Set.

Conversely, suppose that, for all objects a and b, there is an object ba and a natural

isomorphism L: C[_´a,b] @ C[_,ba]. Then the naturality of L -1 is expressed by the following

commutative diagram:

Set now evala,b = L-1ba (idba) and note that evala,b: ba´a®b . We want to prove that ba is an

exponent with evala,b as evaluation map . Indeed, let f = Lc(g): c®ba in the above diagram. Then

we have:

evala,b ° ( Lc(g)´id ) = L-1c(idba ° Lc(g) ) = g

This argument gives the following equivalent characterization of CCC:

3.3.2 Proposition C is a Cartesian closed category iff it is Cartesian and for every

a,bÎObC there is an object ba and a natural isomorphism L : C[_´a,b] ® C[_,ba] .

53

3. Functors and Natural Transformations

Observe that definitions 3.3.1 and 3.3.2 require that the category C be locally small, since they are

based on hom-functors. Thus, in a sense, the equational definition is more general.

3.3.3 Remark It is easy to prove that the following (natural) isomorphisms hold in all CCC•s, for

any object A, B, and C:

1. A @ A;

2. t´A @ A;

3. A´B @ B´A;

4. (A´B)´C @ A´(B´C);

5. (A´B)®C @ A®(B®C);

6. A®(B´C) @ (A®B)´(A®C);

7. t®A @A;

8. A®t @ t.

What is worth mentioning, though, is that these are exactly the isomorphisms that hold in all CCC•s,

i.e., no other isomorphism is valid in all CCC's. The proof of this fact is nontrivial and is a nice

application of lambda calculus to categories (an application in the other direction from what is meant

by the title of this book!). Its key idea will be mentioned in chapter 9.

3.4 More Examples of CCC•s

Both examples here derive from bordering areas of (generalized) computability and Proof Theory.

The first, in particular, like many aspects of these theories, is widely used in the type theoretical

understanding of programming languages constructs.

3.4.1 Partial Equivalence Relations

A very relevant example of CCC is suggested by a long story. It began with Kleene•s realizability

interpretation of intuitionistic logic and continued with the work of Kreisel, Girard and Troelstra in

Proof Theory. The idea is to look at functions as computable ones, as in the case of the category EN,

but by a simple and insightful way cartesian closedness is obtained. The approach is also used in the

’quotient-set“ semantics of types, in functional programming. It will give us a paradigmatic structure

in the categorical semantics of polymorphism in PART II.

As usual, let j: w®PR an acceptable goedel numbering of the partial recursive functions. Let

K = (w,.) be Kleene's applicative structure, where . : w´w®w is the partial application

defined by: m.n = j m (n) . A partial equivalence relation R on a set V is a symmetric and

transitive relation, not necessarely reflexive, on V.

(Notation: n R m iff n relates to m in R; {p}R = {q | q R p} ; Q(R) = {{p}R | p R p }) .

54

3. Functors and Natural Transformations

3.4.1.1 Definition The category PER of partial equivalence relations on w has as objects the

symmetric and transitive relations on w. Morphisms are defined by

fÎPER[A,B] iff f : Q(A) ® Q(B) and $n "p (pAp Þ f({p}A) = {n.p}B ) .

Thus, the morphisms in PER are ’computable“ because they are fully described by partial

recursive functions, which are total on the domain of the source relation.

Let now < , >: w´w®w be an effective and bijective pairing. For A,BÎObPER , the product

A´B is defined by

"m,n,m',n' <m,n> A´B <m',n'> Û ( m A m' and n B n').

It is easy to check that this actually defines a product functor in PER.

The exponent object BA is defined by

"m,n, m (BA) n Û "p,q (p A q Þ m.p B n.q ) .

Cartesian closedness follows by giving a natural isomorphism L : PER[A´C,B] @ PER[A,BC].

Let s be the recursive function of the s-m-n (or iteration) theorem, i.e. js(n,p)(q) = jn(p,q). Then

set L(f)({p} A ) = {s(n,p)}C® B , where n is an index for f. In other words {n.<p,q>} B =

{s(n,p).q}B. Observe that L is a well-defined function from PER[A´C,B] to PER[A,BC], since

s is computable and, then, any index for the recursive function p |_ s(n,p), computes

L(f)ÎPER[A,BC]. As for the naturality of L , one may prove it by the argument above, which also

gives some information on the evaluation map.

Let evalA,B: BA´A®B be defined by eval( {<m,n>}BA´A ) = {m.n}B.

In order to prove that evalA,B is a morphism in the category we must find eA,BÎw such that

eval({<m,n>}BA´A ) = {m.n}B = {eA,B.(<m,n>)}B

Let u be the ’universal“ function, i.e., the partial recursive function such that u(<m,n>) = m.n , and

let e be an index for it, i.e., u = je. It is easy to observe that one can set eA,B = e for all A, B in

ObPER, since

{e.(<m,n>)}B = {u(<m,n>)}B = {m.n}B .

Then, (b) is simply

eval({<s(n,p),q>}BA´A ) = {n.<p,q>}B, by definition of s .

Similarly for (h).

3.4.2 Limit and Filter Spaces

There is an elegant, unifying way to understand the various approaches to generalized computability

proposed in the 60•s and 70•s. The connecting point is the construction of categories of sets where a

suitable notion of limit gives an abstract notion of computability. The idea is to generalize the

technique used when defining the computable elements in Scott domains D (see 2.4.1), in the way

explained below (in short, the computable elements are the limits of recursively enumerable indexed

55

3. Functors and Natural Transformations

sequences.) This suggests several CCC's, such as limit spaces (L-spaces) and filter spaces (FIL)

with their relevant subcategories. They will be introduced here and discussed also in the examples in

section 5.3 and section 8.4, toghether with other ideas for higher type computations.

3.4.2.1 Definition A limit space (L-space) (X,¯) is a set X and a relation (convergence)

between countable sequences {xi}iÎw Í X and elements xÎX (notation: {xi}¯x) such that

1. if all but finitely many xi are x, i.e., {xi} is eventually x, then {xi}¯x;

2. if {xi}¯x and k(0) < k(l) < . . . < k(n) < . . . , then {xk(i)}¯x;

3. if not({xi}¯x), then there is k(0) < k(l) < . . . < k(n) < . . . such that for no subsequence

h(0) < h(l) < . . . < h(n) < . . . one has {x(i)}¯x.

An L-space (X,¯) has a countable basis (is separable) iff for some given countable Xo Í X,

"xÎX ${xi}ÍXo {xi}¯x.

From now on we assume that each countably based L-spaces (X,¯) comes with a given

surjective enumeration e: w®Xo of the base. An immediate example of separable L-spaces is the set

of real numbers endowed with the usual notion of sequence converge (Cauchy).

3.4.2.2 Definition The hom-set L[X,Y] between L-spaces (X,¯) and (Y,¯) consists of all

continuous functions, i.e.,

fÎL[X,Y] iff "xÎX "{x i}¯x {f (xi )}¯f (x),

where convergence is given in the intended spaces.

This category has exponents and products, as (L[X,Y],¯) also is an L-space by

{fi}¯f iff "xÎX, "{xi}¯x {fi(xi)}¯f(x) ,

while products are given by componentwise convergence.

Finally, eval: L[X,Y]´X® Y, with eval(f,x) = f(x), is continuous. As a matter of fact,

(L[X,Y],¯) is the coarsest limit structure (i.e., with more converging sequences) such that eval is

continuous.

One can also show that if (X,¯) and (Y,¯) are separable, then also (L[X,Y],¯) is separable.

Indeed, L-spaces and separable L-spaces, with continuous maps as morphisms, form Cartesian

closed categories.

Yet another CCC of limit spaces may be given by the Moore-Smith net-convergence or,

equivalently, by filter-convergence. Just recall that a filter F (on a given set X) is a set of (sub)sets

closed by intersection and such that AÎF and A Í B imply BÎF (e.g., the collection of subsets

of A which contain a given xÎA is the (ultra)filter generated by x). A filter base is a non empty

collection of non empty subsets of X such that AÎF and BÎF imply $CÎF C Í AÇB. A filter

base F generates a unique filter [F] = {B Í X | $AÎF A Í B}. Define then

56

3. Functors and Natural Transformations

3.4.2.3 Definition (X, F) is a filter space iff "xÎX F(x) is a filter of filters such that the

ultrafilter generated by x is in F(x). Given a filter base F , we write F¯x iff [F]ÎF(x) .

Exercise Prove that the category FIL of filter spaces with continuous maps (where f is

continuous iff F¯x implies f(F)¯x) is a CCC. Give a full and faithful functor F : FIL®L-

spaces. (Hint: a filter structure on FIL[X,Y] is given by X¯f iff F¯x implies X(F)¯f(x),

where X(F) is the set of all W(U) with WÎX and UÎF and W(U) = È{f(U) | fÎW};

moreover, given a filter F and a sequence {xi}, define Con(F,{xi}) iff "UÎF $k "n³k xnÎU

and set {xi}¯x iff $F¯x Con(F,{xi}) ).

A notion of separable filter space is easily given, by taking a countable base of filters (i.e., a

countable collection of sets such that each converging filter is generated by elements of the base).

Clearly, each (separable) topological space (X, top) may be turned into a (separable) filter space:

just take, for each point x , the collection F(x) of all filters containing the filter of neighborhoods of

that point. The reader will have a better insight into the ’injections“

Top ® FIL ® L-spaces

when looking at examples of adjunctions, in section 5.3. As for now, it may suffice to say that there

exist filter spaces whose limit structure is not topological. Some of these filter spaces are among those

needed for the study of the total computable functionals.

In the very general setting of L-spaces we can now hint a notion of computability which

specializes to the one given over Scott domains, when the intended limit structure is derived from the

Scott topology.

Let R be the total recursive functions and (X, X0, e, ¯) a separable L-space, where e is a

given enumeration of the base X0. Define then, in a slightly incomplete way (see the comment

below), the collection Xc Í X of computable elements by xÎXc iff $fÎR {ef(i)}¯x.

In other words, given a countably based limit structure, an element is computable (or recursive) when

it is the limit of a countable sequence indexed over an r.e. set.

Comment L-spaces actually carry too little structure to yield a good definition of ’recursive“ just by

taking arbitrary limits of recursively enumerable converging sequences. Their simplicity and

generality, though, should give an immediate intuition of what is going on. Indeed, the technique in

the definition of computability tidily borrows from similar methods in mathematics. Consider, say,

’smooth manifolds.“ They are defined on the base of the familiar notion of differentiability in Rn,

which is extended by a system of local coordinates to abstract spaces. Similarly here, one takes for

granted the recursive functions and extends computability to an abstract setting (and higher types, in

57

3. Functors and Natural Transformations

particular) by ’local“ properties of convergence as in the equation above. As we shall see later, too,

the categorical language relates and unifies the various classes of structures where this is done.

L-spaces suggest how to express computability by limits very simply; however, the weakness of

these structures is that limits are far away from being uniquely determined and that there is no

obvious way to characterize ’interesting“ sequences and limit points.

The point then is to take only ’some“ limits. This is done by directed sets in Scott domains (see

2.4.1), which are particular converging sequences with a privileged limit, the least upper bound. It

will be described for FIL in the examples at the end of section 5.3.

3.5 Yoneda's Lemma

Let C be a Cartesian closed category. Let F = C´ C[_,(a,b)] ° D : C®Set, G = C[_´a,b]: C®Set.

´

In ¤3.3 we proved that for both F and G there exists an object, respectively called a´b and ba,

such that F @ C[_,a´b] and G @ C[_,ba]. In general, functors which enjoy this property are

called (co-)representable. The formal definition, in case of covariant functors, is the following

(note that F and G are contravariant; we leave as an exercise for the reader to derive the dual

definition) :

3.5.1 Definition A functor K: C®Set is representable iff there exist an object r in C and a

natural isomorphism f: K @ C[r,_].

Exercise Give another definition of CC and CCC by using the previous notion.

Note that, if K: C®Set, every natural transformation j: C[r,_]®K is fully determined by the

image of the identity idr . Indeed, for every fÎC[r,d], jd(f) = jd(f ° idr) = K(f) ° jr(idr) , by the

following diagram:

3.5.2 Lemma (Yoneda) Let K: C®Set be a functor. The map y r,K : Nat(C[r,_], K)®K(r)

that takes every natural transfomation j: C[r,_]®K to j r (id r )ÎK(r) is an isomorphism.

Moreover, it is natural in r and K , that is,

58

3. Functors and Natural Transformations

( where C[f,_] : C[d,_] ® C[r,_] is the natural transformation defined by C[f,_]c = C[f,c] = _° f :

C[d,c]®C[r,c]; see example 3.3.2 ), and

Proof By the Yoneda diagram above and a routine verification of the commutativity of the diagrams

in the definition. ¨

If we take K in the previous lemma to be C[d,_], where d is a generic object in C, this results in

the statement that there is a natural bijection between arrows gÎC[d,r] (that is, elements in

C[d,_](r)) and natural transformations from C[r,_] to C[d,_].

3.5.3 Proposition (Yoneda embedding)

i. Let Y be the map which takes every rÎObC to the hom-functor C[r,_], and every gÎC[d,r] to

the natural transformation C[g,_]: C[r,_]® C[d,_] defined by C[g,_] c = C[g,c] = _° g :

C[r,c]®C[d,c]. Then Y is a full embedding from Cop to Funct(C,Set) .

ii. Let Y be the map which takes every rÎObC to the hom-functor C[_,r] , and every gÎC[d,r]

to the natural transformation C[_,g]: C[_,d]®C[_,r] defined by C[_,g] c = C[c,g] = g ° _ :

C[c,d]®C[c,r] . Then Y is a full and faithful covariant functor from C to Funct(Cop,Set).

Proof We prove only (i), since the other proof is dual.

Y(idr) = idC[r,_] is immediate. Given gÎC[d,r], fÎC[s,r], Y(f°g): C[s,_]®C[d,_] is defined

as follows: for every cÎObC Y(g °f)c = _° f ° g : C[s,c]®C[d,c]. Y is a functor, as, for every

hÎC[s,c],

Y(g ° f)c(h) = h ° f ° g

= Y(g)c(f ° h)

= Y(g)c( Y(f)c(h) )

59

3. Functors and Natural Transformations

= ( Y(g)c ° Y(f)c )(h).

The fact that Y is full and faithful follows, as already observed, from the Yoneda lemma with

C[d,_] instead of K. ¨

3.6 Presheaves

In the last section we proved that every small category C is isomorphic to a full subcategory of

F u n c t (C o p ,Set) through the Yoneda embedding Y. For its relevance, the category

Funct(C op ,Set) has its own name: a functor F: C op ’®Set is called presheaf on C, and

Funct(Cop,Set) is the category of presheaves on C.

The category of presheaves inherits many interesting properties from Set, and in particular it is

itself a topos. For the moment, we only prove the following properties:

3.5.1 Theorem Given a category C, the category of presheaves on C has pullbacks for every pair

of morphisms and is Cartesian closed.