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 **C**ontinuous.)

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*is part of the datum, not just

_{i}*U*(

*Y*). In the standard example, this means we are given

_{i}*topological spaces*

*Y*, not just their underlying sets.) A

_{i}*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*into a

_{i}**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*o

_{i}*h*is a

**C**-morphism from

*Z*to

*Y*for every

_{i}*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*_{1}, …, *X _{n}* in

**C**is obtained by computing the product

*U*(

*X*

_{1}) × … ×

*U*(

*X*) in

_{n}**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*

_{1}) × … ×

*U*(

*X*) the coarsest topology that makes all projections continuous, namely the product topology.)

_{n}I will simply write *X*_{1} × … × *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*_{1}, …, *g _{n}* are

**C**-morphisms with the same domain in

**C**, then their pairing ⟨

*g*

_{1}, …,

*g*⟩ in

_{n}**C**is obtained by computing the pairing ⟨

*U*(

*g*

_{1}), …,

*U*(

*g*)⟩ in

_{n}**D**, and realizing that this lifts to a unique

**C**-morphism; we write it as ⟨

*g*

_{1}, …,

*g*⟩, so that

_{n}*U*(⟨

*g*

_{1}, …,

*g*⟩) = ⟨

_{n}*U*(

*g*

_{1}), …,

*U*(

*g*)⟩ and then it is easy to check that the equations defining products are satisfied, namely: π

_{n}*o ⟨*

_{i}*g*

_{1}, …,

*g*⟩ =

_{n}*g*

_{i}(1≤

*i*≤

*n*), ⟨

*g*

_{1}, …,

*g*⟩ o

_{n}*h*= ⟨

*g*

_{1}o

*h*, …,

*g*o

_{n}*h*⟩, and ⟨π

_{1}, …, π

*⟩ = id, where π*

_{n}*is projection onto the*

_{i}*i*th component.

In the sequel, I will drop mentions of *U*, as they tend to obscure the message, and therefore I will write ⟨*g*_{1}, …, *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*_{1}, …, *X _{n}* in

**Map**

_{C}(namely, in

**C**), their product

*X*

_{1}× … ×

*X*in

_{n}**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*_{1}, …, *g _{n}* from a

**C**-object

*Z*to

*X*

_{1}, …,

*X*respectively, their pairing ⟨

_{n}*g*

_{1}, …,

*g*⟩ in

_{n}**C**is a C-map. Let

*k*be any C-probe from, say,

*C*, to

*Z*. We need to show that ⟨

*g*

_{1}, …,

*g*⟩ o

_{n}*k*is a

**C**-morphism (or rather, its image by

*U*, if we wish to be entirely formal). But that is equal to ⟨

*g*

_{1}o

*k*, …,

*g*o

_{n}*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

**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*for every morphism^{X}*h*:*Z*×*X*→*Y*; - satisfying the equations:
- (β) App o (Λ(
*f*) × id) =_{X}*f*for every morphism*f*:*Z*×*X*→*Y*, - (η) Λ(App) = id
_{YX} - (σ) Λ(
*f*) o*g*= Λ(*f*o (*g*× id)) for all morphisms_{X}*f*:*Z*×*X*→*Y*and*g*:*Z′*→*Z*.

- (β) App o (Λ(

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*lies in the fiber of the set Hom

^{C}**(**

_{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} : **1** → *Z* such that *U*(*z*^{1})(*)=*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}:

**1**→

*Y*, using the latter remark. This allows us to form θ(

^{C}*h*) ≝ App o (

*h*

^{1}× id

*) o ⟨!*

_{C}*, id*

_{C}*⟩ :*

_{C}*C*→

*Y*. Here !

*is the unique morphism from*

_{C}*C*to

**1**, by definition of

**1**as a terminal object. Hence ⟨!

*, id*

_{C}*⟩ is a morphism from*

_{C}*C*to

**1**×

*C*, (

*h*

^{1}× id

*) goes from*

_{C}**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 π

_{2}))(*) ∈

*U*(

*Y*), for every

^{C}**C**-morphism

*f*:

*C*→

*Y*. 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

*Y*, so

^{C}*U*(Λ(

*f*o π

_{2})) is a function from {*} to

*U*(

*Y*).

^{C}We check that θ and θ’ are mutual inverses.

- We have θ(θ'(
*f*)) = App o (θ'(*f*)^{1}× id) o ⟨!_{C}, id_{C}⟩. By definition, θ'(_{C}*f*)^{1}is the unique**C**-morphism from**1**to*Y*such that^{C}*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}) × id) o ⟨!_{C}, id_{C}⟩. Using (β), we see that this is equal to_{C}*f*o π_{2}o ⟨!, id_{C}⟩, namely to_{C}*f*. - In the other direction, θ'(θ(
*h*)) =*U*(Λ(θ(*h*) o π_{2}))(*); now θ(*h*) o π_{2}= App o (*h*^{1}× id) o ⟨!_{C}, id_{C}⟩ o π_{C}_{2}, and the rightmost composition ⟨!, id_{C}⟩ o π_{C}_{2}:**1**×*C*→**1**×*C*is the identity map (exercice!). Therefore θ(*h*) o π_{2}= App o (*h*^{1}× id). Then Λ(θ(_{C}*h*) o π_{2}) = Λ(App o (*h*^{1}× id)) is equal to Λ(App) o_{C}*h*^{1}by (σ), hence to*h*^{1}since Λ(App) is the identity by (η). We conclude that θ'(θ(*h*)) =*U*(*h*^{1})(*), which is equal to*h*, by definition of*h*^{1}.

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*(where^{C}*f*:*Z*×*C*→*Y*in**C**) is such that*U*(Λ(*f*)) (*z*) =*f*o ⟨o !*z*^{1}, id_{C}⟩ for every_{C}*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*^{1} × id* _{C}*) o ⟨!

*, id*

_{C}*⟩ :*

_{C}*C*→

*Y*, for every

*h*∈

*U*(

*Y*). We apply the

^{C}*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*

^{1}) × id

_{U}_{(}

_{C}_{)}), composed with the map

*x*↦ (*,

*x*). By definition of

*h*

^{1},

*U*(

*h*

^{1})(*) =

*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*onto

^{C}*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)) for all morphisms_{C}*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^{1}* o !

*, id*

_{C}*⟩. We check it as follows. Λ'(*

_{C}*f*) o

*z*

^{1}is equal to Λ'(

*f*o (

*× id*

*z*^{1}*)) by (σ’), so*

_{C}*U*(Λ'(

*f*)) (

*z*) =

*U*(Λ'(

*f*) o

*z*

^{1}) (*) =

*U*(Λ'(

*f*o (

*× id*

*z*^{1}*))) (*). But*

_{C}*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩ o π*

_{C}_{2}:

**1**×

*C*→

*Y*is equal to

*f*o (

*× id*

*z*^{1}*); indeed, the π*

_{C}_{2}here is the inverse of ⟨!

*, id*

_{C}*⟩ :*

_{C}*C*→

**1**×

*C*, and ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩ = (*

_{C}*× id*

*z*^{1}*) o ⟨!*

_{C}*, id*

_{C}*⟩, as one can check using the equations of pairing. We have therefore proved that*

_{C}*U*(Λ'(

*f*)) (

*z*) =

*U*(Λ'(

*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩ o π*

_{C}_{2})) (*). This is equal to (θ o

*U*(Λ(

*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩ o π*

_{C}_{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 ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩ o π*

_{C}_{2}))) (*) = θ’ (

*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩). Using that θ’ is its own lift, we obtain that*

_{C}*U*(Λ'(

*f*)) (

*z*) = θ (

*U*(Λ(

*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩ o π*

_{C}_{2}))) (*)) = θ (θ’ (

*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩)) =*

_{C}*f*o ⟨

*o !*

*z*^{1}*, id*

_{C}*⟩.*

_{C}The final claim that *U*(*U*(Λ'(*f*)) (*z*)) (*x*) = *U*(*f*) (*z*, *x*) follows immediately, recalling that *U* (* z^{1}*) (*)=

*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*exists, and by Lemma B, we may assume that it lies in the fiber of Hom

^{C}**(**

_{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*for every C-probe^{C}*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*. (Explicitly, (_ o^{C}*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*_{1},*k*_{2}⟩, where*k*_{1}:*C*→*A*and*k*_{2}:*C*→*X*; it suffices to define*k*_{1}as π_{1}o*k*and*k*_{2}as π_{2}o*k*. We note that*k*_{1}and*k*_{2}are C-probes, too.

We then check that App_{C}o*U*(*k*) =*U*(App o ((_ o*k*_{2}) × id) o ⟨_{C}*k*_{1}, 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*_{2}) × id) o ⟨_{C}*k*_{1}, id⟩) (_{C}*c*) =*U*(App) (*k*_{1}(*c*) o*k*_{2},*c*) =*k*_{1}(*c*) (*k*_{2}(*c*)) (oh, right, I should write*U*(*k*_{1}) and*U*(*k*_{2}) instead of*k*_{1}and*k*_{2}, respectively…), while (App_{C}o*U*(*k*)) (*c*) = App_{C}(*k*_{1}(*c*),*k*_{2}(*c*)) =*k*_{1}(*c*) (*k*_{2}(*c*)) as well.

Now App_{C}o*U*(*k*) =*U*(App o ((_ o*k*_{2}) × id) o ⟨_{C}*k*_{1}, id⟩) means exactly that App_{C}_{C}o*U*(*k*) lifts to the**C**-morphism App o ((_ o*k*_{2}) × id) o ⟨_{C}*k*_{1}, id⟩, showing that App_{C}_{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*^{1}o !,_{C}*k*⟩); since ⟨*z*^{1}o !,_{C}*k*⟩ :*C*→*Z*×*X*is a C-probe and since*f*is a C-map,*f*o*U*(⟨*z*^{1}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*_{1}:*C*_{1}→*Z*be an arbitrary C-probe with codomain*Z*. We wish to check that Λ_{C}(*f*) o*U*(*k*_{1}) lifts to a**C**-morphism from*C*_{1}to*A*. We use property (II) for that, with Λ_{C}(*f*) o*U*(*k*_{1}) for*h*. In other words, for every C-probe*k*_{2}:*C*_{2}→*X*with codomain*X*, we must verify that (_ o*k*_{2}) o Λ_{C}(*f*) o*U*(*k*_{1}) is (lifts to) a**C**-morphism from*C*_{1}to*Y*^{C}^{2}. Let us write*F*for (_ o*k*_{2}) o Λ_{C}(*f*) o*U*(*k*_{1}) :*U*(*C*_{1}) →*U*(*Y*^{C}^{2}).

We recall that (_ o*k*_{2}) o*h*is the function that maps every*c*_{1}in*U*(*C*_{1}) to*h*(*c*_{1}) o*U*(*k*_{2}). Therefore*F*maps every*c*_{1}in*U*(*C*_{1}) to Λ_{C}(*f*) (*U*(*k*_{1}) (*c*_{1})) o*U*(*k*_{2}). For every*c*_{1}in*U*(*C*_{1}) and every*c*_{2}in*U*(*C*_{2}), therefore,*U*(*F*(*c*_{1})) (*c*_{2}) = Λ_{C}(*f*) (*U*(*k*_{1}) (*c*_{1})) (*U*(*k*_{2}) (*c*_{2})). By definition of Λ_{C}(*f*), we obtain that*U*(*F*(*c*_{1})) (*c*_{2}) =*f*(*U*(*k*_{1}) (*c*_{1})) (*U*(*k*_{2}) (*c*_{2})).

Now, since C is closed under binary products,*C*_{1}×*C*_{2}is in C (or rather, there is at least one product of*C*_{1}and*C*_{2}that is in C, and we decide to take this one for*C*_{1}×*C*_{2}). This implies that*k*_{1}×*k*_{2}:*C*_{1}×*C*_{2}→*Z*×*X*is a C-probe.

Since*f*is a C-map,*f*o (*U*(*k*_{1}) ×*U*(*k*_{2})) lifts to a**C**-morphism*g*:*C*_{1}×*C*_{2}→*Y*. We claim that Λ(*g*) is the desired lifting of*F*to a**C**-morphism (from*C*_{1}to).*Y*^{C}^{2}

It suffices to show that*U*(Λ(*g*)) =*F*, namely that*U*(Λ(*g*)) (*c*_{1}) =*F*(*c*_{1}) for every*c*_{1}in*U*(*C*_{1}). In turn, since*U*is faithful, it suffices to show that*U*(*U*(Λ(*g*)) (*c*_{1})) =*U*(*F*(*c*_{1})), or equivalently that*U*(*U*(Λ(*g*)) (*c*_{1})) (*c*_{2}) =*U*(*F*(*c*_{1})) (*c*_{2}) for every*c*_{2}∈*C*_{2}. We use Lemma C (second part), and we obtain that*U*(*U*(Λ(*g*)) (*c*_{1})) (*c*_{2}) =*U*(*g*) (*c*_{1},*c*_{2}). Now*U*(*g*) (*c*_{1},*c*_{2}) = (*f*o (*U*(*k*_{1}) ×*U*(*k*_{2}))) (*c*_{1},*c*_{2})=*f*(*U*(*k*_{1}) (*c*_{1}),*U*(*k*_{2}) (*c*_{2})) =*U*(*F*(*c*_{1})) (*c*_{2}), which completes the verification.

To sum up, Λ(*g*) lifts*F*, so*F*is (lifts to) a**C**-morphism. Since*k*_{2}:*C*_{2}→*X*is an arbitrary C-probe with codomain*X*, that is enough to show that Λ_{C}(*f*) o*U*(*k*_{1}) lifts to a**C**-morphism from*C*_{1}to*A*. Since*k*_{1}:*C*_{1}→*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].

- 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.
- 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. - 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)