A diagram of this type in a category C is a given by three objects, a, c, and b, and two morphisms,

fÎC[a,c] and gÎC[b,c]. A cone to this diagram is an object d, together with three morphisms

haÎC[d,a], hcÎC[d,c] and hbÎC[d,b], such that the following diagram commutes:

A cone (d, {ha, hb, hc}) is a limit, if for any other cone (d', {h'a, h'b, h'c}) there exists a unique

arrow k: d'®d such that h'i = hi ° k, for iÎ{a,b,c}.

The commutativity of the previous diagram implies that f ° ha = g ° hb; conversely, given two

arrows ha and hb such that f ° ha = g ° hb, one obtains a cone by defining hc = f ° ha = g ° hb.

Thus, the diagram for the cone (d, {ha, hb, hc}) is equivalently expressed by giving only the outer

commutative ’square“, i.e., by giving (d, {ha, hb}). In conclusion, a universal cone for a diagram

of this type turns out to be just a pullback.

As usual, by taking the colimit of the same diagram we obtain the dual notion of pushout.

124

6. Cones and Limits

6.3 Existence of limits

In this secton, we study the important question about the existence of limits in a given category.

Starting with the familiar category of sets, we generalise a common construction that allows the

existence of complex limits to be states, provided that simpler ones exist.

Note first that every diagram D has limit in Set. It is obtained as follows.

Let {Di}iÎI be a family of objects in D and consider the object P iÎID i, i.e., the product

indexed by I. The elements of PiÎIDi are tuples {x0, x1, x2, ...} such that xiÎDi, for all iÎI,

or equivalently functions f : I•®ÈiÎIDi, such that f(i)ÎDi .

PiÎIDi has projections pi : PiÎIDi®Di for all iÎI, defined by pi({x0,x1,x2, ...}) = xi. In

general these projections do not form a cone on D, that is, if fe: Di®Dj is an edge of D, one may

have pj ¹ fe°p i . The idea is to take the subset L of P iÎID i of all the tuples that satisfy the

condition pj = fe°pi. That is, {x0, x1, x2, ...}ÎL if and only if, for all edges fe: Di®Dj, one has

xj = fe(xi). Let then gi be the projection pi restricted to L. Then (L,{ gi Î C[L,Di] | i Î I}) is

the limit (prove it as an exercise).

This set-theoretic construction is better formalized in Category Theory in the following way.

Let P(D j / $iÎI $eÎE fe : Di®D j ) be the product of all codomains of edges in D, with

projections pj: P(Dj / $iÎI $eÎE fe: Di®Dj ) ® Dj. By definition of product, there is a unique

function

y1: PiÎIDi® P(Dj / $iÎI $eÎE fe: Di®Dj )

such that pj = pj°y1 for any edge fe: Di®Dj of D. Analogously there is a unique function

y2: PiÎIDi® P(Dj / $iÎI $eÎE fe: Di®Dj )

such that fe°pi = pj°y2 for any edge fe: Di®Dj of D.

This is visualized in the following diagram:

Note now that, in set-theoretic terms, for all the tuples {x0, x1, x2, ...} in PiÎIDi the following

properties are equivalent:

1. for all edges fe: Di®Dj, xj = fe(xi)

2. y 1 ({x0 , x1 , x2 , ...}) = y 2 ({x0 , x1 , x2 , ...})

125

6. Cones and Limits

Then, what we are looking for is the maximal subset L of PiÎIDi whose elements satisfy (2), but

we aleady know that this is none other than the equalizer of y1 and y2. By a diagram,

We are now ready to generalize to every category C the previous construction of limits in Set.

6.3.1 Theorem Let D be a diagram in C with sets I of vertices and E of edges. If every I-

indexed family and every E-indexed family of objects has a product, and every pair of morphisms

has an equalizer, then D has a limit.

Proof Exercise (use the previous diagrams). ¨

6.3.2 Corollary If a category C has arbitrary products, and equalizers for every pair of

morphisms, then every diagram has a limit.

6.3.3 Corollary If a category C has all finite products, and coequalizers for every pair of

morphisms, then every finite diagram has a limit.

The relevance of theorem 6.3.1 is that, in general, it is simpler to check the existence of products and

equalizers than to prove directly the existence of limits.

Example Corollary 6.3.2 may be used to prove that every diagram has a limit in CPO. If {Ci}iÎI

is a family of c.p.o.•s, let P iÎICi be the product indexed by I . P iÎICi may be given a c.p.o.

structure by the componentwise order, that is, (ci)iÎI £ (di)iÎI iff " iÎI ci £ di. The projections

pi: PiÎI(Ci)®Ci are defined by pi( (ci)iÎI ) = ci . It is easy to prove that PiÎI(Ci) is indeed a

cpo, that the projections are continuous, and that PiÎI(Ci) satisfies the universal property of the

product.

Given f,g : A®B , their equalizer is h: A'®A, where A' = {aÎA / f(a) = g(a)} with the

ordering inherited by A, and h is the injection. A' is a c.p.o. Indeed, let D be a direct subset of

126

6. Cones and Limits

A'; then D is also a direct subset of A, and thus f(ÈD)= ÈaÎDf(a) = ÈaÎDg(a) = g(ÈD). By

this, ÈDÎA'. The continuity of h and the universal property for equalizers are easy to prove.

In propositions 2.5.5 and 2.5.6 we showed how to define products and equalizers from terminal

objects and pullbacks. This suggests an even simpler sufficient (and necessary) condition for the

existence of all finite limits.

6.3.4 Corollary If C has a terminal objects and pullbacks for every pair of morphisms, then it has

all finite limits.

Exercise State the dual versions of theorem 6.3.1 and corollaries 6.3.1 to 6.3.4.

6.4 Preservation and Creation of Limits

In this section we study some cases of functors which ’preserve“ the property of objects to be limits

of a diagram.

6.4.1 Definition Let G: A®X be a functor, and let (a,{ti Î A[a,di] | iÎI}) be an universal cone

from a on the diagram D in A. We then say that G preserves the limit (a,{t i Î A[a,di] |

iÎI}) if and only if (Ga,{Gti Î X[Ga,Gdi] | iÎI}) is an universal cone from Ga on the diagram

G(D) in X . Preservation of colimits is defined dually.

6.4.2 Theorem If the functor G: A®X has a left adjoint F: X®A, and the diagram D =

({di}iÎI, {fe}eÎE) in A has limit (a, {tiÎA[a,di] | iÎI} ), then G(D) = ({Gdi}iÎI, {Gfe}eÎE )

has a limit in X, and the limit is (Ga,{GtiÎX[Ga,Gdi] | iÎI}).

Proof By the properties of functors, ({Gdi}iÎI, {Gfe}eÎE ) is a cone; we only need to prove that

it is universal. Let (x,{siÎX[x,Gdi] | iÎI}) be another cone, and let j: A[Fx,di] @ X[x,Gdi] be

the isomorphism of the adjunction. Then (Fx, {j-1(si)ÎA[Fx,di] | iÎI}) is a cone. Indeed, for all

fe: di®dj one has

fe°j-1(si) = j-1(G(fe)°si) by naturality

= j-1(sj) because (si) is a cone on G(D) .

By the universality of (a, {tiÎA[a,di] | iÎI} ) there exists a unique arrow h: Fx®a such that

"iÎI ti°h = j-1(si). Take then j(h): x®Ga. Since Gti°j(h) = j(ti°h) = si, one has that j(h) is

a mediating morphism between the cones (x, {siÎX[x,Gdi] | iÎI}) and (Ga, {GtiÎX[Ga,Gdi] |

iÎI}).

127

6. Cones and Limits

Moreover, j(h) is unique, for, if j(h') is another mediating morphism, then h' is a mediating

morphism between (Fx,{j-1(si)ÎA[Fx,di] | iÎI}) and (a, {tiÎA[a,di] | iÎI} ). By universality,

h' = h (see the diagram below). ¨

The proof of theorem 6.4.2 may be visualized by the following commutative diagrams:

Exercise Give the dual statement of theorem 6.4.2 .

An example of application of (the dual of) theorem 6.4.2 is the following.

6.4.3 Theorem In every Cartesian closed category C, products distribute over colimits.

Proof Just note that by definition of CCC the functor -´a: C®C has a right adjoint for each

aÎObC, and apply the dual of theorem 6.4.2. ¨

6.4.4 Corollary Let C be a CCC. Suppose, moreover, that it contains an initial object 0, and

coproducts for each pair of objects. Then, for all X,Y,ZÎObC, one has

i. 0 x Z @ Z

ii. (X + Y) x Z @ (X x Z) + (Y x Z)

Exercises (Huwig-PoignŽ) A category C has fixpoints if for every morphism f: X´X'®X'

there exists a morphism Y(f): X®X' such that f ° <idX,Y(f)> = Y(f). Prove then the following

facts:

1. CPO has fixpoints.

2. If C is a CCC and it has an initial object 0 and fixpoints, then it is inconsistent , i.e. all objects

are isomorphic. (Hint: let t the terminal object, and consider the projection p2: tx0®0. Then

Y(p2): t®0. Deduce from this an isomorhism between 0 and t ...) .

3. (difficult) If C is a CCC and it has fixpoints and binary coproducts, then C is inconsistent. Hint:

consider the object 2=t+t and interpret the injection tt: t®2 and ff: t®2 as denoting ’truth“ and

128

6. Cones and Limits

’falsehood.“ Then all finitary truth tables can be expressed by morphisms in 2´2´....´2 ®2. The

existence of a fixpoint for ’not“ induces the following identities:

tt = Y(not) or not(Y(not)) = Y(not) or Y(not) = Y(not)

ff = Y(not) and not(Y(not)) = Y(not) and Y(not) = Y(not)

Hence the injections tt , ff : t®2 are identified. As, for all objects X in C, X+X = (t´X) + (t´X)

= (t+t)´X , one may deduce the equality of the coproduct injections u,v: X®X´X for all X . By

this it is easy to obtain the inconsistency.

Fixed points will be widely discussed in chapter 8. The reader may already understand, though,

that from the point of view of denotational semantics, this is a negative result: coproducts (i.e.

disjoint sums) are incompatible with fixed point operators. As is well known, both constructions are

rather relevant in semantic domains.

Another important case of limit-preserving functor is the hom-functor.

6.4.5 Theorem Let C be a small category. For any object cÎObC, the hom-functor hom[c,_]:

C®Set preserves limits.

Proof: Consider the diagram D = ( {di}iÎI, {fe}eÎE) in C, and let (a, {tiÎA[a,di] | iÎI} ) be a

limit. We must prove that the diagram S = ({hom[c,di]}iÎI, {fe ° _}eÎE ) has a limit in Set.

Take L = (hom[c,a],{ti ° _ : hom[c,a]®hom[c,di] | iÎI}) as a limit.

Since hom[c,_] is a functor, L is a cone for S. We have only to prove that it is universal.

Suppose then that L' = ( X, {gi : X®hom[c,di] | iÎI}) is another cone for S. This means that for

any fe: di®dj, and any xÎX, fe ° gi(x) = gj(x). For any xÎX, ( c, {gi(x): c®di | iÎI}) is then a

cone for D, and by universality of (a, {tiÎA[a,di] | iÎI} ), there exists a unique morphism hx:

c®a in C such that gi(x) = ti ° hx for all i. Define then h: X®hom[c,a] by h(x) = hx. We have

(ti ° _) ° h = gi, since for every xÎX , ti ° h(x) = ti ° hx = gi(x). Unicity follows by unicity of hx

for any x. ¨

Exercise Use theorem 6.4.5 and prove theorem 6.4.2 in case the categories considered are small.

4.6 Definition A functor F: A® X creates limits for a given diagram D if, whenever (x,

{siÎX[x,F(di)] | iÎI}) is a limit for F(D) in X, then there exists a unique cone (a, {ti ÎA[a,di] |

iÎI}) over D in A, such that F(a) = x and F(ti ) = si for every iÎI, and (a,{ti Î A[a,di] |

iÎI}) is a limit.

Example The forgetful functor U from Grp to Set creates all limits. For instance, the fact that it

creates products is another way of stating that, given two groups G and G', there is a unique

group structure on U(G)´U(G'), which gives their product in Grp.

129

6. Cones and Limits

6.5 w -limits

An important case of diagrams in a category C is that of infinite chains of objects. These diagrams,

and the associated limits, are particularly relevant for the denotational semantics of programming

languages, since they provide the base for the solution of recursive domain equations with the so-

called least fixed point technique (see chapter 10)

6.5.1 Definition

i) An w-diagram in a category C is a diagram with the following structure:

(dually, one defines w OP-diagrams by just reversing the arrows).

ii. A category C is w -complete (w -cocomplete) iff it has limits (colimits) for all w-diagrams.

w

iii. A functor F: C®C is w -continuous iff it preserves all colimits of w-diagrams.

If C is a partial order then,

i. an w-diagram in C is an w-chain

ii. C is w-cocomplete if and only if C is a cpo

iii. a functor F: C®C is w-continuous iff the associated function on object of C is continuous.

6.5.2 Theorem Let C be a category with initial object 0. Let F: C®C be an w-continuos

(covariant) functor and zÎC[0,F(0)] be the unique arrows defined by the initiality of 0. Assume

also that (c, {tiÎC[F i(0),c]iÎw }) is a colimit for the w-diagram ({Fi(0)}iÎw , Fi(z)}iÎw ),

where F0(0) = 0 and F0(z) = z. Then c @ Fc .

Proof By the hypothesis, one has that (Fc, {Ft i Î C [F i+1 (0),Fc] iÎ w }) is a limit for

({Fi+1(0)}iÎw, {Fi+1(z)}iÎw) and (c, {ti+1ÎC[Fi+1(0),c]iÎw}) is a cone for the same diagram.

Thus, by universality, there exists a unique arrow h: Fc®c such that "iÎw h ° Fti = ti+1. Now

add to (Fc, {FtiÎC[Fi+1(0),Fc]iÎw }) the unique arrow zFcÎC[0,Fc]. This gives a cone for

({Fi(0)}iÎw , {Fi(z)}iÎw ) and, by the universality of (c,{ti Î C[Fi(0),c]iÎw }), there exists a

unique arrow k: c®Fc such that "iÎw k ° ti+1 = Fti (of course k ° t0 = zFc ). But, then, "iÎw

h ° k ° ti+1 = h ° Fti =ti+1 (and h ° k ° t0 = t0), thus h°k is a mediating morphism between (c,

{tiÎC[Fi(0),c]iÎw}) and itself. Thus, by unicity, h°k = id.

In the same way, one proves that k ° h = id. ¨

This is all summarized by the following diagram:

130

6. Cones and Limits

Theorem 6.5.2 tells us how to give meaning to recursive definitions of data types under certain

circumstances. Very informally, assume that types are interpreted as objects of a category. Then in a

recursive definition X = [...X...] of a data type of data X, the transformation [... _ ...] may be

understood as an endofunctor F(_) for which we are seeking a fixed point. Indeed, if F satisfies

the properties in theorem 6.5.2, then the theorem ’solves“ the equation (or recursive definition) X =

[...X...]. In a sense, this construction gives meaning to X = [...X...], over a suitable categorical

structure, in the same way that the equation x = x2+7 is ’given meaning“ over the complex numbers

by finding a solution for it.

However, the assumptions on F are too strong and leave out several significant cases (e.g.,

hom-functors or exponents). Chapter 10 is entirely devoted to a nontrivial extension of this technique

in order to handle a more relevant class of recursive definitions of data types.

References Main textbooks.

131

7. Indexed and Internal Categories

Chapter 7

INDEXED AND INTERNAL CATEGORIES

7.1 Indexed Categories

In this section we introduce the basic notions of the Theory of Indexed Categories. In order to

improve readability, the following exposition is an (over)simplification of the usual, and more

general, approach. In particular, many of the concepts we define up to equality can be defined up to a

fixed collection of canonical isomorphisms. In this case, the indexed notions introduced in the theory

are required to satisfy a suitable set of coherence conditions, which play a quite marginal role, but

conversely can easily puzzle the reader who is approaching the Theory of Indexed Categories for the

first time. The reader who is interested in more notions in this branch of Category Theory should

consult the References.

7.1.1 Definition Let CAT be the (meta)category of all categories, and S be a category. An S-

indexed category is a functor A: Sop ®CAT .

More explicitly, an S-indexed category A is defined by the following data:

i. for every object s of S, a category A(s), called the category of s-indexed families of objects of A;

ii. for every morphism f: s®s' of S, a functor A(f): F(s')®F(s), called the substitution functor

determined by f, and frequently denoted as f*.

Example A simple but important example is the S-indexing S/: Sop®CAT of S itself. S/ takes

every object r of S to the comma category S/r. Remember that the objects of S/s are arrows h: s®r

with codomain r. These arrows should be intuitively thought of as families {h-1(i)/ iÎr}. If f:

s®s' is an arrow of S, then f* : S/s'®S/s is the pulling back functor. Note that pullbacks are

usually defined only up to isomorphism, while we are here implicitly supposing a canonical choice.

As a matter of fact, the pullback and the associated ’functor“ are the basic examples of notions

profitably defined up to isomorphism, which we mentioned in the introduction.

7.1.2 Definition Let A, B: Sop®CAT be two S-indexed categories.

1. The product category A´B: Sop ®CAT is defined by

A´B(s) = A(s)´B(s)

A´B(f) = A(f)´B(f);

2. The dual category Aop: Sop®CAT is defined by

Aop(s) = A(s)op

132

7. Indexed and Internal Categories

Aop(f) = A(f)op

where A(f)op : A(s')op®A(s)op is the defined in the obvious way;

3. If r is an object of S, the S-indexed category Ar is defined by

Ar(s) = A(r´s)

A(f) = A(idr´f).

7.1.3 Definition Let A, B be two S-indexed categories. An S-indexed functor H: A®B is a

natural transformation from A: Sop®CAT to B: Sop®CAT.

Thus, an S-indexed functor H: A®B is a collection of functors H(s): A(s)®B(s), for s object of

S, such that for any f: s®s' in S, H(s) ° A(f) = B(f) ° H(s') (H(s) ° f* = f* ° H(s').

Given two indexed functors H: A®B and K: B®C, their composition K ° H : A®C is defined

component-wise (being the composition of natural transformations), i.e., (K ° H)(s) = K(s) ° H(s).

The identity idA: A®A, is the identity natural transformation from A to A.

7.1.4 Definition Let H: A®B, K: A®B, be two S-indexed functors. An S-indexed natural

transformation t: H®K consists of a natural transformation t(s): H(s)®K(s) for any object s

of S such that, for any f: s®s' in S,

t(s) ° A(f) = B(f) ° t(s') (t(s) ° f* = f* ° t(s') ) .

()

The previous definition is more complex than it seems at first sight. Note that t(s): H(s)®K(s),

t(s'): H(s')®K(s') are natural transformations, while A(f): A(s')®A(s) and B(f): B(s')®B(s) are

functors. We are thus composing natural transformations and functors in the way described at the end

of section 3.2. t(s) ° A(f) and B(f) ° t(s') are natural transformations of the following type:

t(s) ° A(f) : H(s) ° A(f) ® K(s) ° A(f)

B(f) ° t(s') : B(f) ° H(s') ® B(f) ° K(s').

But, according to the definition of S-indexed functors, for any f: s®s', one has H(s) ° A(f) = B(f) °

H(s') and K(s) ° A(f) = B(f) ° K(s'), thus equation ( ) is well typed.

Spelling out the composition of natural transformations and functors in ( ), we have for any f:

s®s' in S and any object a in A(s'),

t(s)A(f)(a) = B(f)(t(s')a)

where the previous equation holds in the category B(s).

The previous situation can be summarized in the following diagram:

133

7. Indexed and Internal Categories

(Vertical) composition of S-indexed natural transformations is defined componentwise, that is, given

H, K, L : A®B,t: H®K and r: K®L, r ° t: H®L is given by (r ° t)(s) = r(s) ° t(s). This is a

good definition since, for any f: s®s' in S and any object a in A(s'),

(r ° t)(s)A(f)(a) = (r(s) ° t(s))A(f)(a)

= r(s)A(f)(a) ° t(s)A(f)(a)

= B(f)(r(s')a) ° B(f)(t(s')a)

= B(f)(r(s')a ° t(s')a)

= B(f)((r ° t)(s')a).

7.1.5 Definition Let A, B be S-indexed categories, H: A®B, K: B®A be S-indexed functors,

and h: idA®K°H, e: H°K®idB be S-indexed natural transformations. <H, K, h, e> : A®B is an

S-indexed adjunction if and only if

(Ke) ° (hK) = idK

(eH) ° (Hh) = idH .

The notion of indexed adjunction is the obvious generalization of the usual notion of adjunction. In

particular it is easy to check that for any object s of S, <H(s), K(s), h(s), e(s)> : A(s)®B(s) is an

adjunction in the usual sense.

The main problem with the definition of adjunction as a quadruple <H, K, h, e> : A®B is in its

generalization of the case with parameters (remember that the definition of exponents requires an

adjunction of this kind). As a triple, an indexed adjunction can be defined in the following, somewhat

informal, way:

7.1.6 Definition Let A, B be S-indexed categories, and H: A® B, K: B® A be S-indexed

functors. <H, K, f> : A®B is an S-indexed adjunction if and only if, for every f: s®s' in S,

134

7. Indexed and Internal Categories

i. <H(s), K(s), f(s)> : A(s)®B(s) is an adjunction

ii. f(s) ° B(f) = A(f) ° f(s') ( f(s) ° f* = f* ° f(s') )

Equation ii expresses the naturality of the isomorphism f with respect to the index s. Spelling out

the composition in ii, we can say that for any f: s®s', a in A(s'), b in B(s'), and g: H(s')(a)®b in

B(s'),

f(s)A(f)(a),B(f)(b) (B(f)(g)) = A(f) (f(s')a,b(g))

Suppose we have an adjunction <H, K, h, e> : A®B. Then we obtain f in definition 7.1.6 by

letting, for any a in A(s), b in B(s), and g: H(s)(a)®b in B(s),

f(s)a,b(g) = e(s)b ° H(s)(g)

As we know from chapter 5, for any s in S, f(s) a,b : B(s)[H(s)(a),b]® A(s)[a,K(s)(b)] is an

isomorphism. We now prove that the previous definition of f(s) satisfies equation ii in definition

7.1.6. For any f: s®s', a in A(s'), b in B(s'), and g: H(s')(a)®b in B(s'), we have

A(f) (f(s')a,b(g)) = A(f) (e(s')b ° H(s)(g)) by def. of f(s')

= A(f) (e(s')b) ° A(f) (H(s)(g)) since A(f) is a functor

= e(s)B(f)(b) ° H(s)(B(f)(g)) by naturality of e and H

= f(s)A(f)(a),B(f)(b) (B(f)(g)) by def. of f(s)

Conversely, given an adjunction <H, K, f> : A®B, we obviously obtain h, e by the following:

h(s)a = f(s)a,H(s)(a)(idH(s)(a)) : a®K(s)H(s)a

e(s)b = f(s)-1K(s)(b),b(idK(s)(b)) : H(s)K(s)b®b.

Definition 7.1.6 has a straightforward generalization to the case with parameters.

7.1.7 Definition Let A, B, D be S-indexed categories, and H: A´D®B, K: Dop´B®A be S-

indexed functors. <H, K, f> : A® B is an S-indexed adjunction with parameters in D if

and only if, for every f: s®s' in S,

i. <H(s), K(s), f(s)> : A(s)®B(s) is an adjunction with parameters in D(s);

ii. f(s) ° B(f) = A(f) ° f(s') ( f(s) ° f* = f* ° f(s') ).

135

7. Indexed and Internal Categories

7.2 Internal Category Theory

A category C is small when the collection MorC of its morphisms is a set. Clearly, then, the

collection ObC of objects of C is also a set. Moreover, there are set-theoretic functions DOM,COD:

MorC®ObC that specify source and target of every morphism, a function ID: ObC®MorC that

defines the identity morphism for every object, and a partial function COMP: MorC´MorC®MorC

for the composition. Given two morphisms f and g, their composition is defined if and only if

DOM(f) = COD(g); the domain of COMP is thus the set {(f,g) | DOM(f) = COD(g)}, that is, the

pullback of the two functions DOM,COD: MorC®ObC. All these functions must also satisfy the

obvious equations stating the behavior of the identity morphism with respect to composition, the

associativity law for compositition, and the rules which specify domain and target for the identity

morphism and for the result of a composition. Thus every small category may be completely

described internally to the category Set, which becomes a sort of ’universe of discourse.“ The

previous discussion, however, has made very little use of the specific structure of Set; we only

needed the existence of pullbacks in order to define the correct domain of the function COMP. In this

section, we will show that most of the basic definitions of Category Theory, such as category,

functor, natural transformation and so on, can be recasted inside any category with all finite limits.

This means that any such a category may be considered a fairly big universe inside which we can

carry out constructions with almost the same confidence as we do in Set. This branch of Category

Theory is known as ’internal,“ since it describes notions of Category Theory by using the categorical

language as a metalanguage.

For many fields of mathematics, from Set Theory to Algebra and Geometry, treatments in the

language of Category Theory, even of well-known results, have never been worthless since most of

the time they created a new, sometimes unexpected, sense of explanation. The same holds for

Category Theory itself: in a sense, Internal Category Theory plays with respect to the general theory

the same role that Category Theory plays with respect to Set Theory. If a notion of Category Theory

cannot be described internally in a simple way, then there is surely something in that notion that is

worth spelling out. As we shall see, this is, for example, the case of the hom-functor and, more

generally, of every presheaf.

Internal Category Theory allows us to work in different universes than Set. This possibility

turns out to be very relevant in several cases, and in particular for the application we aim at in chapter

11, where Internal Category Theory will be applied to the study of categorical models for the

polymorphic lambda calculus. In that case, the possibility of working in more constructive categories

than Set turns out to be essential, as it is known that the standard set-theoretic interpretation of the

first order typed lambda calculus cannot be extended to a model of the second order typed lambda

calculus.

136

7. Indexed and Internal Categories

In the following, E will always denote a category with all finite limits. Our first step is to mimic

within E the presentation, within Set, of a small category. Thus the collections of objects and

morphisms will be viewed as objects of E.

Notation We write X´0Y (instead of X´ZY) for the pullback of X and Y along morphisms with

common target Z; <,>0 will be used as a ’pullback pairing“ map, that is, given (suitable) h:W®X

and k:W®Y, we have <h,k>0 :W®X´ 0 Y; the pullback projections will be usually (but not

always) denoted by the upper case Greek letter P, indexed with a number or some other symbol.

7.2.1 Definition c = (c0 ,c1 ,DOM,COD,COMP, ID) is an internal category of E (cÎCat(E))

iff:

c0, c1ÎObE

DOM, COD : c1 ® c0

COMP : c1 ´0 c1 ® c1 where c1 ´0 c1 is the pullback of DOM, COD : c1®c0

ID : c0 ® c1

and moreover

137

7. Indexed and Internal Categories

Note that in the diagram expressing the associativity of composition there is an implicit isomorphism

between c1´0 (c1´0 c1) and (c1´0 c1) ´0 c1. Indeed,

COMP » (COMP ´0 id) : (c1 ´0 c1) ´0 c1 ® c1

COMP » (id ´0 COMP) : c1 ´0 (c1 ´0 c1) ® c1.

In the following, this isomorphism will be always skipped in order to maintain the notation at a

simpler level.

7.2.2 Examples 1. Given an object e in E, the internal discrete category associated with e

is (e,e,ide,ide,ide,ide).

2. Let E be a CCC with all finite limits, and let A be an object of E. It is possible to define

internally to E a category that plays the role of the category of retractions over A.

Let m = L( eval » (id´eval) ) : AA ´A A ®A A the internal composition map, that is let m

=l(f,g).g » f. Since E has all finite limits, it has equalizers for every pair of morphisms. Let then

(X, x) be the equalizer of

id : AA ® AA

m » <id,id> : AA ®AA

The function m » <id,id> : AA ®AA is lf. f » f; thus the object X represents the subset of AA of

all those functions f such that f = f » f , i.e., X is an internalization for the set of retractions in AA.

X plays the role of c0 in the internal category we are defining.

Intuitively, a morphism between two retractions g and h is a triple (f,g,h), where f is a

function from A to A such that f = h » f » g.

In order to internalize this definition we use the equalizer (Y,y) of

p1 : AA´X´X ® AA

m » (m´id) » < x » p3 , p1, x » p2 > : AA´X´X ® AA

Note that m » (m´id) » < x » p3 , p1, x » p2 > is just lfgh. x(h) » f » x(g).

138

7. Indexed and Internal Categories

COD and DOM are obviously defined by the following equations:

DOM = p2 » y

COD = p3 » y

For ID, note first that by definition of x , m » < x, x > = id » x = x and, therefore,

(lfgh. x(h) » f » x(g) ) » < x, id, id > = x.

Thus < x, id, id >: X ®AA´X´X equalizes p1 and lfgh. x(h) » f » x(g), and ID: X ®Y is the

unique arrow such that y » ID = < x, id, id >. Note that

DOM » ID = p2 » y » ID = p2 » < x, id, id > = id

COD » ID = p3 » y » ID = p3 » < x, id, id > = id.

Finally, we must define COMP: Y´0Y®Y. The idea is that (f,g,h) » (f',k,g) = ( f » f', k, h ). We

start defining an arrow M: Y´0Y® AA´X´X such that M((f,g,h), (f',k,g)) = ( f » f', k, h ); next

we prove that M equalizes p1 and lfgh. x(h) » f » x(g). Then COMP is the unique arrow from

Y´0Y to Y such that y » COMP = M.

3. Given a function f: U®C, consider the C-indexed collection of sets {G(c) = f-1(c)}cÎC. We can

form a small category C , which has C as set of objects, and with hom-sets C [c,c'] =

Set[G(c),G(c')]. Composition and identities are inherited from Set. The previous construction can

be generalized to a generic topos E: given f: U®C in E, there is an internal category Full(f) that

plays the role of the full subcategory generated by the fibers of f. Full(f)0 is C; Full(f)1, together

with the map <DOM,COD>: Full(f)1®C´C, is defined as the exponent p1*(f)p2*(f) in the slice

category E/C´C, where

p1*(f) = f´id: U´C®C´C

p2*(f) = id´f: C´U®C´C

are respectively the pullbaks of f along the first and second projections. Composition is obtained from

the internal composition map m: p2*(f)p1*(f)´p3*(f)p2*(f)®p3*(f)p1*(f) in the slice category

E/C´C´C. Similarly, the identity morphism ID: C®Full(f)1 is obtained from the ’inclusion of

identities“ L(idf): idC®ff in the slice category E/C.

Our exposition of Internal Category Theory proceeds with the definition of ’internal functor.“ Again,

the intuition of a standard functor helps in the understanding of the following definition; a functor F

between two small categories C and D is a pair of functions in Set, F = (F0 , F1 ), where F0 :

Ob C ®Ob D , F1 : MorC ®Mor D ; moreover F1 distributes with respect to composition and

preserves identity.

7.2.3 Definition Let c,dÎCat(E). F is an internal functor from c to d (F: c®d) iff F =

(f0, f1) with f0ÎE[c0,d0], f1ÎE[c1, d1], and F satisfies

139

7. Indexed and Internal Categories

7.2.4 Definition The category Cat(E) has as objects the internal categories of E and as

morphisms the internal functors. Composition of functors is defined in the obvious way; that is,

given F = (f0,f1) and G = (g0,g1), F » G = (f0 » g0, f1 » g1).

For example, Cat(Set) is the category Cat of all small categories, i.e., of all those categories

whose class of morphisms is a set.

It is easy to carry out the usual constructions on categories inside Cat(E). For example, given c

= (c0, c1, DOM, COD, COMP, ID), we can define the dual category cop = (c0, c1, COD, DOM,

COMP » a, ID), where a = <P 2 ,P 1 > 0 : c 1 ´ 0 c 1 « c 1 ´ 0 'c 1 . _op : Cat(E) ® Cat(E) is a

functor.

The product of two internal categories c and d is the category c´d = (c0 ´d 0 , c1 ´d 1 ,

DOM c´DOM d, CODc´COD d, (COMPc´COMP d) » b, IDc´IDd) where b is the isomorphism

(c 1 ´ 0 c 1 )´(d 1 ´ 0 d 1 ) « (c1 ´d 1 )´ 0 (c 1 ´d 1 ). Clearly, _´_ : Cat(E)´Cat(E) ® Cat(E) is a

functor.

7.2.5 Definition Let F = (f0,f1) and G = (g0,g1) be two internal functors from c to d. t is

an internal natural transformation from F to G (t: F®G) iff tÎE[c0, d1] and satisfies

140

7. Indexed and Internal Categories

7.2.6 Definition Given two internal categories c and d, Nat(c,d) is the category that has

internal functors from c to d as objects, and internal natural transformations as arrows. Given s:

F ® G and t: G®H, t » s = COMPd » <t,s>0 : F ® H

7.2.7 Example In this example we define PER as an internal category of w-Set. PER is the

category of partial equivalence relations constructed over Kleene•s applicative structure (w,.).

Remember that the partial application . : w´w®w is defined by m.n = jm(n), where j: w®PR is

an acceptable gšdel numbering of the partial recursive functions. We will use the following notation:

n A m iff n is related to m by A ,

{n}A = {m | m A n } the equivalence class of n with respect to A,

Q(A) = {{n}A | n Î dom(A)} where dom(A) = {n/ nAn} .

The morphisms of the category 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“ in the sense that they are fully described by partial

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

Note that PER is a small category, as the partial equivalence relations (p.e.r.•s) form a set as

well as their morphisms; thus Set contains PER as an internal category. Though, since a crucial

property of PER is that its morphisms are ’computable,“ we are interested in introducing a similar

notion in the category of sets by a realizability relation ’|_“ with respect to numbers.

The category w- Set is defined as follows:

objects: (A,|_)Îw - Set iff

w

A is a set and |_ Í w´A, such that "aÎA $n |_ a .

morphisms : fÎw - Set[A,B] iff

w

141

7. Indexed and Internal Categories

f : A®B and $n "aÎA "p |_A a n.p |_B f(a)

(notation : n |_A®B f and we say that n realizes f ).

Similarly as for PER, each morphism in w - Set is ’computed“ by a partial recursive function,

which is total on { p | p |_Aa } for each aÎA .

It is not difficult to prove that w - Set is a CCC with all finite limits. The terminal object is

simply (1, |_ 1 ) , where 1 is the singleton set and |_ 1 = w´1. If [ , ] is a coding of pairs of

numbers, then (A´B, |_A´B ) is given by [n,m] |_A´B (a,b) iff n |_A a and m |_B b . As for

exponents, let [A®B] = ({f: A ® B | fÎw -Set [A,B] }, |_ A®B ), where |_ A®B is given as

w

above.

There is a simple way to embed Set into w -Set. Let S : Set®w -Set be given by

w

S(S) = (S, |_S) with |_S = w´S , the ’full“ relation.

S is defined as the identity on morphisms, since by the definition of |_S , all functions are realized

by all numbers for total recursive functions. S is a full and faithful functor, which preserves all finite

limits and exponents.

This embedding suggests how to turn PER into an internal category of w -Set (recall that the

exponent of A and B in PER is given by m (A®B) n Û "p,q (p A q Þ m .p B n.q) ).

Indeed, M = (Mo,M1,domM,codM,idM,compM) is defined by

1. Mo = (PER, |_M) where |_M = w´ PER;

2. M1 = ({<{n}A®B,A,B)> | A,BÎM, n (A®B) n }, |_1)

where m |_1 < {n}A®B,A,B> iff m (A®B) n ;

3. domM(<{n}A®B,A,B)>) = A;

4. codM(<{n}A®B,A,B)>) = B;

5. idM(A) = <{i}A®A,A,A)> where i = lx.x is a number for the identity function;

6. compM(<{n}A®B,A,B)>,<{m}B®C,B,C>) = <{b.m.n}A®C,A,C)>

where b = lxyz.x(yz).

We have to check that M is an internal category of w-Set. It will be easy, in view of the set-theoretic

nature of its morphisms. Essentially, one has to prove that the required morphisms are functions that

happen to be realized.

Note first that w -Set[A,S(S)] = Set[A,S] for any A = (A, |_A) in w -Set and any set S, since

|_S is the full relation and, hence, any function is realized by any index. Thus, the set-theoretic

functions domM, codM are also morphisms in w -Set.

M1 is a set of triples: equivalence class, domain, and codomain. The realizability relation in M1

is nontrivial and, hence, one needs to give explicitly the realizers of idM and compM. Indeed, idM

is realized by lx.i, the constant function equal to an index i for the identity function. As for

compM , it is defined as usual only on a subset of M 1´M 1, namely, where the target of the first

morphism coincides with the source of the second. In the general setting, this is expressed by the use

142

7. Indexed and Internal Categories

of a pullback as a source object for COMP. In this specific case, that pullback becomes simply the

set of pairs such as (<{n}A®B,A,B)>,<{m}B®C,B,C>). Then the realizer for compM is b', for

b'[n,m] = bnm, where b is an index for the composition of functions, an operation that may be

uniformly and effectively given over (w,.) .

7.3 Internal Presheaves

We have already remarked that every small category may be regarded as an internal category in Set.

However, in Set we are accustomed to considering not only functors from one small category to

another, but also, for example, functors from a small category to a large one and in particular to Set

itself. A significant example is hom-functor from a small category to Set. Surprisingly, it is possible

to cope at the internal level also with this problem, by means of the notion of internal presheaf.

If F is a functor from Cop to Set, then the component FOb of F is a collection {F(c)} of sets

indexed on objects of C. Such a collection can be regarded as a function r0: X®ObC, where X =

{(c,m)/ mÎF(c)} and r0(c,m) = c. Then FOb(c) @ r0-1(c). Now, given an arrow f: d®c, and

an object (c,m)Îr0-1(c), define a function r1 by r1((c,m),f) = (d,F(f)(m)). The function r1

describes the behavior of F on morphisms. Note that r1((c,m),f) is defined if and only if cod(f) =

r0(c,m) = c; thus, the domain of r1 is the pullback Z (in Set) of cod: MorC®ObC and r0:

X®ObC. Let P2: Z®MorC and P1: Z®X, be the associated projections. Note that

1. r0( r1((c,m), f) ) = r0( (d,F(f)(m)) ) = d = dom(f) = dom( P2(f,(c,m)) ) ;

2. r1((c,m),f°f') = (d,F(f°f')(m)) = (d,F(f')(F(f)(m))) = r1((d',F(f)(m)),f') =

= r1(r1(f,(c,m)),f');

3. r1((c,m), idc) = (c,F(idc)(m)) = (c, m).

That is, more concisely:

i. r0 ° r1 = dom ° P2 : Z®ObC;

ii. r1 ° (idX ´0 comp) = r1 ° ( r1 ´0 idMorC) : X´0MorC´0MorC ® MorC;

iii. r1 ° <idX, ID ° r0>0 = idX,

where ´0 denotes pullback product and ID: ObC®MorC is the function that takes an object c to

idc. Conversely, given a small category C, and a triple (X, r0: X®ObC, r1: X´0ObC®MorC )

that satisfies equations i-iii above, it is possible to define a presheaf F: Cop®Set by letting

F(c) = r0-1(c)

"cÎObC

F(f)(c,m) = r1((c,m),f).

"fÎC[c',c], "(c,m)ÎF(c)

Equation i states that r 1 ((c,m),f) is in F(c'), indeed c' = dom(f) = dom(P 2 ((c,m),f)) =

r0(r1((c,m),f)), and thus, by definition of F, F(f)(c,m)=r1((c,m),f)ÎF(c').

Equations ii and iii express the fact that F is a contravariant functor. Indeed,

F(f»g)(c,m) = r1((c,m),comp(f,g)) by def. of F

= r1( r1((c,m),f), g) by (ii)

143

7. Indexed and Internal Categories

= F(g)( r1((c,m),f)) by def. of F

= F(g)(F(f)((c,m))) by def. of F

and

F(idc)(c,m) = r1((c,m), idc) by def. of F

= (c,m) by (iii)

7.3.1 Definition X is an internal presheaf on cÎCat(E) iff X = (X, r 0 , r 1 ) with,

r0: X®c0

r1: X´0c1®X where X´0c1 is the pullback of r0: X®c0 and COD: c1®c0,

and X satisfies the following:

Example Let cÎCat(E), and e an object of E. The constant-e diagram is the internal presheaves

(e´c0, snd: e´c0®c0, ide´DOM: e´c1®e´c0). Note that e´c1 is the pullback of snd: e´c0®c0

and COD: c1®c0. Moreover, the previous morphism satisfies the requested conditions of definition

7.3.1, since

i. snd ° ide´DOM = DOM ° snd : e´c1®c0 ;

ii. ide´DOM ° (ide´COMP) =

= ide´(DOM ° COMP)

= ide´(DOM ° P2)

144

7. Indexed and Internal Categories

= ide´DOM ° ( ide´P2)

= ide´DOM ° ( ide´DOM ´0 id) : e´c1´0c1®e´c0 ;

iii. ide´DOM ° (ide´ID) = ide´c0 : e´c0®e´c0 .

The intuition behind the previous definition is that of a collection, indexed by c, of objects e.

Indeed, consider the case of an internal category C in Set (i.e., a small category) and let E be a set.

By applying the above ’externalization,“ we obtain

F(c) = r0-1(c) = E´{c}

"cÎObC

"fÎC[c',c], "(e,c)ÎF(c) F(f)(e,c) = r1((e,c),f) = (e,DOM(f)) = (e,c') .

Another major example of a presheaf is given by the hom-functor.

7.3.2 Definition Let cÎCat(E). The internal hom-functor homc is the presheaf (c1 , r 0 ,

r1) on c´cop, where

r0 = <DOM,COD> : c1®c0´c0

r1 = COMP » < p2 » P1, COMP » (id ´0 p1) >0 : c1´0(c1´c1)®c1

(Informally, r1 = lfgh. h » f » g ), and

7.3.3 Definition Let X = (X, r 0 ,r 1 ), Y = (Y, s 0 ,s 1 ) be two presheaves on cÎCat(E). h is

a morphism of presheaves from X to Y ( h : X® Y) iff hÎE[X,Y] and the following

diagrams commute:

The following definition allows to compose an internal presheaf on c with an internal functor F:

d®c, yielding a new presheaf on d.

7.3.4 Definition Let X = (X, r 0 , r 1 ) be an internal presheaf on cÎCat(E), and F: d®c be an

internal functor. The pullback of X along F is the presheaf F*(X) = (Y, s0, s1) on d defined

by the following commutative diagrams, where the squares are pullbacks:

145

7. Indexed and Internal Categories

Suppose that the internal presheaf X ’internalizes“ the functor G: Cop®Set (and F: d®c is an

’internalization“ for F: D®C). Then, G(F(a)) = {xÎX | r 0(x)=f0(a)} = {yÎY | s 0(y)=a} by

definition of the pullback for Y, and, if h: a®b, one has G(F(h)) = lxÎF(b).r 1 (x,f1 (h)) =

lxÎF(b).s1(x,h) by definition of s1.

All the definitions given so far were directed towards the following crucial notion, which will enable

us to define the concept of internal Cartesian closed category.

7.3.5 Definition < F, G, f > : c® d is an internal adjunction from c to d iff F is an

internal functor from c to d, G is an internal functor from d to c and

f : (F´Iddop)*(homd) ® (Idc´Gop)*(homc)

is an isomorphism between presheaves on c´dop.

The definition of adjunction in 7.3.5 is now easily generalized to the case with parameters.

7.3.6 Definition < F, G, f > : c® d is an internal adjunction from c to d w i t h

parameters in a iff F is an internal functor from c´a in d, G is an internal functor from aop´d

in c and

f : (F´Iddop)*(homd) ® (Idc´Gop)*(homc)

is an isomorphism between presheaves on c´a´dop.

146

7. Indexed and Internal Categories

We can also give an ’equational“ characterization of internal adjunctions, in the spirit of theorem

5.3.5.

7.3.7 Theorem Every internal adjunction < F, G, f > : c ® d is fully determined by the

following data in (i) or (ii):

i. - the functor G: d®c

- an arrow f0: c0®d0

- an arrow Unit: c0®c1 such that DOM » Unit = id , COD » Unit = g0 » f0

- an arrow f-1: Y®X, where X and Y are respectively the pullbacks of

<DOM,COD> : d1®d0´d0 , f0´id: c0´d0®d0´d0

<DOM,COD> : c1®c0´c0 , id´g0: c0´d0®c0´c0

and, moreover, the previous functions satisfy the following equations:

a. < r0, COMP » < g1 » PX, Unit » p1» r0 >0 >0 » f-1= idY

b. f-1» < r0, COMP » < g1 » PX, Unit » p1» r0 >0 >0 = idX

ii. - the functor F: c®d,

- an arrow g0: d0®c0,

- an arrow Counit: d0®d1 such that DOM » Counit = f0 » g0 , COD » Counit = id

- an arrow f: X®Y, where X and Y are respectively the pullbacks of

<DOM,COD> : d1®d0´d0 , f0´id : c0´d0®d0´d0

<DOM,COD> : c1®c0´c0 , id´g0 : c0´d0®c0´c0

and moreover the previous functions satisfy the following equations:

a. < r0', COMP » < Counit » p2» r0', f1 » PY>0 >0 » f = idX

b. f » < r0', COMP » < Counit » p2» r0', f1 » PY>0 >0 = idY

Proof See the appendix to this chapter.

We are finally ready to define internal Cartesian closed categories.

7.3.8 Definition An internal Cartesian closed category is a category cÎCat(E) with three

adjunctions, the third one with parameter in c:

1. < O, T, 0 > : c®1 , where 1 is the internal terminal category.

2. < D, x, <,> > : c®c´c , where D is the internal diagonal functor.

3. < x, [,] , L > : c®c , where this adjunction has parameters in c.

7.3.9 Examples 1. In example 2 in 7.2.2, we defined the internal category Ret A ÎCat(E) of

retractions on a generic object A of E, where E is a CCC with all finite limits. We now prove that if A

is a reflexive object, that is, if AA < A, then RetA is Cartesian closed.

147

7. Indexed and Internal Categories

Let AA < A via (in,out). By theorem 2.3.6 we know that t < A and A´A < A. Call these

retractions (in',out') and (in",out"), respectively.

Let us begin with the internal terminal object in RetA. The idea is that every constant function is

a terminal object in a category of retractions. Since t < A via (in',out'), in': t ® A is a point of A

and, thus, we can take in'» out': A®A as the constant function we are looking for; moreover, c =

L(in'» out'» p2) : t ® AA is the point in AA that represent it. Then the internal terminal object t0: t

® X is defined by the following:

We leave it to the reader to check the soundness of the previous definition, as well as the definition of

internal products, and we move on to exponents.

The first notion we must define is the arrow [,] 0 : X´X®X. The idea is that, given two

retractions f, g, their exponent is the retraction [f,g]0=la.in(x(g)»out(a)»x(f)). Let

H = l(f,g)la. in( x(g)»out(a)»x(f) ) : (X´X)´A®A .

Then [,]0: X´X®X is formally defined by the following diagram:

The function EVAL: X´X®Y is the internal Counit of the adjunction; it takes two retractions f

and g, and gives a morphism EVALf,g from the retraction [f,g]0x0f to the retraction g (where

x0 is the internal product on objects). More specifically, if

E = l(f,g)la:[f,g]0x0f. out(FST(a))(SND(a)): X´X´A®A

(where la:h.M is shorthand for la.[h(a)/a]M, and FST, SND are the internal projections)

E1 = L(E): X´X®AA

E 2 = x 0»<[,]0 ,p1 >: X´X®X.

Then EVAL: X´X®Y is defined by the following commutative diagram:

148

7. Indexed and Internal Categories

We must now define L: U ® W, where U and W are the pullbacks in the following diagram:

Informally L works on tuples of the kind (f,g,h, (r, fx0g, h)) where f,g,h are retractions and r

is a morphism from fx0g to h, that is r: A®A such that r = h » r » fx0g.

Now, let Curry(r) = ly.in( lz.(r » in")(z,y)): A®A. Then Curry(r) is a morphism from g to

[f,h]0: indeed, by omitting for simplicity the function x: X®AA, we have

[f,h]0 » ly.in( lz.(r » in")(z,y)) » g =

= la.in( h » out(a) » f ) » ly.in( lz.(r » in")(z,g(y)) )

= ly.in( h » lz.(r » in")(z,g(y)) » f )

= ly.in( lz.( h » r » in")(f(z),g(y)) )

= ly.in( lz.(h » r » fx0g » in")(z,y) )

= ly.in( lz.(r » in")(z,y) )

Let Curry = lr.ly.in( lz.(r » in")(z,y)): AA ®AA.

Then F = < Curry » p1 » y » PU, id´[,]0 » s > : U®AA´X´X .

But we have already verified that

p1 » F = ( lfgh. x(h) » f » x(g) ) » F

and, thus, there exists a unique morphism F: U®Y such that F = y » F.

Finally L = <s, F>0 : U ® W.

2. This example continues example 7.2.7, where we defined PER as an internal category of the

category w -Set. We still need to check that the internal category PER of w -Set is an internal CCC.

In general, observe that in order to ’internalize“ a categorical construction, as we did for the category

149

7. Indexed and Internal Categories

of retractions, say, one has to turn implicit set-theoretic functional dependencies into morphisms of

the intended global category E. For example, consider the map L that gives the internal natural

isomorphism for Cartesian closure. Externally, L is implicitly indexed by objects a, b, for

instance, and the map a,b |_ L a,b is simply a function in Set. The internal version, requires only

that the map L, depending also on a and b, is a morphism in E.

The result, that M is an internal CCC of w -Set, then follows by the uniformity and effectiveness

of the argument for the Cartesian closure of PER. Namely, one only has to observe that evalA,B is

realized by any index e of the partial recursive universal function (and hence we could set eA,B = e

in the example). Thus, not only evalA,B is realized, but the construction is internal to w -Set as it

depends on A,B by a constant function (or e is independent of A, B). Thuis is also the case for

L A,B , since it is uniformly realized by any index of the function s of the s-m-n iteration theorem,

independently of A, B.

7.4 Externalization

In this section, we define the process of externalization of an internal category via hom-functors that

correspond, essentially, to the Yoneda embedding. Since for any object e of E the hom functor

[e,_]: E®Set preserves pullbacks, it transforms an internal category c = (c0, c1, DOM, COD,

COMP, ID)ÎCat(E) into a small category [e,c] = ([e,c0], [e,c1], [e,DOM], [e,COD], [e,COMP],

[e,ID]).

More generally, if cÎCat(E), then [_,c]ÎCat(Eop®Set), and, for the uniform behavior with

respect to the indexes in E, [_,c] can be also regarded as an E-indexed category, that is, a functor

Eop®Cat. In the next section we show that, conversely, every E-indexed category can be regarded

as an internal category in Eop®Set.

7.4.1 Definition Let c = (c0 , c1 , DOM, COD, COMP, ID) Î Cat(E), then [e,c] = ([e,c0 ],

[e,c1], [e,DOM], [e,COD], [e,COMP], [e,ID]).

The objects of [e,c] are the arrows sÎ E[e, c0]. Given two objects s, t, a morphism f: s®t

in [e,c] is an arrow fÎE[e, c1] such that DOM » f = s, COD » f = t . The identity of s is ids =

ID » s. Let c2 be the object of composable maps of c, that is the pullback c1´0c1 of COD and

DOM. Since the hom-functor [e,_]: E®Set preserves pullbacks, [e,c2 ] is the pullback of

[e,COD] and [e,DOM], and [e,COMP]: [e,c2]®[e,c1] has the expected type. Given two arrows

f: s®t, g: t®g in [e,c], their composition by [e,COMP] is g o f = COMP » <g,f>0. In case the

ambient category E has small hom-sets, the category [e,c] is obviously small.

Note that, if c,dÎCat(E), then [e,c´d] @ [e,c]´[e,d] and [e,cop] @ [e,c]op.

150

7. Indexed and Internal Categories

In the previous definition, e can be regarded as a parameter, yielding a functor [_,c] :

Eop®Cat, that is, an E-indexed category.

7.4.2 Definition Let cÎCat(E). The functor [_,c] : Eop®Cat is defined in the following way:

on objects eÎE [_,c] = [e,c]

on arrows s: e'®e [_,c](s) = [s,c] is the functor from [e,c] in [e',c] that is defined as

[s,c0] on objects and as [s,c1] on arrows.

More explicitly, the functor [s,c] takes every tÎ[e,c] (i.e., t: e®c0) to t » s, and every g: t®t'

to g » s.

We have to prove as follows that the previous definition makes sense:

1. "s: e'®e, [s,c]: [e,c] ® [e',c] is a functor, for

1.1. "t: e®c0 [s,c](idt ) = [s,c](ID » t ) = ID » t » s = idt o s

1.2. "f: d®g , "g: r®d in [e,c]

[s,c](f o g) = COMP » < f, g > » s = COMP » < f » s, g » s > = [s,c](f) o [s,c](g)

2. [_,c] : Eop ® Cat is a functor, for

2.1. "e [_,c] (ide) = I : [e,c] ® [e,c] (immediate by definition of [_,c] )

2.2. "s: e®e' , "t: e'®e", [_,c](t » s) = [_,c](s) » [_,c](t ) : [e,c] ® [e",c]; indeed,

2.2.1. on objects gÎ[e,c]: [_,c](t » s)(g) = g » t » s = [_,c](s)([_,c](t )(g))

2.2.1. on arrows g t®t' in [_,c]: [_,c](t » s)(g) = g » t » s = [_,c](s)([_,c](t )(g))

Note that if c = (c0, c1, DOM, COD, COMP, ID) is an internal category in E, then ([_,c0], [_,c1],

[_,DOM], [_,COD], [_,COMP], [_,ID]) is an internal category in Eop®Set.

Definitions 7.4.3 and 7.4.4 show how to externalize, respectively, an internal functor, an internal

natural transformation, and an internal presheaf. Again these definitions, as well as others in the

sequel, are parametric with respect to the object e of E .

7.4.3 Definition Let c,dÎCat(E), F = (f0 ,f1 ): c®d be an internal functor, and let e be an

object of E. The functor [e,F]: [e,c]® [e,d] is defined as [e,f0] on objects, and as [e,f1] on

arrows.

That is, the functor [e,F]: [e,c] ® [e,d] takes every object s in [e,c] to f0 » s in [e,d], and

every arrow g: s®t in [e,c] to f1» g: (f0 » s)®(f0 » t) in [e,d].

151

7. Indexed and Internal Categories

7.4.4 Definition Let c,dÎCat(E) and let F = (f0 ,f1 ): c®d be an internal functor. The E-

indexed functor [_,F]: [_,c]®[_,d] is the natural transformation defined by [_,F](e) = [e,F], for

every object e of E.

We must prove the naturality in e of the previous definition; that is, for any s: e'®e,

[e',F] » [s,c] = [s,d] » [e,F] .

We have, for any object t of [e,c] (i.e, t: e®c0),

[e,F][s,c](t) = [e',F](t » s) by def. of [s,c]

= f0 » t » s by def. of [e',F]

= [s,d] » f0 » t by def. of [s,d]

= [s,d] » [e,F] by def. of [e,F].

7.4.5 Definition Let t: F®G be an internal natural transformation, where F,G: c®d. The

natural transformation [e,t]: [e,F]® [e,G] is defined as the homonimous function [e,t]:

[e,c0]®[e,d1]; that is, it takes every object s of [e,c] to [e,t](s) = t » s : (f0 » s)®(g0 » s)

(where the last ’typing“ is in [e,c]).

Exercise Prove that the previous definition makes sense, that is:

1. [e,t](s) : [e,F](s) ® [e,G](s)

2. for every h: s®g in [e,c], [e,G](h) o[e,t](s) = [e,t](g) o[e,F](h).

7.4.6 Definition Let t: F®G be an internal natural transformation, where F,G: c®d. The E-

indexed natural transformation [_,t]: [_,F]®[_,G] is defined by the following: for any object e of E,

[e,t]: [e,F]®[e,G].

Now we will show how to externalize the notion of morphism of presheaves.

7.4.7 Definition Let X=(X, r 0 , r 1 ) be an internal presheaf on cÎCat(E). The functor [e,X]:

[e,c]op®Set is defined by:

[e,X](s) = { fÎE[e,X] / r0 » f = s }

"sÎ[e,c] ,

"g: t®s in [e,c], [e,X](g) : [e,X](s)®[e,X](t) is given by:

"fÎ[e,X](s) [e,X](g)(f) = r1» <f, g>0 Î[e,X](t)

(note that r0 » [e,X](g) (f) = r0 » r1» <f,g>0 = DOM » P2» <f,g>0 = DOM » g = t )

We have chosen the name [e,X] as an analogy for the previous constructions, but in this case it

no longer has a direct relation with the Yoneda embedding. The same holds below for the

externalization [e,h] of a morphism of presheaves h.

152

7. Indexed and Internal Categories

Next we check that by externalizing an internal homc on c´cop we just obtain the hom-functor

from [e,c]op´[e,c] to Set.

7.4.8 Proposition Let cÎCat(E) and let homc = (c1, r 0, r 1) be the internal hom-functor on

c´cop. Then, for every eÎObE, [e,homc] = hom[e,c]: [e,c]op´[e,c]®Set (to within the implicit

isomorphism [e,c]op´[e,c] @ [e,cop´c] ).

Proof

- on objects: let <s,t>: e ® c0´c0

[e,homc](<s,t>) = {f: e®c1 / r0 » f = <s,t> }

= {f: e®c1 / <DOM,COD> » f = <s,t> }

= hom[e,c](s,t);

- on morphisms: let <f,g> : <s,t>® <g,d> in [e,cop´c]. "hÎ[e,homc](<g,d>), i.e., for all

h: e®c1 such that <DOM,COD> » h = <g,d>, we have

[e,homc](<f,g>)(h) = r1 » <h, <f,g>>0

= COMP » < p2 » P2, COMP » (id ´0 p1) >0 » <h, <f,g>>0

= COMP » < g, COMP » <h, f>0 >0

= gohof. ¨

The next definition finally externalizes the notion of morphism of presheaf that simply becomes a

natural transformation. Proposition 7.4.10 states that the composition of an internal functor with a

morphism of presheaf, given by the pulling back construction of definition 7.3.3, externalizes to the

composition of the two associated external functors.

7.4.9 Definition Let h be a morphism of presheaves from X = (X, r 0 ,r 1 ) to Y = (Y,

s0,s1), where X an Y are internal presheaves on c. The natural transformation [e,h]: [e,X]®[e,Y]

(where [e,X], [e,Y]: [e,c]op ®Set ) is defined in the following way: "gÎ[e,c], "fÎ[e,X](g),

[e,h](g)(f) = h » f (note that [e,h](g)(f) Î[e,Y](g), since s0 » h » f = r0 » f = g ).

[e,h] is indeed a natural transformation, since, "g: t®g in [e,c], "fÎ[e,X](g)

[e,Y](g) ([e,h](g)(f) ) = [e,Y](g) (h » f) by def. of [e,h]

= s1 » <h » f, g>0 by def. of [e,Y](g)

= s1 » h´0id » <f, g>0

= h » r1 » <f, g>0 by the ’naturality“ of h

= h » ([e,X](g)(f) ) by def. of [e,X](g)

= [e,h](t) ([e,X](g)(f) ) by def. of [e,h]

153

7. Indexed and Internal Categories

7.4.10 Proposition Let F: d®c be an internal functor, X = (X, r 0, r 1) an internal presheaf

on c, and F* (X) = (Y, s 0 , s 1 ). For every object e of E, the functors [e,F* (X)] and

[e,X]»[e,F]op: [e,d]op®Set are naturally isomorphic. The isomorphism is

ht = lg. PX » g : [e,F*(X)](t) ® [e,X]([e,F]op(t))

ht-1 = lh.<t, h>0 : [e,X]([e,F]op(t)) ® [e,F*(X)](t)

Proof Let us check first that ht and ht-1 have the correct types.

By definition [e,F*(X)](t) = {gÎE[e,Y] / s0 » g = t }. Let gÎ[e,F*(X)](t). Then the following

diagram commutes:

Thus PX » g Î [e,X](f0 » t) = [e,X]([e,F]op(t))

Conversely, let hÎ[e,X]([e,F]op(t)). Then the arrow <t, h>0: e®Y is well defined, because r0

» h = f0 » t . By definition of s0, s0 » <t, h>0 = t which implies <t, h>0Î[e,F*(X)](t).

We now prove the naturality of ht and ht-1. Let k: g®t in [e,d]op; for every gÎ[e,F*(X)](t)

[e,X]([e,F]op(k))(ht(g)) = [e,X]( f1 » k ) (PX » g) by def. of [e,F]op

= r1» <PX » g, f1 » k >0 by def. of [e,X]

= r1» PX´0f1 » < g, k >0

= PX » s1 » < g, k >0 by def. of r1

= PX » ([e,F*(X)](k) (g) ) by def. of [e,F*(X)]

= hg( [e,F*(X)](k) (g) ) by def. of h

Conversely, for every k: g®t in [e,d]op and every hÎ[e,X]([e,F]op(t)):

[e,F*(X)](k) ( ht-1(h) ) = s1 » < ht-1(h) , k >0 = s1 » < <t, h >0 , k >0

Thus: PX » ([e,F*(X)](k) ( ht-1(h) ) ) = PX » s1 » < <t, h >0 , k >0

= PX » s1 » < <t, h >0 , k >0

= r1» PX´0f1» < <t, h >0 , k >0

= r1» < PX » <t, h >0, f1» k >0

= r1» < h, f1 » k >0

s0 » ([e,F*(X)](k) ( ht-1(h) ) ) = s0 » s1 » < <t, h >0 , k >0

and

= DOM » P2 » < <t, h >0 , k >0

= DOM » k

=g

And since f = <s0 » f, PX » f >, then for every f : e®Y,

154

7. Indexed and Internal Categories

[e,F*(X)](k) ( ht-1(h) ) = <g, r1» < h, f1 » k >0 >0

= <g, [e,X]([e,F]op(k)) (h) >0

= hg-1( [e,X]([e,F]op(k)) (h) ). ¨

7.4.11 Proposition Let < F, G, f > : c®d be an internal adjunction. For every e in E, define

Qe = h'» [e,f] » h-1, where

h : [e,(F´Iddop)*(homd)] ® [e, homd] » [e,Fop´Id]

h': [e,(Idc´Gop)*(homc)] ® [e, homc] » [e,Id´Gop]

are the isomorphisms of proposition 7.4.10 .

Then <[_,F], [_,G], Q > : [_,c]®[_,d] is an E-indexed adjunction.

Proof For every object e of E, we have

hom[e,d][[e,F](_), _ ] = [e, homd] » [e,Fop´Id]

@ [e,(F´Iddop)*(homd)] via h-1

@ [e,(Idc´Gop)*(homc)] via [e,f]

@ [e, homc] » [e,Id´Gop] via h'

= hom[e,c][_, Ee,G(_) ].

Moreover, the previous adjunction is ’natural in e,“ that is,

"fÎE[e',e] Qe' » [_,d](f) = [_,c](f) » Qe .

More explicitly, we must check that, for every fÎE[e',e], s object of [e,c], t object of [e,d], and

g: (f0 » s)®t in [e,d], one has

Qe' <s » f, t » f> ([_,d](f) ) (g) = ([_,c](f) ) Qe<s,t> (g)

We have

Qe' <s » f, t » f> ([_,d](f) ) (g) = Qe' <s » f, t » f> (g » f ) by def. of [_,d]

= Qe' <s » f, t » f> (g » f )

= PX » f » <<s » f,t » f >, g » f >0 by def. of Qe'

= PX » f » <<s,t>, g >0 » f

= (Qe<s,t> (g) ) » f by def. of Qe

= ([_,c](f) ) Qe<s,t> (g) by def of [_,c]. ¨

7.4.12 Exercise Prove that if <F, G, f > : c®d is an internal adjunction, and Unit and Counit

are the arrows in theorem 7.3.7, than for every object s: e®d0 in [e,d], Unit » s, Counit » s are

respectively unit and counit for s in the associated external adjunction <[e,F], [e,G], Q e >:

[e,c]®[e,d].

155

7. Indexed and Internal Categories

7.5 Internalization

In this section we show how to translate (small) E-indexed notions to internal ones in the topos of

presheaves Eop®Set.

7.5.1 Definition Let A: Eop®Cat be an E-indexed category, where all the indexed categories

are small. The internal category A = (A0, A1, DOM, COD, COMP, ID)ÎCat(Eop®Set) is defined

as follows: for all objects e, e' and arrows f: e'®e in E,

- A0: Eop®Set is the functor defined by

A0(e) = ObA(e)

A0(f) = A(f)ob : ObA(e)®ObA(e')

- A1: Eop®Set is the functor defined by

A1(e) = MorA(e)

A1(f) = A(f)mor : MorA(e)®MorA(e')

- DOM: A1®A0 is the natural transformation whose components are the domain maps in the

local categories, i.e., for eÎObE, DOMe: MorA(e)®ObA(e) is defined by DOMe(h:s®t)

= s.

- COD, ID and COMP are defined analogously, ’fiberwise“.

The claimed naturality for DOM, COD, ID, COMP is immediate, since A is a functor. For

instance, let fÎE[e',e] and hÎA(e)[s,t]; then DOM e'(A(f)mor(h)) = A(f)ob » DOM e(h). The

reader can check the other cases as an exercise.

7.5.2 Definition Let A, B be two E-indexed categories, and let H: A®B be an E-indexed

functor.The associated internal functor H = (H 0 ,H 1 ): A®B in Eop ®Set, is defined in the

following way:

- H0: A0®B0 is the natural transformation given by H0(e) = H(e)ob

- H1: A1®B1 is the natural transformation given by H1(e) = H(e)mor

The naturality of H0 and H1 is an immediate consequence of the ’naturality“ of H: A®B, that is

H(s) ° A(f) = B(f) ° H(s'). The equations in definition 7.2.3 easily follow from the fact that for every

e, H(e) is a functor.

7.5.3 Definition Let H: A®B, K: A®B be two E-indexed functors, and let t: H®K be an E-

indexed natural transformation. Then the associated internal natural transformation t: H®K in

Eop®Set is the natural transformation t: A0®B1 such that, for any e in E, and any a in A(e),

te(a) = t(e)a.

156

7. Indexed and Internal Categories

Recall that t: H®K consists of a natural transformation t(e): H(s)®K(e) for any object e of

E, such that, for any f: e®e' in E, and any object a in A(e'), t(e)A(f)(a) = B(f)(t(e')a) .

As a consequence, te(A0(f)(a)) = B1(f)(te'(a)), which gives the naturality of t .

7.5.4 Proposition Let A, B be E-indexed categories, H: A® B, K: B® A be E-indexed

functors, and <H, K, f> : A®B be an E-indexed adjunction. Then <H, K, f = f> : A®B is an

internal adjunction in Eop®Set .

Proof Exercise.

The picture is finally completed by the following result, which shows that by applying the

externalization process of section 7.4 to an internal category A, derived from an E-indexed category

A, we obtain an indexed category equivalent to A. However, when we externalize A, we do not

want a category indexed over all functors from E into Set. Since we are interested in a category

indexed over E, we must externalize only with respect to a full subcategory of Eop®Set equivalent

to E. The obvious choice is to consider the image Y(E) of E under the Yoneda embedding Y(e) =

E[_, e] (recall that Y(E) is a full subcategory of Eop®Set ). We will then obtain an indexed

category A# : Eop®Cat. Recall though that the ’internalization“ can take place only if the indexed

category takes small categories as values, while internal categoies do not need to live in small ambient

categories. Thus, the circle is closed by the following theorem, provided that the assumption is made

that E is small.

7.5.5 Theorem Let A: Eo p ® C a t be an E-indexed category, with E small, and let

AÎCat(Eop®Set) be its associated internal category. Then the indexed categories A# = [Y(_), A] :

Eop®Cat and A are equivalent.

Proof Let eÎObE. Then A#(e) = [Y(e), A] is, by definition, the category with

Objects: Nat[E[_,e], A0]

Morphisms: g: s®t in [Y(e), A] iff

gÎNat[E[_,e], A1] , DOM » g = s, COD » g = t

Now let fÎE[e',e]; by definition one has

A#(f) = [Y(f), A] : A#(e)® A#(e')

A#(f)(s) = s » Y(f) for sÎNat[E[_,e], A0]

A#(f)(g) = g » Y(f) for gÎNat[E[_,e], A1]

The natural isomorphism between A and A# is given by the Yoneda lemma: for every e in E, we

have natural isomorphisms Y0(e): Nat[E[_,e], A0]®A0(e) and Y1(e): Nat[E[_,e], A0]®A1(e).

Y 0 and Y 1 define the components on objects and morphisms of an indexed functor Y(e):

A#(e)®A(e). Explicitly,

Y(e)(s) = se(ide) for sÎNat[E[_,e], A0]

Y(e)(g) = ge(ide) for gÎNat[E[_,e], A1].

157

7. Indexed and Internal Categories

Then the due diagrams commute, by the usual Yoneda argument.

Our final result shows that, by following the other path (from internal to internal, via external),

one obtains equivalent categories:

7.5.6 Theorem Let cÎCat(E) be an internal category, C = [_,c]: Eop®Cat be as in definition

7.4.2, and Y: E®Y(E) be the Yoneda embedding. Then CÎCat(Y(E)).

Proof Let c = (c0, c1, DOM, COD, COMP, ID); note first that, by definition of C, for the internal

category C = (d0, d1, DOM', COD', COMP', ID')ÎCat(Eop®Set) we have

d0 = E[_, c0] = Y(c0)

d1 = E[_, c1] = Y(c1)

and hence CÎCat(Y(E)), since Y is full. That C is an internal category, follows by the fact that Y

preserves pullbacks. ¨

Appendix

We now study in more details the notions of internal adjunction and internal CCC. The details are

rather complex and this appendix may be skipped at first reading.