<<

. 5
( 10)



>>



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.

<<

. 5
( 10)



>>