<<

. 2
( 10)



>>

°f+ = idX, i.e., that X<Y via ( f+,f-) in Stab.

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.

<<

. 2
( 10)



>>