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).

1more comment