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 Map_C, 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 : C → D 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 : X → Y 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 g_i : E → U(Y_i), i ∈ I, with common domain E. (Note that each C-object Y_i is part of the datum, not just U(Y_i). In the standard example, this means we are given topological spaces Y_i, 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 g_i into a C-morphism from X to Y_i.

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 g_i 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 g_i o h is a C-morphism from Z to Y_i 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, X≤Y) 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 : C → D 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).

Probes

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 : C → D 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 : C → X whose domain is an object C in C.

Let us define a C–map 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 : C → X 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 : X → Y induces a C-map U(g). Indeed, for every C-probe k : C → X, 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 Map_C 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 Map_C

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 X₁, …, X_n in C is obtained by computing the product U(X₁) × … × U(X_n) 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(X₁) × … × U(X_n) the coarsest topology that makes all projections continuous, namely the product topology.)

I will simply write X₁ × … × X_n 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 g₁, …, g_n are C-morphisms with the same domain in C, then their pairing ⟨g₁, …, g_n⟩ in C is obtained by computing the pairing ⟨U(g₁), …, U(g_n)⟩ in D, and realizing that this lifts to a unique C-morphism; we write it as ⟨g₁, …, g_n⟩, so that U(⟨g₁, …, g_n⟩) = ⟨U(g₁), …, U(g_n)⟩ and then it is easy to check that the equations defining products are satisfied, namely: π_i o ⟨g₁, …, g_n⟩ = g_i (1≤i≤n), ⟨g₁, …, g_n⟩ o h = ⟨g₁ o h, …, g_n o h⟩, and ⟨π₁, …, π_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 ⟨g₁, …, g_n⟩ 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 Map_C, and they are computed as in C. In other words, given finitely may objects X₁, …, X_n in Map_C (namely, in C), their product X₁ × … × X_n in C is also their product in Map_C, 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 g₁, …, g_n from a C-object Z to X₁, …, X_n respectively, their pairing ⟨g₁, …, g_n⟩ in C is a C-map. Let k be any C-probe from, say, C, to Z. We need to show that ⟨g₁, …, g_n⟩ o k is a C-morphism (or rather, its image by U, if we wish to be entirely formal). But that is equal to ⟨g₁ o k, …, g_n 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 π₁, g o π₂⟩. Before we show that Map_C is Cartesian-closed (under some assumptions on C), let us explore the shape of exponentials in C.

Exponentials

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

• a morphism App : Y^X × X → Y (application, sometimes called evaluation);
• an operation Λ (currification, sometimes called abstraction), such that Λ(h) is a morphism from Z to Y^X for every morphism h : Z × X → Y;
• satisfying the equations:
  • (β) App o (Λ(f) × id_X) = f for every morphism f : Z × X → Y,
  • (η) Λ(App) = id_Y^X
  • (σ) Λ(f) o g = Λ(f o (g × id_X)) for all morphisms f : Z × X → Y 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 Y^X 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 Y^C 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 : C → Set be a topological construct with discrete terminal objects. Given any two objects C and Y in C, if the exponential Y^C exists in C, then up to isomorphism Y^C lies in the fiber of the set Hom_C(C, Y).

Proof. A word of explanation, first: Hom_C(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 Hom_C(C, Y) that is isomorphic to Y^C.

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 z¹ : 1 → Z such that U(z¹)(*)=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 h ∈ U(Y^C), we build h¹ : 1 → Y^C, using the latter remark. This allows us to form θ(h) ≝ App o (h¹ × id_C) o ⟨!_C, id_C⟩ : C → Y. Here !_C is the unique morphism from C to 1, by definition of 1 as a terminal object. Hence ⟨!_C, id_C⟩ is a morphism from C to 1 × C, (h¹ × id_C) goes from 1 × C to Y^C × C, and App goes from Y^C × C to Y. Therefore θ(h) is a morphism from C to Y in C, hence an element of Hom_C(C, Y).

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

We check that θ and θ’ are mutual inverses.

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

By unique transportability, there is a unique object B in the fiber of Hom_C(C, Y) that turns θ and θ’ into mutually inverse isomorphisms in C. This shows that B, the desired exponential object in the fiber of Hom_C(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 Y^C is already in the fiber of Hom_C(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 Hom_C(C, Y). We need to be a bit more formal, and allow ourselves to take (yet) another object in the fiber of Hom_C(C, Y), possibly.

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

• Application App : Y^C × C → Y is such that U(App) is ordinary set-theoretic application, namely U(App) (h, x) = h(x) for all h ∈ Hom_C(C, Y) and x ∈ U(C);
• Currification Λ(f) : Z → Y^C (where f : Z × C → Y in C) is such that U(Λ(f)) (z) = f o ⟨z¹ o !_C, id_C⟩ for every z ∈ Z. In particular, for every x ∈ C, 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 (h¹ × id_C) o ⟨!_C, id_C⟩ : C → Y, for every h ∈ U(Y^C). 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(h¹) × id_U(C)), composed with the map x ↦ (*, x). By definition of h¹, U(h¹)(*) = 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 ∈ Hom_C(C, Y) and x ∈ U(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 Hom_C(C, Y) that makes θ an isomorphism from Y^C 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 × C → Y be that application and Λ'(f) : Z → A denote the currification of f : Z × C → Y. Explicitly, we recall that θ’ is the inverse of θ, and we have:

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

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

• (β’) App’ o (Λ'(f) × id_C) = f for every morphism f : Z × C → Y,
• (η’) Λ'(App’) = id_A,
• (σ’) Λ'(f) o g = Λ'(f o (g × id_C)) for all morphisms f : Z × C → Y and g : Z′ → Z.

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

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

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

Similarly, the second equation is U(Λ'(f)) (z) =f o ⟨z¹ o !_C, id_C⟩. We check it as follows. Λ'(f) o z¹ is equal to Λ'(f o (z¹ × id_C)) by (σ’), so U(Λ'(f)) (z) = U(Λ'(f) o z¹) (*) = U(Λ'(f o (z¹ × id_C))) (*). But f o ⟨z¹ o !_C, id_C⟩ o π₂ : 1 × C → Y is equal to f o (z¹ × id_C); indeed, the π₂ here is the inverse of ⟨!_C, id_C⟩ : C → 1 × C, and ⟨z¹ o !_C, id_C⟩ = (z¹ × id_C) o ⟨!_C, id_C⟩, as one can check using the equations of pairing. We have therefore proved that U(Λ'(f)) (z) = U(Λ'(f o ⟨z¹ o !_C, id_C⟩ o π₂)) (*). This is equal to (θ o U(Λ(f o ⟨z¹ o !_C, id_C⟩ o π₂))) (*) (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 π₂))(*) for every g, so we recognize that U(Λ(f o ⟨z¹ o !_C, id_C⟩ o π₂))) (*) = θ’ (f o ⟨z¹ o !_C, id_C⟩). Using that θ’ is its own lift, we obtain that U(Λ'(f)) (z) = θ (U(Λ(f o ⟨z¹ o !_C, id_C⟩ o π₂))) (*)) = θ (θ’ (f o ⟨z¹ o !_C, id_C⟩)) = f o ⟨z¹ o !_C, id_C⟩.

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

On top of all that, we can show that the object Y^C 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 Map_C

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 : C → Set be a topological construct with discrete terminal objects, and let us assume that C is a strongly productive class of objects of C. Then Map_C is Cartesian-closed.

Proof. Given any two objects X and Y in Map_C (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 Map_C 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 : C → X, there is a map _ o k (post composition with k—which I should really write as _ o U(k)!), which sends every f ∈ C(X,Y) to f o U(k) ∈ Hom_C(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 Y^C exists, and by Lemma B, we may assume that it lies in the fiber of Hom_C(C, Y). Therefore _ o k is a function from C(X,Y) to U(Y^C).

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(Y^C), where k : C → X 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 Y^C for every C-probe k : C → X 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 : C → X with codomain X, (_ o k) o h is a C-morphism from Z to Y^C. (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 Map_C. In [2], it is written as [Y^X]_C.

• We let application in Map_C be the function (in Set) App_C : C(X,Y) × U(X) → U(Y) defined by App_C (f, x) ≝ f(x).
  We need to check that App_C is a morphism in Map_C, namely that, given any C-probe k : C → A × X, App_C 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 ⟨k₁, k₂⟩, where k₁ : C → A and k₂ : C → X; it suffices to define k₁ as π₁ o k and k₂ as π₂ o k. We note that k₁ and k₂ are C-probes, too.
  We then check that App_C o U(k) = U(App o ((_ o k₂) × id_C) o ⟨k₁, id_C⟩) : C → Y. 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 k₂) × id_C) o ⟨k₁, id_C⟩) (c) = U(App) (k₁(c) o k₂, c) = k₁(c) (k₂(c)) (oh, right, I should write U(k₁) and U(k₂) instead of k₁ and k₂, respectively…), while (App_C o U(k)) (c) = App_C (k₁(c), k₂(c)) = k₁(c) (k₂(c)) as well.
  Now App_C o U(k) = U(App o ((_ o k₂) × id_C) o ⟨k₁, id_C⟩) means exactly that App_C o U(k) lifts to the C-morphism App o ((_ o k₂) × id_C) o ⟨k₁, id_C⟩, showing that App_C is a C-map.
• As far as currification is concerned, we consider an arbitrary C-map f : Z × X → Y. (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 z ∈ Z, 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 : C → X, f(z, _) o U(k) = f o U(⟨z¹ o !_C, k⟩); since ⟨z¹ o !_C, k⟩ : C → Z × X is a C-probe and since f is a C-map, f o U(⟨z¹ o !_C, k⟩) is a C-morphism, hence also f(z, _) o U(k).
• Knowing this (still assuming an arbitrary C-map f : Z × X → Y), we define Λ_C(f) as the function z ↦ f(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 k₁ : C₁ → Z be an arbitrary C-probe with codomain Z. We wish to check that Λ_C(f) o U(k₁) lifts to a C-morphism from C₁ to A. We use property (II) for that, with Λ_C(f) o U(k₁) for h. In other words, for every C-probe k₂ : C₂ → X with codomain X, we must verify that (_ o k₂) o Λ_C(f) o U(k₁) is (lifts to) a C-morphism from C₁ to Y^C₂. Let us write F for (_ o k₂) o Λ_C(f) o U(k₁) : U(C₁) → U(Y^C₂).
  We recall that (_ o k₂) o h is the function that maps every c₁ in U(C₁) to h(c₁) o U(k₂). Therefore F maps every c₁ in U(C₁) to Λ_C(f) (U(k₁) (c₁)) o U(k₂). For every c₁ in U(C₁) and every c₂ in U(C₂), therefore, U(F (c₁)) (c₂) = Λ_C(f) (U(k₁) (c₁)) (U(k₂) (c₂)). By definition of Λ_C(f), we obtain that U(F (c₁)) (c₂) = f (U(k₁) (c₁)) (U(k₂) (c₂)).
  Now, since C is closed under binary products, C₁ × C₂ is in C (or rather, there is at least one product of C₁ and C₂ that is in C, and we decide to take this one for C₁ × C₂). This implies that k₁ × k₂ : C₁ × C₂ → Z × X is a C-probe.
  Since f is a C-map, f o (U(k₁) × U(k₂)) lifts to a C-morphism g : C₁ × C₂ → Y. We claim that Λ(g) is the desired lifting of F to a C-morphism (from C₁ to Y^C₂).
  It suffices to show that U(Λ(g)) = F, namely that U(Λ(g)) (c₁) = F (c₁) for every c₁ in U(C₁). In turn, since U is faithful, it suffices to show that U(U(Λ(g)) (c₁)) = U(F(c₁)), or equivalently that U(U(Λ(g)) (c₁)) (c₂) = U(F(c₁)) (c₂) for every c₂ ∈ C₂. We use Lemma C (second part), and we obtain that U(U(Λ(g)) (c₁)) (c₂) = U(g) (c₁, c₂). Now U(g) (c₁, c₂) = (f o (U(k₁) × U(k₂))) (c₁, c₂)= f (U(k₁) (c₁), U(k₂) (c₂)) = U(F (c₁)) (c₂), which completes the verification.
  To sum up, Λ(g) lifts F, so F is (lifts to) a C-morphism. Since k₂ : C₂ → X is an arbitrary C-probe with codomain X, that is enough to show that Λ_C(f) o U(k₁) lifts to a C-morphism from C₁ to A. Since k₁ : C₁ → Z 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 (β) App_C o (Λ_C(f) × id) = f, (η) Λ_C(App_C) = id, and (σ) Λ_C(f) o g = Λ_C(f o (g × id)). Considering that App_C (f, x) = f(x) and Λ_C(f) (z) = f (z, _), this is immediate. ☐

Continuing from there

Now that we know that Map_C 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 C–generated objects, which is equivalent to Map_C, 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 C–generated, 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)