Topological Functors II: the Cartesian-closed category of C-maps

A while back, I gave an introduction to topological functors, and I promised I would post one or more followups. So here we are. I will explain how the construction of the Cartesian-closed category of C-generated topological spaces due to M. Escardó, J. Lawson and A. Simpson [3] is really a construction that generalizes way beyond topological spaces, to all (well-fibered) topological constructs [2, Section 3]. I applied it to streams and prestreams in [2], but not everyone may be interested in the latter, while knowing that the idea of C-generation adapts to general topological functors is probably more interesting.

I will definitely not explain the whole construction. It turns out that this would be too much. I will concentrate on the core of the construction, which generalizes the first step of Escardó, Lawson and Simpson: the construction of a Cartesian-closed category MapC, built from a so-called strongly productive class C of objects of a category C, where C is the domain of a so-called well-fibered topological construct U. The Escardó-Lawson-Simpson construction is the special case where C is the category Top of topological spaces and U is the forgetful functor to Set.

(Update, May 15th, 2023: I have prepared a video on this subject, to be presented at the seminar on categorical topology at the University of Puebla, Mexico, see this page. The slides and the video(s) are at the bottom. This is probably better for an introduction to the topics on this page. But continue reading if you wish to understand the technical details, too.)

A refresher on topological functors

What you should keep in mind is that the paradigmatic example of a topological functor is the forgetful functor from the category Top of topological spaces to the category Set of sets. (I will call this the standard example.) The actual definition is more complicated: a functor U : CD is topological if and only if it is faithful, amnestic, and is such that every U-source has a U-initial lift.

Before I start, you may safely assume that D=Set. In any case, the construction I want to explain here eventually only works in that case. A topological functor U from a category C to Set is called a topological construct.

Alright. Being faithful is easy to explain. That just means that U is injective on hom sets, namely that if two morphisms f, g : XY in C (with the same domain and the same codomain) are such that U(f)=U(g), then f=g. In the standard example, any two continuous maps between the same spaces that are equal as ordinary functions between the underlying sets… are equal.

Given two objects X and Y of C, any morphism g from U(X) to U(Y) in D either lifts to a morphism ĝ from X to Y in C, meaning that U(ĝ)=g, or it does not. Since U is faithful, if the lift ĝ exists, it is unique. In the standard example, a set function g between two topological spaces has a lift if and only if it is continuous, and then ĝ is g itself, seen as a continuous map. Hence, and to avoid some pedantry, I will simply write the lift ĝ… as g. I will in fact avoid talking about lifts altogether, and I will simply say that g is a C-morphism from X to Y, instead of saying that g lifts to one. (And I am tempted to even say “C-continuous”, but maybe it is enough if you think of C as being some form of stand-in for Continuous.)

The condition “every U-source has a U-initial lift” means the following. A U-source is a family of morphisms gi : EU(Yi), iI, with common domain E. (Note that each C-object Yi is part of the datum, not just U(Yi). In the standard example, this means we are given topological spaces Yi, not just their underlying sets.) A lift of that U-source is a C-object X such that U(X)=E (in the standard example, X must be E with some topology) that turns every gi into a C-morphism from X to Yi.

This lift is U-initial if and only if, in a sense, X is the coarsest C-object such that U(X)=E and making every gi into a C-morphism. More formally, U-initiality means that for every C-object Z, an arbitrary D-morphism h : U(Z) → E is in fact a C-morphism from Z to X if and only if gi o h is a C-morphism from Z to Yi for every i in I.

Speaking of “C-objects X such that U(X)=E” is a bit awkward. It is traditional to talk about those C-objects as those being in the fiber of E. In the standard example, the fiber of a set E consists of those topological spaces whose points are those of E. Therefore, the fiber of E is really another way of talking about the collection of topologies on E (in the standard example).

Topologies are ordered by “coarser than” and “finer than”, and the categorical analogue is to say that given two C-objects X and Y in the fiber of the same D-object E, X is finer than Y (in notation, XY) if and only if the identity morphism from E to E is a C-morphism from X to Y. Naturally, Y is coarser than X if and only if X is finer than Y.

Then U is amnestic if and only if ≤ is antisymmetric on each fiber. In the standard example, this means that if a topology is both coarser and finer than another, then they are equal.

In the final paragraphs of part I, I had given a few examples of topological functors, including the forgetful functor from the category Pre of preordered sets to Set, as well as functors from categories of streams or prestreams to Top.

We will need a final property that not all topological functors have. A functor U : CD is well-fibered if and only if:

  • each fiber is small, namely for every D-object E, the collection of C-objects in the fiber of E is a set;
  • and it has discrete terminal objects, meaning that D has a terminal object 1 (the one element set in the standard example, or more generally if D=Set), and that there is exactly one object in its fiber (in the standard example, there is only one topology on a set with just one element).


I will follow the same path as in Section 5.6 of the book, or Section 3 of [2]. Not much of either, though! We will only imitate results of Section 5.6 of the book until and including Theorem 5.6.4, and Section 3 of [2] until and including Theorem 1.

In the sequel, U : CD will be a fixed topological functor, and C will be a class of objects of C. At some point, I will specialize this and require D to be Set, but this is not needed yet.

A C-probe is any C-morphism k : CX whose domain is an object C in C.

Let us define a Cmap from X to Y in C as any morphism g : U(X) → U(Y) in D such that g o k is a C-morphism for every C-probe k : CX with codomain X. That may seem to fail to type-check: I really mean that g o U(k), which is a D-morphism from U(C) to U(Y), should lift to a C-morphism from C to Y. But the formal definition is a bit heavy; in the standard example, that a set function g is a C-map means that g o k is continuous for every C-probe k with codomain X, and we don’t care about inserting U here and there. I will still try to mention U whenever that is not too heavy.

All C-morphisms are C-maps, or rather, every C-morphism g : XY induces a C-map U(g). Indeed, for every C-probe k : CX, g o k is a C-morphism, being the composition of two C-morphisms. Conversely, not all C-maps are C-morphisms, and that is the point.

There is a category MapC whose objects are those of C, and whose morphisms are the C-maps. This is a category that is a priori larger than C: although it has the same objects, it has more morphisms.

Products in MapC

An amazing thing about topological functors is that they preserve and reflect both limits and colimits. I have discussed that in the first post on the subject.

Hence, in particular, if D has all finite products, then C has all finite products, too; the product of finitely may objects X1, …, Xn in C is obtained by computing the product U(X1) × … × U(Xn) in D, and then taking the coarsest object X in the fiber of the latter that turns all the projections into C-morphisms. (In the standard example, this means giving the set U(X1) × … × U(Xn) the coarsest topology that makes all projections continuous, namely the product topology.)

I will simply write X1 × … × Xn for the resulting product in C.

Projections and pairings of C-morphisms are then computed in D, and are automatically C-morphisms. More precisely, if g1, …, gn are C-morphisms with the same domain in C, then their pairing ⟨g1, …, gn⟩ in C is obtained by computing the pairing ⟨U(g1), …, U(gn)⟩ in D, and realizing that this lifts to a unique C-morphism; we write it as ⟨g1, …, gn⟩, so that U(⟨g1, …, gn⟩) = ⟨U(g1), …, U(gn)⟩ and then it is easy to check that the equations defining products are satisfied, namely: πi o ⟨g1, …, gn⟩ = gi (1≤in), ⟨g1, …, gn⟩ o h = ⟨g1 o h, …, gn o h⟩, and ⟨π1, …, πn⟩ = id, where πi is projection onto the ith component.

In the sequel, I will drop mentions of U, as they tend to obscure the message, and therefore I will write ⟨g1, …, gn⟩ both for pairing in C and in D, and I will confuse any C-morphism g with the corresponding D-morphism U(g)—as in the standard example, where we take continuous maps and considering them as set functions without bothering to mention the conversion from the former to the latter. If you have any doubts about the correctness of the arguments, I refer you to [2, Section 3], where everything is done formally.

Lemma A. If D has all finite products, then so has MapC, and they are computed as in C. In other words, given finitely may objects X1, …, Xn in MapC (namely, in C), their product X1 × … × Xn in C is also their product in MapC, and the projection maps and pairing maps are C-maps.

Proof. The projections are C-maps by construction, and the equations defining products are automatically satisfied. We only have to show that given C-maps g1, …, gn from a C-object Z to X1, …, Xn respectively, their pairing ⟨g1, …, gn⟩ in C is a C-map. Let k be any C-probe from, say, C, to Z. We need to show that ⟨g1, …, gn⟩ o k is a C-morphism (or rather, its image by U, if we wish to be entirely formal). But that is equal to ⟨g1 o k, …, gn o k⟩, which is a pairing in D, equivalently in C, hence is a C-morphism. ☐

In the sequel, I will write f × g for the product of two morphisms (in whichever category that has binary products); that is an abbreviation for the morphism ⟨f o π1, g o π2⟩. Before we show that MapC is Cartesian-closed (under some assumptions on C), let us explore the shape of exponentials in C.


Given any two objects X and Y in a category with finite products, the exponential YX, if it exists, is an object, together with:

  • a morphism App : YX × XY (application, sometimes called evaluation);
  • an operation Λ (currification, sometimes called abstraction), such that Λ(h) is a morphism from Z to YX for every morphism h : Z × XY;
  • satisfying the equations:
    • (β) App o (Λ(f) × idX) = f for every morphism f : Z × XY,
    • (η) Λ(App) = idYX
    • (σ) Λ(f) o g = Λ(f o (g × idX)) for all morphisms f : Z × XY and g : Z′ → Z.

This is discussed in Section 5.5.3 of the book. There are many other possible equivalent definitions, but the above definition has two advantages: first, it is closest to what one needs in computer science, as it shows best the connection with the lambda-calculus ((β) is the lambda-calculus’ β-equivalence rule, (η) is η-equivalence, and (σ) is compatibility of lambda-abstractions with substitutions); second, it shows that exponential objects can be characterized entirely equationally (i.e., using equations, not more complicated statements of the form “for every diagram, there is a unique arrow”).

An object X is exponentiable if and only if the exponential YX exists for every object Y. Equivalently, X is exponentiable if and only if the functor _ × X has a right adjoint (and that right adjoint is the functor _X).

Finally, a category is Cartesian-closed if and only if it has all finite products and every object is exponentiable. Those are exactly the models of (simply-typed, extensional) lambda-calculus.

The shape of exponentials in C (when they exist)

We will now assume that D is just Set, as I had warned I would eventually do. A topological functor from C to Set is called a topological construct. We note that Set has all finite products, and is Cartesian-closed.

The following is Corollary 1 in [2]. This is the generalization of the familiar fact that, if the exponential YC of two objects C and Y exists in Top, then it can be taken, up to isomorphism, to be the space of all continuous maps from C to Y, with some unique topology (Theorem 5.5.1 in the book).

In doing so, we will use the fact that any topological functor is uniquely transportable: every isomorphism f from U(Y) to E in D lifts to a unique isomorphism from Y to some (unique) object X in the fiber of E. (In the standard example, this means that given any topological space Y, and any bijection f between the underlying set of Y with some set E, there is a unique topology on E that turns f into a homeomorphism).

Lemma B. Let U : CSet be a topological construct with discrete terminal objects. Given any two objects C and Y in C, if the exponential YC exists in C, then up to isomorphism YC lies in the fiber of the set HomC(C, Y).

Proof. A word of explanation, first: HomC(C, Y) is the hom set from C to Y in C, namely, the set of C-morphisms from C to Y in C. The “up to isomorphism” part means that there is a C-object B in the fiber of HomC(C, Y) that is isomorphic to YC.

Let me also remind you that having discrete terminal objects means that there is exactly one object 1 of C such that U(1) is the one-element set {*}. This must be the terminal object of C, because the terminal objects are the zero-ary products, and products in C are lifted from products in Set. The point in using this assumption is that, given any object Z of C, for every element z of U(Z), there is a unique morphism z1 : 1Z such that U(z1)(*)=z. It is obtained as the U-initial lift of the U-source consisting of the unique function * ↦ z : {*} → U(Z): this lift must be a C-morphism from some object X in the fiber of {*} to Z, and the assumption of having discrete terminal objects guarantees that X is, in fact, 1.

We now show that B exists. For every hU(YC), we build h1 : 1YC, using the latter remark. This allows us to form θ(h) ≝ App o (h1 × idC) o ⟨!C, idC⟩ : CY. Here !C is the unique morphism from C to 1, by definition of 1 as a terminal object. Hence ⟨!C, idC⟩ is a morphism from C to 1 × C, (h1 × idC) goes from 1 × C to YC × C, and App goes from YC × C to Y. Therefore θ(h) is a morphism from C to Y in C, hence an element of HomC(C, Y).

We have therefore defined a map θ from U(YC) to HomC(C, Y). We build a map θ’ in the reverse direction by letting θ'(f) ≝ U(Λ(f o π2))(*) ∈ U(YC), for every C-morphism f : CY. Note that f o π2 is a C-morphism from 1 × C to Y, so Λ(f o π2) is a C-morphism from 1 to YC, so U(Λ(f o π2)) is a function from {*} to U(YC).

We check that θ and θ’ are mutual inverses.

  • We have θ(θ'(f)) = App o (θ'(f)1 × idC) o ⟨!C, idC⟩. By definition, θ'(f)1 is the unique C-morphism from 1 to YC such that U(θ'(f)1)(*)=θ'(f); but θ'(f)=U(Λ(f o π2))(*), so uniqueness implies that θ'(f)1 = Λ(f o π2). Therefore θ(θ'(f)) = App o (Λ(f o π2) × idC) o ⟨!C, idC⟩. Using (β), we see that this is equal to f o π2 o ⟨!C, idC⟩, namely to f.
  • In the other direction, θ'(θ(h)) = U(Λ(θ(h) o π2))(*); now θ(h) o π2 = App o (h1 × idC) o ⟨!C, idC⟩ o π2, and the rightmost composition ⟨!C, idC⟩ o π2 : 1 × C1 × C is the identity map (exercice!). Therefore θ(h) o π2 = App o (h1 × idC). Then Λ(θ(h) o π2) = Λ(App o (h1 × idC)) is equal to Λ(App) o h1 by (σ), hence to h1 since Λ(App) is the identity by (η). We conclude that θ'(θ(h)) = U(h1)(*), which is equal to h, by definition of h1.

By unique transportability, there is a unique object B in the fiber of HomC(C, Y) that turns θ and θ’ into mutually inverse isomorphisms in C. This shows that B, the desired exponential object in the fiber of HomC(C, Y), exists. ☐

Now, and I am ashamed to say so, the proof of Corollary 1 in [2], or rather of Lemma 3 there, contains a gap. It says that application and currification can be characterized concretely, in the manner we are going to describe next. To do so, it says that if YC is already in the fiber of HomC(C, Y), then θ is the identity map, from which the following formulae follow. But that is not true: θ may be a somewhat arbitrary automorphism of HomC(C, Y). We need to be a bit more formal, and allow ourselves to take (yet) another object in the fiber of HomC(C, Y), possibly.

Lemma C. In the setting of Lemma B, we may additionally require that:

  • Application App : YC × CY is such that U(App) is ordinary set-theoretic application, namely U(App) (h, x) = h(x) for all h ∈ HomC(C, Y) and xU(C);
  • Currification Λ(f) : ZYC (where f : Z × CY in C) is such that U(Λ(f)) (z) = f o ⟨z1 o !C, idC⟩ for every zZ. In particular, for every xC, U(U(Λ(f)) (z)) (x) = U(f) (z, x).

Proof. We reuse the notations used in the proof of Lemma B.

Let us recall that θ(h) = App o (h1 × idC) o ⟨!C, idC⟩ : CY, for every hU(YC). We apply the U functor to that equation, and, remembering that U preserves products exactly (by Lemma A), we obtain that U(θ(h)) is U(App) composed with (U(h1) × idU(C)), composed with the map x ↦ (*, x). By definition of h1, U(h1)(*) = h, so U(θ(h)) maps every x in C to U(App) (h, x). Hence:

  • (1) U(App) (h, x) = U(θ(h)) (x) for all h ∈ HomC(C, Y) and xU(C).

Right, there is an extra θ in here, and we will remove it now. The key is to switch to another (isomorphic) exponential object A on C and Y. A is obtained by unique transportability as the unique object in the fiber of HomC(C, Y) that makes θ an isomorphism from YC onto A in C. True, that is exactly what we did in the proof of Lemma B, but we did not make application and currification explicit on that object. Hence let App’ : A × CY be that application and Λ'(f) : ZA denote the currification of f : Z × CY. Explicitly, we recall that θ’ is the inverse of θ, and we have:

  • App’ = App o (θ’ × idC);
  • Λ'(f) = θ o Λ(f).

I will let you check that the usual equations defining application and currification are satisfied:

  • (β’) App’ o (Λ'(f) × idC) = f for every morphism f : Z × CY,
  • (η’) Λ'(App’) = idA,
  • (σ’) Λ'(f) o g = Λ'(f o (g × idC)) for all morphisms f : Z × CY and g : Z′ → Z.

Now equation (1) above applies to every h ≝ θ'(h’) where h’ is arbitrary in U(A) [= HomC(C, Y)], and yields:

  • (2) U(App’) (h‘, x) = h‘ (x) for all h‘ ∈ HomC(C, Y) and xU(C),

which is the first of the equations we are looking for (modulo the replacement of YC by A, and of App by App’).

Similarly, the second equation is U(Λ'(f)) (z) =f o ⟨z1 o !C, idC⟩. We check it as follows. Λ'(f) o z1 is equal to Λ'(f o (z1 × idC)) by (σ’), so U(Λ'(f)) (z) = U(Λ'(f) o z1) (*) = U(Λ'(f o (z1 × idC))) (*). But f o ⟨z1 o !C, idC⟩ o π2 : 1 × CY is equal to f o (z1 × idC); indeed, the π2 here is the inverse of ⟨!C, idC⟩ : C1 × C, and ⟨z1 o !C, idC⟩ = (z1 × idC) o ⟨!C, idC⟩, as one can check using the equations of pairing. We have therefore proved that U(Λ'(f)) (z) = U(Λ'(f o ⟨z1 o !C, idC⟩ o π2)) (*). This is equal to (θ o U(Λ(f o ⟨z1 o !C, idC⟩ o π2))) (*) (using the fact that we have written θ as its own lift, and Λ'(g) = θ o Λ(g) for every g). Now we recall that θ'(g) was defined as U(Λ(g o π2))(*) for every g, so we recognize that U(Λ(f o ⟨z1 o !C, idC⟩ o π2))) (*) = θ’ (f o ⟨z1 o !C, idC⟩). Using that θ’ is its own lift, we obtain that U(Λ'(f)) (z) = θ (U(Λ(f o ⟨z1 o !C, idC⟩ o π2))) (*)) = θ (θ’ (f o ⟨z1 o !C, idC⟩)) = f o ⟨z1 o !C, idC⟩.

The final claim that U(U(Λ'(f)) (z)) (x) = U(f) (z, x) follows immediately, recalling that U (z1) (*)= z. ☐

On top of all that, we can show that the object YC satisfying both the requirements of Lemma B and Lemma C is unique. But we will not need it, and I will skip this.

Strongly productive classes and the Cartesian-closed structure of MapC

Let again D be Set, namely let us assume that U is a topological construct. Let us say that the class C is strongly productive if and only if:

  • every object C of C is exponentiable (in C);
  • the product of any two objects of C in C is in C.

Technically, products are only defined up to isomorphism, so the latter requirement is better understood as “given any two objects of C, at least one of their products in C is in C“. I will ignore that kind of subtlety. The following is Theorem 1 in [2], and is the main result in this post.

Theorem. Let U : CSet be a topological construct with discrete terminal objects, and let us assume that C is a strongly productive class of objects of C. Then MapC is Cartesian-closed.

Proof. Given any two objects X and Y in MapC (namely, in C), let us write C(X,Y) for the set of all C-maps from X to Y. We will build the exponential object on X and Y in MapC as an object of C in the fiber of C(X,Y). (In the standard example, this means that the exponential will be the set of C-maps from X to Y, with some topology.)

Given any C-probe k : CX, there is a map _ o k (post composition with k—which I should really write as _ o U(k)!), which sends every fC(X,Y) to f o U(k) ∈ HomC(C, Y); f o U(k) is a C-morphism indeed, by definition of C-maps. Now, since C, as an object of the strongly productive class C, is exponentiable in C, the exponential object YC exists, and by Lemma B, we may assume that it lies in the fiber of HomC(C, Y). Therefore _ o k is a function from C(X,Y) to U(YC).

We will also assume that App and Λ(f) (for every relevant f) are mapped by U to the specific forms given in Lemma C.

We form the U-source consisting of all the maps _ o k : C(X,Y) → U(YC), where k : CX ranges over all the C-probes with codomain X. (C varies, too, as k does.) Since U is a topological functor, that U-source has a U-initial lift. Explicitly, there is an object A in the fiber of C(X,Y) such that:

  • (I) _ o k is (lifts to) a C-morphism from A to YC for every C-probe k : CX with codomain X;
  • (II) for every function h : U(Z) → C(X,Y), h is a C-morphism if and only if for every C-probe k : CX with codomain X, (_ o k) o h is a C-morphism from Z to YC. (Explicitly, (_ o k) o h is the function that maps every z in U(Z) to h(z) o U(k).)

We claim that this object A is the desired exponential object in MapC. In [2], it is written as [YX]C.

  • We let application in MapC be the function (in Set) AppC : C(X,Y) × U(X) → U(Y) defined by AppC (f, x) ≝ f(x).
    We need to check that AppC is a morphism in MapC, namely that, given any C-probe k : CA × X, AppC o U(k) is (lifts to) a C-morphism. (Yes, we are using Lemma A implicitly here: A × X is in the fiber of U(A) × U(X), namely of C(X,Y) × U(X). I will continue to use Lemma A implicitly on a regular basis.)
    To this end, we write k as ⟨k1, k2⟩, where k1 : CA and k2 : CX; it suffices to define k1 as π1 o k and k2 as π2 o k. We note that k1 and k2 are C-probes, too.
    We then check that AppC o U(k) = U(App o ((_ o k2) × idC) o ⟨k1, idC⟩) : CY. To this end, we use the characterization of U(App) given in Lemma C, namely U(App) (h, x) = h(x). For every c in C, U(App o ((_ o k2) × idC) o ⟨k1, idC⟩) (c) = U(App) (k1(c) o k2, c) = k1(c) (k2(c)) (oh, right, I should write U(k1) and U(k2) instead of k1 and k2, respectively…), while (AppC o U(k)) (c) = AppC (k1(c), k2(c)) = k1(c) (k2(c)) as well.
    Now AppC o U(k) = U(App o ((_ o k2) × idC) o ⟨k1, idC⟩) means exactly that AppC o U(k) lifts to the C-morphism App o ((_ o k2) × idC) o ⟨k1, idC⟩, showing that AppC is a C-map.
  • As far as currification is concerned, we consider an arbitrary C-map f : Z × XY. (Recall that this is just a set function from U(Z) × U(X) to U(Y), with some properties in terms of probes.) For each zZ, there is a function f(z, _) : U(X) → U(Y). The first thing we do is to check that f(z, _) is a C-map from X to Y.
    For every C-probe k : CX, f(z, _) o U(k) = f o U(⟨z1 o !C, k⟩); since ⟨z1 o !C, k⟩ : CZ × X is a C-probe and since f is a C-map, f o U(⟨z1 o !C, k⟩) is a C-morphism, hence also f(z, _) o U(k).
  • Knowing this (still assuming an arbitrary C-map f : Z × XY), we define ΛC(f) as the function zf(z, _) : U(Z) → U(A). We recall that U(A) is equal to C(X,Y), the set of all C-maps from X to Y, hence this is well-typed. We claim that ΛC(f) is itself a C-map.
    To this end, let k1 : C1Z be an arbitrary C-probe with codomain Z. We wish to check that ΛC(f) o U(k1) lifts to a C-morphism from C1 to A. We use property (II) for that, with ΛC(f) o U(k1) for h. In other words, for every C-probe k2 : C2X with codomain X, we must verify that (_ o k2) o ΛC(f) o U(k1) is (lifts to) a C-morphism from C1 to YC2. Let us write F for (_ o k2) o ΛC(f) o U(k1) : U(C1) → U(YC2).
    We recall that (_ o k2) o h is the function that maps every c1 in U(C1) to h(c1) o U(k2). Therefore F maps every c1 in U(C1) to ΛC(f) (U(k1) (c1)) o U(k2). For every c1 in U(C1) and every c2 in U(C2), therefore, U(F (c1)) (c2) = ΛC(f) (U(k1) (c1)) (U(k2) (c2)). By definition of ΛC(f), we obtain that U(F (c1)) (c2) = f (U(k1) (c1)) (U(k2) (c2)).
    Now, since C is closed under binary products, C1 × C2 is in C (or rather, there is at least one product of C1 and C2 that is in C, and we decide to take this one for C1 × C2). This implies that k1 × k2 : C1 × C2Z × X is a C-probe.
    Since f is a C-map, f o (U(k1) × U(k2)) lifts to a C-morphism g : C1 × C2Y. We claim that Λ(g) is the desired lifting of F to a C-morphism (from C1 to YC2).
    It suffices to show that U(Λ(g)) = F, namely that U(Λ(g)) (c1) = F (c1) for every c1 in U(C1). In turn, since U is faithful, it suffices to show that U(U(Λ(g)) (c1)) = U(F(c1)), or equivalently that U(U(Λ(g)) (c1)) (c2) = U(F(c1)) (c2) for every c2C2. We use Lemma C (second part), and we obtain that U(U(Λ(g)) (c1)) (c2) = U(g) (c1, c2). Now U(g) (c1, c2) = (f o (U(k1) × U(k2))) (c1, c2)= f (U(k1) (c1), U(k2) (c2)) = U(F (c1)) (c2), which completes the verification.
    To sum up, Λ(g) lifts F, so F is (lifts to) a C-morphism. Since k2 : C2X is an arbitrary C-probe with codomain X, that is enough to show that ΛC(f) o U(k1) lifts to a C-morphism from C1 to A. Since k1 : C1Z is an arbitrary C-probe with codomain Z, this shows that ΛC(f) is a C-map from Z to A, as claimed.
  • Finally, we verify the equations (β) AppC o (ΛC(f) × id) = f, (η) ΛC(AppC) = id, and (σ) ΛC(f) o g = ΛC(f o (g × id)). Considering that AppC (f, x) = f(x) and ΛC(f) (z) = f (z, _), this is immediate. ☐

Continuing from there

Now that we know that MapC is Cartesian-closed (under some conditions), it is not too hard to show that there is a full subcategory of C, consisting of so-called Cgenerated objects, which is equivalent to MapC, and therefore also Cartesian-closed. This is done in Section 3.2 of [2]. However, and although it is not too hard, it still takes some time to explain, and we have already suffered enough for this time. This, too, follows the Escardó-Lawson-Simpson construction pretty closely [3] (or see Section 5.6 of the book).

A harder result is that, just like the Escardó-Lawson-Simpson construction, the C-generated objects turn out to be exactly the colimits of objects of C. This is the topic of Section 3.3 of [2], and is also adapted from [3]. In the categorical context, however, we need an extra assumption: the class C must contain at least one object C such that U(C) is a non-empty set; I hope you will agree that this is a pretty mild condition. (This condition is not needed in the ordinary Escardó-Lawson-Simpson construction because we can always reduce to the case where this condition holds in Top.)

Finally, all this is done assuming that C is strongly productive, but it is enough to assume that C is productive, namely that it consists of exponential objects (as for strongly productive classes), and that binary products are Cgenerated, not necessarily in C. This approach of dealing with the strongly productive case first, then reducing the productive case to it, is imitated from the book.

Anyway, I may describe those other results another time, or not, who knows. I would like to conclude by saying that, although I was pretty happy to see that the Escardó-Lawson-Simpson construction lifts conveniently beyond topological spaces, and to the setting of topological constructs, I am a bit frustrated that I could not extend it to topological functors with values in a more general category D than Set. For example, there is a topological functor (not a construct) from the category of streams to Top, and such a more general result would perhaps give a more straightforward construction of the various Cartesian-closed categories of streams that I am building in [2].

  1. Jǐrí Adámek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories. The Joy of Cats. John Wiley and Sons, 1990. Online edition, 2004.
  2. Jean Goubault-Larrecq. Exponentiable streams and prestreams. Applied Categorical Structures 22, pages 515–549, 2014. The published version, available from Springer Link, contains two mistakes, which are repaired in the HAL report.
  3. Martín Escardó, Jimmie Lawson, and Alex Simpson. Comparing Cartesian Closed Categories of (Core) Compactly Generated Spaces. Topology and Its Applications, 143(1–3):105–146, 2004.

Jean Goubault-Larrecq (April 20th, 2023)