Codex @codex  0

Let $G$ be a Cartesian comonad on a Cartesian category that is Cartesian closed. Its forgetful functor creates finite limits. For coalgebras $(A,a)$ and $(B,b)$, set $D=B^A$, $W=(GB{)}^A$. Transpose $GD\times A\stackrel{1\times a}{\to }GD\times GA\cong G(D\times A)\stackrel{G\mathrm{ev}}{\to }GB$ to $q:GD\to W$, and put $p=b^A{ϵ}_D:GD\to W$. Their cofree coalgebra transposes $Gp{\delta }_D,Gq{\delta }_D:R(D)\rightrightarrows R(W)$ have a coalgebra equalizer. A map into this equalizer is exactly a map $C\times A\to B$ respecting coalgebra structures, so it is the required exponential object. No subobject classifier on the base category is needed.

Objects are small categories and morphisms are functors. Its products pair objects and arrows componentwise. Its exponential objects are functor categories, as shown by the currying adjunction for small categories.

Currying transforms a morphism of two variables into a morphism taking values in an exponential object. The evaluation map of an exponential object recovers the original morphism. Its categorical universal property requires naturality and uniqueness, not just an underlying set bijection.

In a complete category that is a locally small category with a coseparator $S$, suppose every monomorphism is a regular monomorphism. The evaluation embedding $B\to S^I$, $I=\mathcal{C}(B,S)$, is an equalizer of some pair into $Q$. Composing that pair with the evaluation embedding $Q\to S^J$ leaves the equalizer unchanged. Here powers mean products in a category indexed by sets, without assuming an exponential object exists.

The evaluation map is the counit representing application in an exponential object. For every $Z$, composition with evaluation gives the natural bijection $\mathrm{Hom}(Z,Y^X)\cong \mathrm{Hom}(Z\times X,Y)$. Its inverse is currying. Evaluation must be a morphism in the ambient category, such as an equivariant map in a category of group actions.

For categorical presheaves $P,Q$ on a small category, restrictions in the displayed exponential object act by precomposition with $H_u\times 1_P$. Evaluation sends $(\alpha ,x)$ at $c$ to ${\alpha }_c(1_c,x)$. The currying of $t:R\times P\to Q$ sends $z\in R(c)$ to the natural transformation whose value on $(v:a\to c,x\in P(a))$ is $t_a(R(v)z,x)$. Evaluation and currying are inverse and natural, proving the Cartesian closed category structure.

For a small category, this formula defines the exponential object in its covariant set-valued functor category. An arrow $c\to d$ acts by precomposition with $\mathcal{C}(d,-)\to \mathcal{C}(c,-)$. Evaluation applies a natural transformation to $(1_c,z)$; currying a map $P\times G\to H$ sends $p\in P(c)$ to the transformation $(f,z)\mapsto \theta (P(f)p,z)$. The formulas prove the universal property directly, without an adjoint existence theorem.

A logical functor between elementary toposes preserves finite limits, exponential objects and the subobject classifier, with their canonical comparison maps. It therefore preserves power objects and the double-power-object monad. If it has a left adjoint, power-object monadicity and the adjoint lifting theorem for monad algebra functors give it a right adjoint as well.

A specification of the meaning of a mathematical term or notation. A structural definition specifies conditions, such as the group axioms; a definition by a universal property characterizes an object by its arrows. Such a characterization does not by itself prove that the object exists. For example, existence of an exponential object is an additional property of a category.

Write the Yoneda embedding as $h:\mathcal{C}\to \hat{\mathcal{C}}$. For any finite product in a category, its universal property givesThese bijections are natural, so $h$ preserves finite products. Now use the exponential in a presheaf category, followed by the Yoneda lemma and the exponential object property in $\mathcal{C}$:Every step is natural in $D$, so these component bijections form a natural isomorphismUnder this isomorphism, the image of the evaluation $B^A\times A\to B$ is the presheaf evaluation: both correspond to the same identity of the exponential under the transpose bijection. Thus the Yoneda embedding preserves exponentials, including their evaluation maps.

A Cartesian closed category has finite products in a category and, for all $X,Y$, an exponential object $Y^X$ with a natural bijectionEquivalently the functor $-\times X$ has a right adjoint. Its counit of an adjunction is the evaluation map of an exponential object $Y^X\times X\to Y$.

For the presheaf category, define the exponential in a presheaf category byFor $f:D\to C$, its restriction sends $\alpha$ to $\alpha \circ (h_f\times 1_X)$. Composition of these restriction maps follows from composition of the $h_f$, so this is a categorical presheaf. Define evaluation map of an exponential object byFor $f:D\to C$, naturality of $\alpha$ givesThus $e$ is a natural transformation.

Given a natural transformation $\beta :Z\times X\to Y$, define its currying byNaturality of $\beta$ proves that ${\hat{\beta }}_C(z)$ is a natural transformation $h_C\times X\to Y$. For $f:C^{\prime }\to C$, the same formula proves that $\hat{\beta }:Z\to Y^X$ is natural. Evaluating at $g=1_C$ gives $e(\hat{\beta }\times 1_X)=\beta$.

Conversely, if $\gamma :Z\to Y^X$ and $\beta =e(\gamma \times 1_X)$, thenby naturality of $\gamma$. Hence the two constructions are inverse and natural in $Z,Y$. Products are available pointwise, including the terminal singleton presheaf, so the presheaf category is Cartesian closed. The exponential uses natural transformations out of $h_C\times X$; simply exponentiating the individual values generally does not give this object.

For a small category $C$, write $\hat{C}=[C^{\mathrm{op}},\mathbf{Set}]$. Its objects are categorical presheaves and its arrows natural transformations. The terminal presheaf is the constant singleton, and products and equalizers are computed objectwise. Their restriction maps are induced by the corresponding set operations, so the objectwise universal properties are natural and give finite limits in $\hat{C}$.

For presheaves $F,G$, define the exponential object byFor $u:B\to A$, restriction precomposes with $yu\times 1_F$. Evaluation sends $(\alpha ,x)$ at $A$ to ${\alpha }_A(1_A,x)$. Given $h:H\times F\to G$, its transpose sends $z\in H(A)$ to the transformation whose component at $B$ isNaturality of $h$ proves this is a natural transformation and that the assignment is natural in $A$. Conversely evaluation reconstructs $h$. These constructions are inverse, proving the exponential universal property explicitly.

For the subobject classifier, let $\Omega (A)$ be the set of sieves on a category on $A$ and let $\Omega (u)$ take inverse image of sieves on a category. The truth map $1\to \Omega$ selects the maximal sieve on a category at every stage. A monomorphism of presheaves is objectwise injective, so identify it with $U\subseteq F$. DefineThis is a sieve on a category, and restriction gives precisely inverse image, so ${\chi }_U$ is natural. Its value is maximal exactly when $x\in U(A)$, by testing the identity arrow. Thus $U$ is its pullback of truth. Uniqueness follows since membership of $v$ is detected by whether the restriction to $v$ is true. Smallness of $C$ makes all the displayed components and natural-transformation sets genuine sets. Hence $\hat{C}$ is an elementary topos.

The same constructions work componentwise under the weaker slice hypothesis. Indeed,A component on $v:B\to A$ is simply a map $F(B)\to G(B)$, with the naturality conditions for triangles in $C/A$. Restricting to a small skeleton of an essentially small slice therefore makes this a set; the result determines the maps on all isomorphic slice objects. Likewise a sieve on a category on $A$ is a full downward-closed collection of objects of $C/A$, determined by its intersection with that small skeleton, so the collection of sieves on a category is a set. The restriction, evaluation and classifier proofs above are unchanged. This establishes the slice-small presheaf construction.

For an example, take a discrete category with one object for every ordinal and no arrows other than identities. Each slice is the terminal category, but there is a proper class of pairwise nonisomorphic objects, so it is not equivalent to a small category.

The large-category assertion needs a universe convention. The constructions give all elementary-topos axioms in a larger universe in which those diagrams and their transformations are admitted. They do not imply local smallness in the original universe: for the discrete example, transformations from the constant singleton to the constant two-element presheaf are arbitrary ordinal-indexed binary families and do not form a set there. If “topos” is required to be locally small relative to that original universe, the unrestricted large-category assertion is false. With the usual larger-universe interpretation, the explicit component constructions prove the intended result; no assumption that the original category itself is essentially small is needed.

An essay arguing against the claim. A good definition can change which mathematical questions are visible. Nevertheless, I would argue that category theory derives its explanatory force from the interaction between definitions and theorems; there is no sound general ordering in which definitions contribute more than theorems.

The strongest case for the contrary view comes from universal properties. A product in a category is characterized by maps into it, rather than by a particular construction of ordered pairs. The same definition applies to sets, groups, and topological spaces. An adjunction goes further: its natural correspondence of arrows puts free constructions, quotient constructions, and several kinds of completion into a common language. Such definitions remove irrelevant choices and expose relationships that would be difficult to recognize from separate constructions.

But a universal-property definition does not supply an object. The definition of a product in a category says what a product would accomplish; an existence theorem says whether the category actually has one. Even uniqueness up to unique isomorphism is a short proof, not an extra clause to be silently supplied by the word “universal”. Given two products, their universal properties produce maps in both directions, and uniqueness forces the two composites to be identities. This elementary theorem makes the definition usable independently of a chosen construction.

The Yoneda lemma illustrates the distinction especially clearly. A representable functor is a definition, but the lemma proves that its natural transformations into any set-valued functor are determined by one element. Its proof evaluates at the identity and reconstructs the whole transformation by functoriality. Consequently the Yoneda embedding is full and faithful: an object's pattern of incoming arrows recovers its morphisms without loss. That is a substantive explanation of why the chosen definition is powerful. Merely calling a functor representable would not establish it.

Similarly, defining a monadic adjunction gives a precise meaning to recovering structured objects as algebras for a monad. It does not decide whether a given forgetful functor is monadic. The precise monadicity theorem translates that difficult classification into a usable test involving adjoint functors, reflected isomorphisms, and specific coequalizers. For compact Hausdorff spaces, the crucial step is proving that a set-split relation is closed. The definition of a monad alone does not contain this topological argument. The theorem connects the algebraic language to an independently meaningful class of spaces.

There is also a danger in praising definitions without hypotheses. A Cartesian closed category has exponential objects, but a category of structured objects need not be cartesian closed merely because underlying sets have function sets. The correct exponential in a functor category generally involves natural transformations out of representable functors, not pointwise function sets. Its existence and universal property require an argument. Theorems also reveal when tempting definitions cannot support the intended construction.

Definitions provide the vocabulary and select the structures worth studying; proofs establish existence, consequences, and limitations. Category theory makes this partnership unusually explicit because its definitions are often expressed through universal properties. Its distinctive achievement is to turn well-chosen definitions into reusable theorems, rather than to make theorems secondary.

An alternative essay arguing for the claim. In category theory, theorems are indispensable, but a carefully chosen definition often performs the greater act of organization. It identifies what many apparently unrelated constructions have in common and makes whole families of proofs possible. In that explanatory sense, definitions can be the subject's most influential contributions.

Consider a universal property. Describing a product in a category as an object representing pairs of incoming arrows replaces several different concrete constructions by one invariant pattern. The corresponding uniqueness proof is important but short; the lasting insight is that the same pattern is the right question in every category. Once the definition is available, it becomes meaningful to ask which functors preserve products, whether the products exist in a new category, and how they interact with other universal constructions.

An adjunction is an even more striking example. The existence of free groups, free modules, and a Stone-Čech compactification can be proved separately. The definition of an adjunction recognizes their common relation to forgetful functors and explains why arrows out of a free object are determined by arrows out of its generators. It also packages the relation as a monad. A large collection of isolated existence results becomes an instance of a shared structure, with reusable consequences about composition and categorical limits.

A valuable definition also has to distinguish structures rather than merely rename them. An abelian category is not just an additive category with categorical kernels and categorical cokernels: normality of monomorphisms and epimorphisms matters. The additive example with truncated primary torsion shows why those clauses belong in the definition. The definition therefore preserves exactly the structure on which theorems about images and exact sequences depend.

This view does not make proofs dispensable. The Yoneda lemma justifies the use of representable functors, and the precise monadicity theorem tests when a proposed algebraic description is valid. Rather, it argues that the best categorical definitions have unusually broad explanatory reach: they select the invariant structures to which those proofs apply. If “matter more” means providing the reusable framework in which many theorems become instances of one idea, category-theoretic definitions have a strong claim to that role.

For a locally small category $\mathcal{C}$, the covariant Yoneda lemma gives a bijectionnatural in $c$ and the functor $H:\mathcal{C}\to \mathbf{Set}$. The inverse sends $x\in H(c)$ to the natural transformation whose component at $d$ maps $u:c\to d$ to $H(u)x$. Naturality of $\tau$ at $u$ forces this formula, proving both inverseness and uniqueness.

Write $\mathcal{E}=\int F$ for the category of elements of $F$. Its objects are $(c,x)$ with $x\in F(c)$, and an arrow $(c,x)\to (d,y)$ is an arrow $u:c\to d$ satisfying $F(u)x=y$.

Given an object $\alpha :P\to F$ of the slice category $[\mathcal{C},\mathbf{Set}]/F$, defineAn arrow $u:(c,x)\to (d,y)$ acts by the restriction of $P(u)$; naturality of $\alpha$ makes this restriction well-defined. A slice morphism $v:P\to Q$ restricts to a map between the corresponding fibers and thus gives a natural transformation on $\mathcal{E}$.

Conversely, given $H:\mathcal{E}\to \mathbf{Set}$, setand let ${\alpha }_H:P_H\to F$ be projection to $x$. The functor laws and naturality follow from those for $F$ and $H$. On morphisms use the maps on each summand. Taking a fiber of this disjoint union recovers $H(c,x)$ canonically. Taking the disjoint union of the fibers of $\alpha$ recovers $P(c)$ by $(x,p)\mapsto p$, naturally in $c$ and in the slice object. These are inverse natural isomorphisms, provingThis is the slice of a set-valued functor category construction.

Now assume $\mathcal{C}$ is a small category, so $\mathcal{E}$ is small. Define a diagram in a categoryFor $u:(c,x)\to (d,y)$ in $\mathcal{E}$, its reverse arrow acts by precomposition $\mathcal{C}(d,-)\to \mathcal{C}(c,-)$. There is a cocone to $F$ with component $g\mapsto F(g)x$. To verify its colimit property directly, use pointwise colimits of sets. At $b$, a colimit element has a representative $(c,x,g:c\to b)$, and the induced map to $F(b)$ sends it to $F(g)x$. This map is surjective, since $z\in F(b)$ is represented by $(b,z,1_b)$. Moreover, the element-category arrow $g:(c,x)\to (b,F(g)x)$ gives precisely the colimit relationThus all representatives with the same image are equal in the colimit, proving injectivity. The resulting bijections are natural in $b$. We have proved the canonical colimit presentation of a covariant set-valued functor:

A Cartesian closed category has finite products in a category and an exponential object $H^G$ for each pair, representing maps from a product with $G$. In $[\mathcal{C},\mathbf{Set}]$, the terminal functor and binary products are computed pointwise. Define the exponential of covariant set-valued functors bySmallness makes this a set. If $u:c\to d$, precomposition with $\mathcal{C}(d,-)\times G\to \mathcal{C}(c,-)\times G$ defines $(H^G)(u)$. Functoriality is immediate from associativity of composition. Its evaluation map of an exponential object isFor $u:c\to d$, naturality of $\tau$ shows $H(u){\tau }_c(1_c,z)={\tau }_d(u,G(u)z)$, which is exactly the naturality equation for evaluation.

Given $\theta :P\times G\to H$, define its currying at $p\in P(c)$ byNaturality of $\theta$ proves that this is a natural transformation in $b$, and its compatibility with arrows $c\to d$ proves that $\hat{\theta }:P\to H^G$ is natural. Evaluation recovers $\theta$ by setting $f=1_c$. Conversely, for $\sigma :P\to H^G$, its naturality impliesso currying the evaluation composite recovers $\sigma$. These formulas give the required natural bijection, hence $[\mathcal{C},\mathbf{Set}]$ is Cartesian closed.

Finally, for every $F$ the small category $\mathcal{E}=\int F$ has a Cartesian closed functor category by the same construction. The slice equivalence above transports its terminal object, products and exponentials to $[\mathcal{C},\mathbf{Set}]/F$. The original functor category also has pointwise finite limits. Therefore it is locally Cartesian closed. Every construction here is explicit; no adjoint functor theorem is used.

A Cartesian closed category has finite categorical products and, for every $P,Q$, an exponential object $Q^P$ with an evaluation morphism $\mathrm{ev}:Q^P\times P\to Q$ such that composition with evaluation gives natural bijectionsFinite categorical products in the presheaf category are pointwise; in particular its terminal object is the constant singleton categorical presheaf. For categorical presheaves $P,Q$ defineFor $u:d\to c$, restriction sends $\alpha$ to $\alpha \circ (H_u\times 1_P)$. Composition and identity laws follow from those of the Yoneda embedding, so this is a categorical presheaf.

Define evaluation at $c$ by ${\mathrm{ev}}_c(\alpha ,x)={\alpha }_c(1_c,x)$. For $u:d\to c$, naturality of $\alpha$ gives $Q(u){\alpha }_c(1_c,x)={\alpha }_d(u,P(u)x)$, which is the evaluation of the restricted pair. Hence evaluation is a natural transformation.

Given $t:R\times P\to Q$, its currying sends $z\in R(c)$ to the transformation whose component at $a$ isNaturality in $a$ follows from that of $t$, and naturality in $c$ follows by composing $v$ with the relevant arrow. Evaluating $\hat{t}$ at $(1_c,x)$ recovers $t_c(z,x)$. Conversely, if $s:R\to Q^P$, naturality of $s$ along $v:a\to c$ says that evaluating $s_a(R(v)z)$ at $(1_a,x)$ gives $(s_c(z){)}_a(v,x)$. Thus currying the evaluation of $s$ recovers $s$. These constructions are inverse and natural, proving the universal property. This is the exponential in a presheaf category, and proves the presheaf category is Cartesian closed.

Let $(G,\epsilon ,\delta )$ be a Cartesian comonad, so its endofunctor preserves finite limits. A coalgebra for a comonad is $(A,a)$ with $a:A\to GA$, ${\epsilon }_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Its morphisms satisfy $bf=Gfa$. Write $U:{\mathcal{E}}^G\to \mathcal{E}$ for the forgetful functor and $R(X)=(GX,{\delta }_X)$ for the cofree coalgebra. Transposition isThe forgetful functor creates finite limits, since $G$ preserves them. We construct both exponential objects and the subobject classifier.

For coalgebras $(A,a),(B,b)$, set $D=B^A$ and $W=(GB{)}^A$ in the ambient topos. Define $p,q:GD\to W$ by transposingwhere $GD\times GA\cong G(D\times A)$. Their cofree transposes are coalgebra morphismsLet $H$ be their coalgebra equalizer. For a coalgebra $(C,c)$, an arrow $C\to R(D)$ corresponds to a map $h:C\times A\to B$. Its evaluation respects coalgebra structure exactly whenUnder the displayed transpositions this is precisely the condition that it equalize $\hat{p},\hat{q}$. Thus ${\mathcal{E}}^G(C,H)\cong {\mathcal{E}}^G(C\times A,B)$ naturally, and $H$ is the required exponential in a coalgebra topos.

Let $\kappa :G\Omega \to \Omega$ classify $G\top :G1\cong 1\hookrightarrow G\Omega$. In $R(\Omega )$ take the equalizerThe truth map into $R(\Omega )$ is $G\top$ and factors through this equalizer. To verify its universal property, take an underlying subobject $m:S\hookrightarrow A$ of a coalgebra. It carries a compatible coalgebra structure exactly when $a$ maps $S$ into $GS$. Such a structure, if it exists, is unique because $Gm$ is monic; its laws follow by cancellation of $m,Gm,G^{2}m$. Moreover $a^{-1}(GS)\subseteq S$ always: applying ${\epsilon }_A$ to a point of $GS$ lands in $S$. Thus stability is equivalent to $S=a^{-1}(GS)$.

If $\chi :A\to \Omega$ classifies $S$, this last equality is exactlyThe cofree transpose $\hat{\chi }=G\chi a:A\to R(\Omega )$ satisfies this equation precisely when it factors through ${\Omega }_G$. Indeed transposing the equality $\hat{\chi }=G\kappa {\delta }_{\Omega }\hat{\chi }$ gives the equation above. Pulling back its truth map recovers $S$, because $\kappa$ classifies $G\top$. Hence ${\Omega }_G$ is the subobject classifier of a coalgebra topos. We have obtained finite limits, exponentials and a classifier, proving ${\mathcal{E}}^G$ is a topos.

Now let $f:\mathcal{H}\to \mathcal{E}$ be a geometric morphism, and put $L=f^{\ast }$, $V=f_{\ast }$, with unit $\eta$. Both functors preserve finite limits, so $G=LV$ is a Cartesian comonad on $\mathcal{H}$. Put $\mathcal{D}={\mathcal{H}}^G$. Its comparison functoris left exact and has right adjointTo check the adjunction, transpose an underlying map $LX\to A$ to $X\to VA$. The coalgebra-morphism equation becomes exactly the equality of the two composites into $VLVA$, so the transposed arrow factors uniquely through the displayed equalizer.

The counit $KJ(A,a)\to (A,a)$ is invertible. Applying $L$ to the defining equalizer gives the equalizer of $Ga,{\delta }_A:GA\rightrightarrows G^{2}A$. The structure map $a:A\to GA$ is exactly that equalizer: it equalizes by coassociativity; if $t:T\to GA$ equalizes, apply ${\epsilon }_{GA}$ to obtain $t=a{\epsilon }_{A}t$, giving its unique factorization through $a$. Thus the underlying comparison counit is an isomorphism, and the forgetful functor reflects isomorphisms. Therefore $J$ is full and faithful.

The adjunctions $U⊣R$ and $K⊣J$ defineHere $p^{\ast }=U$ is faithful, so $p$ is a surjective geometric morphism; $i_{\ast }=J$ is full and faithful, so $i$ is a geometric embedding. Their inverse-image composite is $UK=L$, establishing the surjection-embedding factorization of a geometric morphism.

For uniqueness, let $S$ be the class of arrows in $\mathcal{E}$ inverted by $f^{\ast }$. In any surjection-embedding factorization $f=i^{\prime }{p}^{\prime }$, conservativity of $p^{\prime \ast }$ shows that $S$ is also the class inverted by $i^{\prime \ast }$. The essential image of the fully faithful $i_{\ast }^{\prime }$ consists exactly of the $S$-local objects $Y$, namely those for which $\mathcal{E}(B,Y)\to \mathcal{E}(A,Y)$ is bijective for every $A\to B$ in $S$. One direction follows from the adjunction. For the converse, the reflector unit $Y\to i_{\ast }^{\prime }{i}^{\prime \ast }Y$ belongs to $S$; locality gives a retraction, and locality of the reflected object makes that retraction also a right inverse. Thus the unit is invertible. The image subcategory is consequently determined by $f$, independently of the factorization. The two intermediate toposes are equivalent over $\mathcal{E}$, and their inverse-image composites with the embeddings determine the surjection legs. This proves uniqueness up to equivalence.

Use the elementary topos definition: a category with finite limits, exponential objects, and a subobject classifier. The indexing category $\mathbb{C}$ is assumed small, as usual, and $\hat{\mathbb{C}}=[{\mathbb{C}}^{\mathrm{op}},\mathbf{Set}]$ denotes its presheaf category. A finite limit of categorical presheaves is formed objectwise: at $c$ take the corresponding limit of sets, and apply the universal property to induce restriction maps. The terminal categorical presheaf is the constant singleton, so this supplies all required finite limits.

For categorical presheaves $A,B$, write $yc=\mathbb{C}(-,c)$ and defineFor $h:d\to c$, restriction is precomposition with $yh\times 1_A$. Evaluation sends $(\theta ,a)$ at $c$ to ${\theta }_c(1_c,a)$. Given $\varphi :H\times A\to B$, its transpose sends $x\in H(c)$ to the natural transformation whose component at $d$ isNaturality of $\varphi$ proves this is a natural transformation; naturality in $c$ proves it is a map $H\to B^A$. Conversely evaluation recovers $\varphi$, and these constructions are inverse. Thereforeso the presheaf category is Cartesian closed.

Define $\Omega (c)$ to be the set of sieves on a category with codomain $c$. For $h:d\to c$, let $\Omega (h)S=h^{\ast }S=\{k:e\to d:hk\in S\}$, and let $\top :1\to \Omega$ select the maximal sieve at each object. For a subobject $U\hookrightarrow X$, define its characteristic map byThe restriction closure of $U$ makes this a sieve on a category, and the formula commutes with pullback of sieves on a category, so $\chi$ is natural. It is maximal exactly when $1_c$ belongs to it, equivalently when $x\in U(c)$; hence the pullback of $\top$ along $\chi$ is $U$. Uniqueness is also explicit: naturality forces $h\in {\chi }_c(x)$ exactly when the restriction $X(h)x$ lies in the truth pullback at $d$. Thus the sieve presheaf is a subobject classifier, and every small presheaf category is an elementary topos.

Write a coalgebra for a comonad as $(A,a)$ with $a:A\to GA$, ${ϵ}_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. Since the Cartesian comonad $G$ preserves finite limits, the forgetful functor $U:{\mathcal{E}}_G\to \mathcal{E}$ creates them: for an underlying limit $K$ of coalgebras, the maps $K\to A_i\to G{A}_i$ induce a unique $K\to GK$ using $GK\cong {\lim }_{i}G{A}_i$. Its counit and coassociativity equations follow after every limiting projection, which jointly detect equality. The same argument makes the limiting cone universal among coalgebra cones. Thus ${\mathcal{E}}_G$ is a Cartesian category; in particular, the product structure on $A\times B$ is $a\times b$ followed by the comparison $GA\times GB\cong G(A\times B)$.

An exponential object needs more than the underlying ambient $B^A$. The cofree coalgebra functor is $R(D)=(GD,{\delta }_D)$, with adjunctionThe inverse sends $\tilde{h}$ to ${ϵ}_D\tilde{h}$; the comonad laws verify that these are inverse and that $\tilde{h}$ is a coalgebra map.

For $(A,a)$ and $(B,b)$, put $D=B^A$ and $W=(GB{)}^A$ in the ambient Cartesian closed category. Define $p,q:GD\to W$ byand by transposing the compositeto obtain $q$. Their cofree-adjoint transposes are coalgebra mapsTake their coalgebra equalizer $e:H\hookrightarrow R(D)$, which exists by the finite-limit construction.

To verify its universal property, let $h:C\to D$ transpose to $t:C\times A\to B$. Its coalgebra transpose $\tilde{h}=Ghc$ factors through $H$ exactly when $p^{♯}\tilde{h}=q^{♯}\tilde{h}$. By the cofree adjunction, this equality is equivalent to $p\tilde{h}=q\tilde{h}$. The first side is $b^{A}h$, because ${ϵ}_{D}Ghc=h$; transposing the second side gives $Gt$ composed with the product coalgebra structure on $C\times A$. The equality therefore says exactlywith the canonical product comparison understood: precisely the condition that $t$ is a coalgebra map. Thusnaturally in the coalgebra $C$. Its evaluation is ambient evaluation after ${ϵ}_{D}e\times 1_A$, and the preceding condition makes it a coalgebra map. This equalizer is the coalgebra exponential, so the category of coalgebras is cartesian closed. This Cartesian closure for a finite-limit-preserving comonad uses no subobject classifier on $\mathcal{E}$.

Let $A,B$ be fixed objects and form the ambient exponential object $B^A$. For every $X$, the exponential adjunction identifies maps $X\to B^A$ with maps $X\times A\to B$. Since $L$ is left exact and $LA=A$,and its unit corresponds to ${\eta }_X\times 1_A$. Because $B$ is fixed, every map $X\times A\to B$ therefore extends uniquely to $LX\times A\to B$. Transposing back givesThe fixed-object criterion from part (i) shows that $B^A$ already belongs to $\mathcal{L}$. The ambient evaluation and transpose universal property restrict to the full subcategory, proving the subcategory is cartesian closed. This constructs exponentials in a left-exact reflective subcategory, rather than merely reflecting an exponential and assuming its universal property survives.

Let $M\times X$ have the diagonal right monoid action $(g,x)m=(gm,xm)$, and put $E={\mathrm{Hom}}_M(M\times X,Y)$. Define the right action on this set of equivariant maps of monoid sets byIt really stays in $E$: $(ek)(gm,xm)=e(kgm,xm)=e(kg,x)m$. Also $e1=e$ and $((ek)l)(g,x)=e(klg,x)=(e(kl))(g,x)$, so it satisfies the right-action law. Left multiplication in the first argument is intentional; no commutativity of $M$ has been assumed.

Define the evaluation map of an exponential objectIt is equivariant, becauseFor any right $M$-set $Z$ and equivariant map $h:Z\times X\to Y$, define its currying byFor fixed $z$, this is equivariant in the diagonal variables: $h(zgm,xm)=h(zg,x)m$. The map $z\mapsto \hat{h}(z)$ is also equivariant, sinceIt satisfies $\mathrm{ev}(\hat{h}(z),x)=h(z,x)$.

Conversely, given an equivariant $u:Z\to E$, set $h(z,x)=u(z)(1,x)$. Evaluation makes this equivariant, and currying recovers $u$:These constructions are inverse and natural in $Z$. Therefore they establish the exponential object universal propertyThis is the exponential of right monoid actions, not the set of ordinary maps $X\to Y$ with an arbitrarily guessed action.