Any small [pretopos](http://ncatlab.org/nlab/show/pretopos) $C$ can be embedded into a Grothendieck topos by a fully faithful functor that preserves all the pretopos structure (limits, images, finite unions of subobjects, disjoint coproducts, and quotients of equivalence relations). Namely, we may consider the topos of sheaves for the coherent topology on $C$, with the sheafified Yoneda embedding. If $C$ is (locally) cartesian closed, then that structure is also preserved by this embedding.


My question is, what if $C$ also has a natural numbers object, or more general initial algebras for special endofunctors (e.g. "W-types")? Can we embed it into a topos of sheaves in a way that preserves these initial algebras?



Sheaf embedding preserving initial algebras?
Sometimes, but not always.


One case when this is possible is given by Proposition D5.1.8 in *Sketches of an Elephant*. Namely, if $C$ is a small elementary topos with an NNO that is *standard*, meaning that the family of all numerals $s^n o : 1\to N$ (for external natural numbers $n\in \mathbb{N}$) is epimorphic, then it can be embedded in a Grothendieck topos by a functor preserving both finite limits and finite colimits. Such a functor then necessarily preserves the NNO, by Freyd's characterization of the latter. The Grothendieck topos is the topos of sheaves on $C$ for the topology consisting of all (not necessarily finite) epimorphic families.


Every Grothendieck topos is standard, but Example D5.1.7 gives an elementary topos with NNO that is not standard. It is the filterquotient of $\rm Set/\mathbb{N}$ by a filter containing the cofinite filter, and it contains a global natural number $\omega : 1\to N$ that is *disjoint* (as a subobject of $N$) from every numeral $s^n o$. Moreover, just after D5.1.7 it is shown that this topos does not admit a functor to any Grothendieck topos preserving finite limits and finite colimits, and the proof actually shows that it does not admit a functor to any Grothendieck topos preserving finite limits and the NNO. The point is that such a functor would preserve the existence of a global natural number disjoint from every numeral, which is impossible in a standard topos.


Thus, the answer to the question is no in general, even if $C$ is an elementary topos; but yes if $C$ is a *standard* elementary topos. (I don't know if anything can be said about standard pretoposes; the proof of D5.1.8 is impredicative, as is the proof of Freyd's characterization of NNOs.)


