<< стр. 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

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

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)СОДЕРЖАНИЕ >>