The following result is well-known in folklore (I think), but I’ve been unable to find a reference in the literature:



> 
> Let $T$ be a finitely presented essentially algebraic theory, and $\newcommand{\E}{\mathcal{E}}\E$ an elementary topos with NNO. Then there is an initial model of $T$ internal to $\E$.
> 
> 
> 


(By *essentially algebraic* I mean the notion also known as a *cartesian theory* or *finite limit theory*.)


As with many folklore results, various generalisations of this (to settings weaker than elementary toposes, and giving a monadic left adjoint not just an initial model) should also hold, and are also I think fairly well-known or “clearly straightforward generalisations” to people sufficiently well-versed in the field — I’d be equally interested to hear a reference for any such generalisations.


I’d also be interested if anyone can see a way to deduce this directly from some other result(s) in the literature. Proving this by hand isn’t terribly hard (essentially: take the standard construction of a free set model using syntax, and internalise it to an elementary topos), but there’s a fair bit of careful detail-checking to do there (especially when weakening the setting to less than a topos), and I haven’t managed to find a simpler way to deduce it from results in the literature.


The closest results I’ve found are:


* Theorem 7.43 of Johnstone 1977 *Topos Theory*, due to Lesaffre, which is the special case of single-sorted algebraic theories.
* Ch.VI of Johnstone–Wraith 1978 *Algebraic theories in toposes* (in *Indexed categories and their applications*, LNM 661 1978). This gives some very relevant results, for a class of theories nearly as general as EAT’s (and sufficient for my interests), but doesn’t (as far as I can see) give free models or any result which immediately implies their existence, except in the special case of the theory of categories, which is rather easier than the general case.
* The material in §B2 of Johnstone’s *Sketches of an Elephant*, particularly Theorem 2.4.6, the indexed special adjoint functor theorem. One can deduce this result from that theorem, but the application requires (among other ingredients) construction of a separating family, which seems to me not much easier than just constructing free models by hand directly (but perhaps I’m overcomplicating something).



Free models of finitely presented essentially algebraic theories in elementary toposes?
If you are willing to accept internal argument instead of purely categorical (external) one, a very good reference for this is Palmgren and Vickers' paper: " [Partial Horn Logic and cartesian categories](https://core.ac.uk/download/pdf/82110032.pdf)".


They give a construction of the initial model for "partial horn theories" (which are equivalent to cartesian theories) which is constructive and predicative.


They don't completely clarify what framework is needed for their proof, but looking at the paper it seems clear that it can be applied internally in any exact locally cartesian closed category with a natural number objects.


I believe (and Steve Vickers seemed to think it was the case as well last time we spoke) their proof also applies within an "arithmetic universe" (a pretopos with parametrized list object) but that is not so easy to extract from the paper.


In both case it applies in elementary toposes with NNO. This is explicitly claimed in the introduction of the paper : they mentioned it can be applied internally within the "predicative toposes" of Moerdijk and Palmgren, and this includes elementary toposes with NNO.


For the record, I would be quite interested if someone could give a satisfying proof that this construction works in an arithmetic universe.


