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.
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.
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).
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.
If $G: E \to E$ is a pullback-preserving comonad acting on a topos $E$, then the category of coalgebras $E_G$ is also a topos.
It suffices to produce finite limits and power objects in $E_G$. Pullbacks in $E_G$ are created by the forgetful functor $E_G \to E$ because $G$ preserves pullbacks, and $G 1$ is terminal in $E_G$ if $1$ is terminal in $E$, since the right adjoint $G-: E \to E_G$ preserves limits. So $E_G$ is finitely complete.
Since $G: E \to E$ preserves pullbacks, it also preserves monos. In particular, if $\in_Y \hookrightarrow Y \times P Y$ denotes the elementhood relation between $Y$ and its power object $P Y$ in $E$, we have a chain of monos
where the middle two objects are pullbacks of the diagram
in $E$. The composite of the monos in (1) names a subobject of $G Y \times G P Y$, which is classified by a map
in $E$.
Let $\delta: G \to G G$ denote the comultiplication and $\varepsilon: G \to 1_E$ the counit of $G$, and suppose $Y$ carries a $G$-coalgebra $\eta: Y \to G Y$. Define the object $P_G Y$ in $E_G$ to be the equalizer in $E_G$ of the following pair of coalgebra maps from the cofree coalgebra $G P Y$ to itself:
where $P$ is the contravariant power object functor (whence the direction $P \eta: P G Y \to P Y$). We will show that $P_G Y$ is the power object of $Y$ in $E_G$.
So, let $(X, \theta: X \to G X)$ be a coalgebra. We must show that coalgebra maps $f: X \to P_G Y$ correspond precisely to subcoalgebras of the product $X \times Y$ in $E_G$ (whose underlying object in $E$ is the pullback $X \times_{G 1} Y$). The remainder of the proof will be proven with the help of three lemmas.
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.
In any commutative square
the arrows $f$, $g$ coincide because $G \gamma$ and $\delta S$ have a common left inverse $G\varepsilon S: G G S \to G S$. Therefore the pullback of the arrows $G\gamma$, $\delta S$ is the same as their equalizer, which is $\gamma: S \to G S$. For the second sentence, the condition that the two pullback projections coincide is equivalent to the condition that the projection is the equalizer, and equalizers are monic.
Suppose $G: E \to E$ is a comonad which preserves pullbacks, and let $(S, \gamma: S \to G S)$ be a $G$-coalgebra. Then a pair $(k: R \to S, \beta: R \to G R)$ defines a subcoalgebra of $S$ precisely when $k$ is monic and the compatibility square
commutes.
First, $G k$ is monic assuming $k$ is monic, since $G$ preserves pullbacks. Therefore $\beta$ is uniquely determined. We must show that $\beta: R \to G R$ satisfies the axioms for a coalgebra structure, i.e., that
Since $k$ is monic, the second equation follows from the equation
but this equation holds since
using in turn naturality of $\varepsilon$, the square (3), and the fact that $S$ is a coalgebra.
Again, $G$ preserves pullbacks, so $G G k$ is monic assuming $k$ is. So the first equation of (4) follows from
and this last equation is left to the reader; it follows from naturality of $\delta$, the square (3), and the fact that $S$ is a coalgebra.
In the notation of lemma 1, if $k: R \to S$ is a monic coalgebra map, then the square
is a pullback.
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, (5) (and functoriality of $G$), (6), the coassociativity on the coalgebra $S$, (6) again, and naturality of $\delta$. Comparing the first and last terms of this series, and using the fact that $G G k$ is monic (because $k$ is monic and $G$ preserves pullbacks), 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 (cf. lemma 0), we infer that $k \circ p = g$. Moreover, this $p$ is unique since $k$ is monic. Thus, we have shown that any square (6) factors uniquely, via the map $p: X \to R$, through the square (5); this completes the proof.
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.
That $g: X \to G P Y$ equalizes the pair of maps in (2) translates to a condition on $h: X \to P Y$, that the following diagram commutes:
Or, that the subobject $i: R \hookrightarrow Y \times X$ equals the subobject classified by
First, remembering how $\phi$ was defined, 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 (7). Thus the proof of theorem 1 is complete.
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.
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:
A modal operator $(G, \delta)$ is strict if
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
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
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.
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.
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].