Todd Trimble Three topos theorems in one

I want to discuss a neat theorem (theorem 2 below) which manages to roll several fundamental theorems of topos theory into one.

I’ve known this theorem for some time now (since about 1997), but for a long time it struck me as just a kind of curiosity – I didn’t know any exciting new applications, and I didn’t even know what I should name the new concept that the theorem depends on. But, after thinking about some recent discussion on the blog on modal logic, it occurred to me there might be some justification for christening this new concept “modal operator”.

Just giving the baby a jazzy new name (even if it doesn’t really suit her in the end) somehow rekindled the motivation to want to show her to people: write down the proofs, see if I could make it grow, and so on. And in the process, I found a way to construct modal operators that for some reason hadn’t occurred to me before (theorem 3). If anyone knows about this concept from somewhere else, I’d really like to know about it!

Although this article is more or less self-contained, it’s really addressed to those who know some topos theory at an introductory level, say through the first five chapters of the book by Mac Lane and Moerdijk. I’ve included a little appendix on a way to think about sheafification, which I’m sure is known to experts but which I’ve never seen written down.

Three theorems

There are three basic theorems for building new toposes from old ones:

• Slice theorem: If $E$ is a topos and $X$ is an object, then $E/X$ is a topos.

• Lex comonad theorem: If $G: E \to E$ is a left exact comonad acting on a topos $E$, then the category of $G$-coalgebras is also a topos.

If the slice theorem is the one which passes to toposes of presheaves on internal discrete categories, then the lex comonad theorem is the one which, among other things, extends that further to toposes of presheaves on general internal categories.

• Lex idempotent monad theorem: If $J: E \to E$ is a left exact idempotent monad acting on a topos $E$, then the category of $J$-algebras is also a topos.

This is the theorem which takes us from presheaves to sheaves. Here the monad $J$ is the composite of taking the associated sheaf functor (which is left exact) followed by the forgetful functor from sheaves to presheaves; the $J$-algebras are the sheaves. The monad $J$ is idempotent because the associated sheaf of a sheaf $X$ is canonically isomorphic to $X$ (alternatively, because the embedding of sheaves in presheaves is full and faithful). In fact, every such lex idempotent monad on a topos $E$ arises in this way, by sheafifying with respect to a Lawvere-Tierney topology in $E$.

Thus the three theorems taken together effect the passage from a base category $Set$ as a topos, to Grothendieck toposes. We will show how to effect this passage in just one step, instead of three separate ones. In fact, we will see that all three theorems can be combined into one master theorem (theorem 2 below).

Two theorems in one

The first reduction combines the slice theorem and the lex comonad theorem into one. The idea is rather simple. Indeed, notice that the slice $E/X$ is the category of coalgebras for the comonad $- \times X: E \to E$, where the comonad structure comes from the unique comonoid structure which exists on any object $X$:

The comonad $- \times X$ isn’t left exact (it doesn’t preserve the terminal object), but it does preserve pullbacks.

Thus, we will reproduce the following theorem. It has long been known as folklore to experts, and appears in Johnstone’s Sketches of an Elephant, section A, Remark 4.2.3.

Lemma 0: If $(S, \gamma: S \to G S)$ is a $G$-coalgebra, then the coassociativity square

is a pullback. In any pullback, if the two pullback projections coincide (as here, where they are both $\gamma$), then the pullback projection is monic.

Now we return to the proof of Theorem 1; it remains to show that the equalizer $j: P_G(Y) \to G P Y$ of the pair of maps in (2) is the power object of the coalgebra $(Y, \eta: Y \to G Y)$. Let $(X, \theta: X \to G X)$ be a coalgebra, and $f: X \to P_G(Y)$ a coalgebra map. Then $g = j f: X \to G P Y$ equalizes the maps in (2). Moreover, since $G P Y$ is cofree, we have that to each $G$-coalgebra map $g: X \to G P Y$, there exists a unique $h: X \to P Y$ in the topos $E$ such that

Thus $g: X \to G P Y$ in $E_G$ or $h: X \to P Y$ in $E$ corresponds to a subobject $i: R \hookrightarrow X \times Y$ in $E$. We need to check that the condition that $g$ equalizes the pair of maps in (2) corresponds precisely to the condition that $R$ is a subcoalgebra of $X \times_{G 1} Y$ (the product of $X$ and $Y$ in $E_G$). Or, taking into account lemmas 0, 1, 2: precisely to the condition that there is a pullback diagram of the form

where $\gamma$ is the coalgebra structure on $X \times_{G 1} Y$, and $k$ is monic.

Application of theorem 1

Let us put this theorem to work, by showing how the passage from a topos $E$ to the topos of presheaves on an internal category can be accomplished in just one step, instead of two. Given an internal category in $E$ with underlying span

there is a comonad formed as the composite

where $s^*$ denotes pulling back along $s$, and $\Pi_t$ is right adjoint to $t^*$.

This comonad takes an object $Y$ of $E$ (“a set”) to

where $t^{-1}(x)$ denotes the set of all morphisms whose target is $x \in C_0$. This comonad is manifestly pullback-preserving. A coalgebra structure

sends $y \in Y$ to some summand at an index $x$ (so we think of this $y \mapsto x$ as giving a fibering $p: Y \to C_0$). More precisely, $y$ is mapped to a function $y^{-}: t^{-1}(x) \to Y$, so that given $f: x' \to x = p(y)$ in $t^{-1}(x)$, hitting it with $y^{-}$ gives an element $y^f$ in $Y$. The assignments $(f, y) \mapsto y^f$ should be thought of as producing a (contravariant) action of $C$ on the fibered set $Y \to C_0$, inasmuch as the coalgebra axioms guarantee equational axioms of the form

wherever they make sense. But such a $C$-action is simply another name for a presheaf $F$ on $C$, where the fibering $Y \to C_0$ corresponds to the category of elements of $F$.

In summary, coalgebras of this comonad $G: E \to E$ are exactly internal presheaves on $C$, and theorem 1 shows that the category of presheaves is a topos, in a single shot.

Two theorems in one, again

We’ve now given a reduction of three fundamental theorems of topos theory to two:

• Pullback-preserving comonad theorem: Given a pullback-preserving comonad $G: E \to E$ acting on a topos $E$, the category of coalgebras $E_G$ is a topos.

• Lex idempotent monad theorem: Given a left exact idempotent monad $J : E \to E$ acting on a topos $E$, the category of algebras $E^J$ is a topos.

What is interesting in these cases is that the relevant constructions, in particular the construction of power objects, can be made to look exactly the same in $E^J$ as in $E_G$. It is therefore very tempting to seek a further reduction, i.e., a generalization which combines these two theorems into one. But finding a common generalization of monads and comonads would seem to be an ill-advised task, to say the least.

In particular, there is no analogue of the counit

in the monad case, even when the monad is idempotent. However, looking over our earlier proofs, particularly of lemmas 0, 1, and 2, we found that the presence of a counit for our comonad $G$ played a very restricted role. In fact, it played no essential role whatsoever, except in one place in the proof of lemma 0, where it was used to prove that coalgebra structures fit into pullback squares

here we used only the fact that $G\varepsilon$ was a common left inverse to $\delta$, $G\gamma$. In other words, if we take this pullback property for granted, then the rest of the proof of theorem 1 goes through without invoking the counit again.

Let’s look now at the monad side of things. For general monads $J$, there are two structure maps

where $u: 1 \to J$ denotes the unit, but for idempotent monads these maps coincide: each is the inverse of the monad multiplication

which for an idempotent monad is an isomorphism, by definition. Moreover, an algebra structure for an idempotent monad,

is itself an isomorphism with inverse given by the unit $u X: X \to J X$. In particular, it is trivial that for a $J$-algebra $X$, the following square is a pullback:

since all arrows in sight are isomorphisms. If we then define $\delta: J \to J J$ to be $u J$, then this pullback square for $J$-algebras has the same formal shape as the pullback square for $G$-coalgebras above.

With these preliminaries in place, we now propose the following definition as a generalization of pullback-preserving comonad and lex idempotent monad:

Definition 1: Let $E$ be a finitely complete category.

• A modal operator on $E$ is a pullback-preserving functor $G: E \to E$ equipped with a transformation $\delta: G \to G G$, such that the following coassociativity square is a pullback:

  $$\array{ G & \stackrel{\delta}{\to} & G G \\ \delta \downarrow & & G\delta \\ G G & \stackrel{\delta G}{\to} & G G G }$$

• A modal operator $(G, \delta)$ is strict if

  $$1_{G 1} = (G 1 \stackrel{\delta G 1}{\to} G G 1 \stackrel{G 1}{\to} G 1)$$

• If $(G, \delta)$ is a modal operator on $E$, then a $G$-structure is an object $X$ of $E$ together with a morphism $\eta: X \to G X$ such that the coassociativity square

  $$\array{ X & \stackrel{\eta}{\to} & G X \\ \eta \downarrow & & \downarrow G\eta \\ G X & \stackrel{\delta X}{\to} & G G X }$$

  is a pullback. A morphism of $G$-structures $(X, \eta)$, $(Y, \theta: Y \to G Y)$ is a map $f: X \to Y$ such that

  $$\array{ X & \stackrel{\eta}{\to} & G X \\ f \downarrow & & \downarrow G f \\ Y & \stackrel{\theta}{\to} & G Y }$$

  commutes. $\Box$

The category of $G$-structures will be denoted $E_G$. It is not hard to see that $G$ is strict if and only if $G 1$ is terminal in $E_G$.

Remark: I invite discussion about the appropriateness of the term ‘modal operator’ to describe such structures. On the one hand, Tarski has given a topological interpretation of a modal operator ‘necessity’, by considering the operator on the Boolean algebra $P X$ which maps a subset to its interior with respect to some given topology on $X$; such interior operators are the same as left exact comonads on $P X$. (See for instance the paper by Awodey-Kinisha.) On the other hand, Lawvere claims that a Lawvere-Tierney topology, that is a left exact internal monad on $\Omega$, or (on a categorified level) a left exact idempotent monad on the ambient topos $E$, should be construed as a modal operator $j$ where truth of $j\phi$ is read as saying ‘$\phi$ is true locally’ (where the meaning of ‘local’ depends on the Lawvere-Tierney topology chosen). It’s clear that I’m trying to consider an abstract common (categorified) generalization that covers these cases, but at present I haven’t assembled more convincing arguments for why ‘modal operator’ is a good term. Maybe it is, maybe it isn’t…

I’m happy to hear other suggestions, of course. I seem to recall that modal operators as defined here bear some broad resemblance to the notion of “interpolad” due to Koslowski, but I have not studied this work. $\Box$

Here then is our fundamental three-in-one theorem:

Theorem 2: Let $(G, \delta)$ be a strict modal operator on a topos $E$. Then the category of $G$-structures $E_G$ is also a topos.

Proof: This proceeds pretty much the same way as the proof given above for theorem 1. It is straightforward to check that the underlying functor $E_G \to E$, from $G$-structures to $E$, creates and preserves pullbacks if $G$ preserves pullbacks. Thus $E_G$ admits pullbacks, and it admits a terminal object $G 1$ under the strictness assumption; therefore $E_G$ admits all finite limits. In particular, the underlying object in $E$ of the product of two $G$-structures $X$, $Y$ is $X \times_{G 1} Y$.

Power objects in $E_G$ are constructed just as they were in theorem 1. First one constructs an auxiliary map in $E$,

namely the map which classifies the subobject defined by the composite mono

and then as before one defines, for a $G$-structure $(Y, \eta: Y \to G Y)$, a putative power object $P_G(Y)$ in $E_G$, namely the equalizer of the diagram

in $E_G$. One then has the task of proving that this works: that given a $G$-structure $(X, \theta: X \to G X)$, that $G$-structure maps are in natural bijection with $G$-structure subobjects of $X \times_{G 1} Y$, the product of $X$ and $Y$ in $E_G$. At the risk of some redundancy (by essentially repeating earlier arguments), let’s run through this now.

Lemma 3: Let $G: E \to E$ be a modal operator, and $(S, \gamma: S \to G S)$ a $G$-structure. Then a mono in $E_G$ targeted at $(S, \gamma)$ is given precisely by a mono $k: R \to S$ in $E$ which fits into a pullback square of the form

Proof: A morphism $k$ in $E_G$ is monic if and only if its underlying morphism in monic in $E$, because the underlying functor $E_G \to E$ creates and preserves pullbacks and therefore monos.

So let $k: R \to S$ be a mono in $E$, and suppose (9) is a pullback square. The map $\beta: R \to G R$ is uniquely determined since $G k$ is monic, and we claim it defines a $G$-structure on $R$. Indeed, we have a diagram

where the right-hand square is a pullback by assumption and the fact that $G$ preserves pullbacks. Therefore, to show the left-hand square is a pullback, it suffices to show the composite square is a pullback. But this composite is the same as the composite square for the diagram

in which both squares are pullbacks. Thus $\beta: R \to G R$ indeed defines a $G$-structure, and commutativity of (9) says $k$ is a $G$-structure map. Thus one direction of the lemma is established.

For the other direction, suppose that (9) defines a monomorphism of $G$-structures. We must show (9) is a pullback. For this, suppose we have a commutative square

First, we prove that $f$ equalizes the pair $\delta R, G\beta: G R \to G G R$. We have a series of equations

using, in turn, (9) (and functoriality of $G$), (10), the coassociativity on the $G$-structure $S$, (10) again, and naturality of $\delta$. Comparing the first and last terms of this series, and using the fact that $G G k$ is monic, we obtain $\delta R \circ f = G\beta \circ f$.

Thus $f$ factors through the equalizer $\beta: R \to G R$ of $\delta R, G \beta: G R \stackrel{\to}{\to} G G R$. Write $f = \beta \circ p$. We then have

and since $\gamma$ is monic, we infer that $k \circ p = g$. Moreover, this $p$ is unique since $k$ is monic. Thus, we have shown that any square (10) factors uniquely, via the map $p: X \to R$, through the square (9); this completes the proof of lemma 3. $\Box$

Now we resume the proof of theorem 2; it remains to show that the equalizer $j: P_G(Y) \to G P Y$ of the pair of maps in (8) is the power object of the $G$-structure $(Y, \eta: Y \to G Y)$. Let $(X, \theta: X \to G X)$ be a $G$-structure, and $f: X \to P_G(Y)$ a $G$-structure map. Then $g = j f: X \to G P Y$ equalizes the maps in (8).

Let $h: X \to P Y$ be the composite

Then we have

where the first equation is the equalizing condition on $g$, the second uses the fact that $g$ is a $G$-structure map, and the third uses functoriality of $G$. Hence $g$ is retrievable from $h$. In fact, the mapping

defines a bijection between maps $g$ satisfying the equalizing condition and maps $h: X \to P Y$ such that

The map $h$ classifies a subobject $i: R \hookrightarrow X \times Y$ in $E$, and we need to check that condition (11) on $h$ corresponds precisely to the condition that $R$ is a sub-$G$-structure of $X \times_{G 1} Y$. Or, taking into account lemma 3: precisely to the condition that there is a pullback diagram of the form

where $\gamma$ is the $G$-structure on $X \times_{G 1} Y$, and $k$ is monic.

Proof: The condition is that the subobject $i: R \hookrightarrow Y \times X$ equals the subobject classified by the composite given in (11):

The subobject classified by $\phi \circ G h: G X \to P G Y$ appears as the left-hand column in

Then, the condition is that postcomposing $\phi \circ G h$ by $P\eta$ and precomposing with $\theta$, the subobject of $Y \times X$ classified by $P\eta \circ \phi \circ G h \circ \theta$, which is obtained by further pulling back as below, should match the subobject $i: R \hookrightarrow Y \times X$, as in the left-hand column below:

This condition amounts saying that the top left square is a pullback (and that $i: R \to Y \times X$ factors through the inclusion $Y \times_{G 1} X \hookrightarrow Y \times X$), since the other three squares are obviously pullbacks already if $G$ preserves pullbacks. That the top left square is a pullback is tantamount to having a pullback (through which the top left square factors)

precisely as in (12). Thus the proof of theorem 2 is complete. $\Box$

To tie up some loose ends, we should check that theorem 2 really does specialize to the pullback-preserving comonad theorem and the lex idempotent monad theorem. In other words, we should check that $G$-structures really are the same things as $G$-coalgebras or $G$-algebras, where $G$ is either a pullback-preserving comonad or a lex idempotent monad, seen as a modal operator.

First, suppose $G$ is a pullback-preserving comonad. We have already seen that a $G$-coalgebra $(X, \eta: X \to G X)$ satisfies the $G$-structure axiom. Converse, if $(X, \eta: X \to G X)$ is a $G$-structure, then it is also a $G$-coalgebra: all we have to do is verify the equation

Since we have a pullback

we know $\eta$ is monic by lemma 0, so it suffices to show $\eta = \eta \circ \varepsilon X \circ \eta$. But we have

using naturality of $\varepsilon$, the counit axiom for comonads, and commutativity of (13). Finally, since $\delta$ is monic, we have $\eta = \eta \circ \varepsilon X \circ \eta$, as was to be shown.

Next, let $G$ be a lex idempotent monad, and define $\delta: G \to G G$ to be $u G$. Here we have a commuting coassociativity square for $\delta$ which consists of isomorphisms and is therefore a pullback, so $(G, \delta)$ is a modal operator. Also, for a $G$-algebra $(X, \alpha: G X \to X)$, the map $\alpha$ is an isomorphism, and so here algebra structure boils down to a condition that the unit $u X: X \to G X$ is invertible (and then $\alpha = (u X)^{-1}$). It is then automatic that $\eta = u X: X \to G X$ satisfies the $G$-structure pullback condition (again since all arrows in the coassociativity square (13) are isomorphisms).

In the other direction, if $(X, \eta: X \to G X)$ is a $G$-structure, then the naturality square

factors through the pullback (13) via a unique map $i: X \to X$, and since $\eta$ is an isomorphism in this case, we must have $i = 1_X$, whence also $\eta = u X$. Thus $u X$ is an isomorphism, so that $X$ is a $G$-algebra. In other words, the category of $G$-algebras for a lex idempotent monad $G$ is equivalent to the category of $G$-structures where $G$ is viewed as a modal operator.

Finally, it is clear that $1$ is a $G$-algebra, hence the $G$-algebra map $G 1 \to 1$ is an isomorphism. Hence $G 1$ is terminal in $E_G$, so that $G$ is strict.

• More generally, any lex monad $G: E \to E$ defines a modal operator if we put $\delta = u G: G \to G G$, and, as above, any $G$-algebra is a $G$-structure. But $G$-structures need not be $G$-algebras. Indeed, $G$-structures coincide with algebras over the idempotent monad $J_G: E \to E$ associated with $G$, where $J_G \hookrightarrow G$ is defined to be the equalizer of the pair of transformations
  $$u G, G u: G \stackrel{\to}{\to} G G$$

Application of theorem 2, and further results

We have seen that pullback-preserving comonads and left exact idempotent monads (equivalently, pullback-preserving idempotent monads) are examples of modal operators. In order for the notion of modal operator to be a really viable concept, however, we should give some other interesting examples which fall outside these two classes. We should also make good on our promise to present the fundamental passage, from a topos $E$ to the topos of sheaves on an internal site in $E$, in a single step (more precisely, a single application of theorem 2).

These goals are interconnected: we will construct, given an internal site $(C, j)$ in $E$, a (strict) modal operator $G: E \to E$ such that the category of sheaves $Sh(C, j)$ is equivalent to the category of $G$-structures. This $G$ is neither a pullback-preserving comonad nor a lex idempotent monad; it’s a hybrid which supports the viability of our notion of modal operator.

Indeed, it isn’t hard to imagine how this works. First, we have a two-step passage

where $U: E^{C^{op}} \to E$ assigns to each presheaf its underlying “set” (object) of elements, and $G$ is right adjoint to $U$; the comonad $U G: E \to E$ was the one used to describe $E^{C^{op}}$ as the category of coalgebras in the application of theorem 1. The functor $a: E^{C^{op}} \to Sh(C, j)$ is the associated sheaf functor, and $i$, its right adjoint, is the underlying functor from sheaves to presheaves. The composite $J = i a$ is a lex idempotent monad whose category of algebras is $Sh(C, j)$, and naturally theorem 2 guarantees that $Sh(C, j)$ is a topos, given that $E^{C^{op}}$ is.

Suppose we traverse the full circuit of arrows from $E$ back to itself, giving rise to an operator

This $K$ is a hybrid formed from the comonad $U G$ and the monad $J = i a$, but is neither a comonad nor a monad itself. It is, as we shall see, a (strict) modal operator on $E$, such that $Sh(C, j)$ is equivalent to the category of $K$-structures! This is the denouement we were waiting for: it shows that the passage from sets to sheaves is really a one-step process, if we choose the modal operator on sets right.

The entire discussion is concentrated in theorem 3 below, after a few preliminaries. Let $E$ be finitely complete, and let $G: E \to E$ be a modal operator. For each $G$-structure $(Y, \eta): Y \to G Y$, the map $\eta$ is a map of $G$-structures. Thus, if $U: E_G \to E$ denotes the underlying functor and $G: E \to E_G$, by slight abuse of notation, denotes the evident functor $X \mapsto G X$, then we have a natural transformation

Of course, this isn’t generally a unit of an adjunction or anything like that, but much of the power of modal operators derives from a fact which is the essential point of lemma 3 above: that $\eta$ is cartesian with respect to monos. We take advantage of this fact repeatedly.

If furthermore $(H, \delta)$ is a modal operator on $E_G$, then we have a round trip operator

and we define a transformation $\lambda: K \to K K$ in the only reasonable way possible: as the composite

Theorem 3: $(K, \lambda)$ defines a modal operator on $E$, and $E_K \simeq (E_G)_H$. If the modal operators $G$ and $H$ are strict, then so is $K$.

Proof: A completely detailed proof involves some largish diagrams, but we sketch the essential points. To prove $K$ is a modal operator, we need to contemplate a diagram of shape

where all four squares are pullbacks by more or less the same argument, which we give just for the square labeled (4): this square is obtained by applying the pullback-preserving functor $U H$ (at the argument $H G$) to the square

which is a pullback by lemma 3 ($H\eta$ is monic, and the transformation $\eta$ is cartesian with respect to monos). This completes the sketch for why $K$ is a modal operator.

Now we sketch the equivalence $(E_G)_H \simeq E_K$. In one direction, it is relatively easy to define a functor $(E_G)_H \to E_K$. For consider an object of $(E_G)_H$. This consists of an object $X$ of $E$ together with structures

(where $h X$ denotes the underlying object in $E$ of the value of $H$ applied to the $G$-structure $(X,\eta)$), subject to various pullback conditions. Observe that $\eta$ may be regarded as a map in $E_G$; by applying $H: E_G \to E_G$ to it, we obtain a map

and hence a composite

which is a map $\zeta: X \to K X$ which defines a putative $K$-structure. Indeed, in $E$ we have a diagram of the form

where (1) is a pullback because $\theta$ is the underlying map of an $H$-structure, (2) is a pullback because $h\eta$ is a monic $H$-structure map (then use lemma 3), (3) is a pullback because $H$ preserves pullbacks and $\theta$ is also a monic $G$-structure map (lemma 3 again), and (4) is a pullback because $H$ preserves pullbacks and $h\eta$ is a monic $G$-structure map.

In the other direction, we now define a functor $E_K \to (E_G)_H$. This is a bit trickier; the main hurdle to overcome is to produce a $G$-structure $\eta: X \to U G X$ from a $K$-structure $\zeta: X \to U H G X$. In summary, the pullback of a diagram having the form

is $X$ (with both pullback projections being $\zeta: X \to h G X$), by taking advantage of the pullback axiom on the $K$-structure $\zeta$ together with naturality of $\eta$. If we leave off the leftmost and topmost map from this diagram, we get a diagram

whose pullback is $U G X$ (with both pullback projections being $U G\zeta$), by the pullback condition on $\zeta$ and the fact that $U G$ preserves pullbacks. Thus the first pullback $X$ factors through the second pullback $U G X$, by a map I shall again call $\eta: X \to U G X$. It may be checked that this makes $X$ a $G$-structure. From all this we get a pullback

so that $\zeta: X \to h G X$ is a $G$-structure map, and it will be so regarded. Thus, we interpret this pullback square as lifted up to the category $E_G$, and we hit it with the pullback-preserving functor $h = U H$. The result is the square appearing in the diagram

and the pullback of the right-hand column against the bottom map is, by the $K$-structure axiom, $X$ with both pullback projections being $\zeta: X \to U H G X$. Thus we arrive at a diagram

in which $\zeta = h\eta \circ \theta$. It may be checked that $\theta$ defines an $H$-structure in $E_G$, and this concludes our sketch of the equivalence $E_K \simeq (E_G)_H$.

Finally, if the modal operators $G$ and $H$ are strict, then $G 1$ is terminal in $E_G$, and then $H G 1$ is terminal in $(E_G)_H \simeq E_K$. Since $K 1 = H G 1$ is terminal in $E_K$, it follows that $K$ is strict. This concludes the proof of theorem 3. $\Box$

Theorem 3 gives one means of constructing new modal operators from old.

Acknowledgments

I thank Sridhar Ramesh and Mike Shulman for pointing out that Theorem 1 appears in print in Johnstone’s Elephant, and Mike for many thoughtful comments on a draft of this article, in particular for pointing out the closely related work by Toby Kenney on toposes constructed by means of diads [reference to be inserted].