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