It has been known for some time that one can define a topos as a model of a (finitary) essentially algebraic theory (or in other words, can be defined internal to any category with finite limits). In particular, given a topos $E$ (for instance the topos of sets) one can define an internal topos in $E$ (e.g. a small topos). One can ask for stronger (and in fact is easier to define) in an internal _universe_: this is a category theoretic analogue of a Grothendieck universe. Such a thing gives rise to an internal topos $M$ in $E$ that is in addition a _locally full subcategory_. The nontechnical definition is that there is an $E$-object $e(x)$ of $M$-elements of any $M$-object $x$ (recall that elements are functions $1 \to x$, here taken in $M$), and (the $E$-object of) functions _in $E$_ between $e(x)$ and $e(y)$ correspond to the $E$-object of functions _in $M$_ between $x$ and $y$.

There are toposes, given a metatheory of $ZFC$, that have no universes in this sense, namely the topos of sets in $V_{\omega+\omega}$, much like one cannot prove the existence of Grothendieck universes in vanilla ZFC. 

What I'm curious about is the existence of internal toposes that _aren't_ locally full (equivalently, arise from universes). Shouldn't we get the _free internal topos_ in a topos? If we have NNOs, can we get the free internal topos with NNO? Are there good descriptions of these?

Given the topos of ZFC sets, the models of ZC give internal toposes, but I'm interesting in when we can say something about internal toposes without any material meta-theory.


----

Postscript: Joyal defined (in work decades old by not yet published) a special sort of category called an _arithmetic universe_, which is much weaker than a topos, yet has enough structure to define the free internal arithmetic universe in it. I guess the free internal topos should be exist in a topos, but otherwise I can't be sure it's possible. I worry about erroneously "proving the existence of a model" out of nothing.