Relative consistency of ETCS over the theory of a well-pointed topos with NNO EDIT: I'm bumping this, because I'm still curious, and because I have a relative consistency result over the theory of a well-pointed topos with NNO, and I am wondering how much baggage I save by not assuming AC in the base model (I'm not using AC in the proof either).
Gödel's well-known proof of the implication $Con(ZF) \Rightarrow Con(ZFC)$ used the construction of the inner model $L$ in $ZF$ to get a model of $ZFC$ (and in fact much more). However such a construction is not (immediately) available in a category-theoretic approach to set theory. In particular, given a well-pointed topos with NNO, which is the set theory ETCS minus the axiom of choice, I wonder whether there is any way to construct a model of ETCS. On the face of it, it doesn't seem likely, as objects of the given topos are quite amorphous. 
The only thing I can think of (admittedly I haven't tried very hard) is by passing to a model of ZF via pure sets, constructing $L$, and then taking the category of sets of $L$. But this is somewhat unsatisfactory, as it leaves the comfy realm of categories and heads out into material set theory. So:

Is there a category-theoretic construction of a model of ETCS from a well-pointed topos with NNO?

 A: I confess that I am not altogether clear what the Question requires, whilst many of the Comments are beyond me, but here is a construction of which you may not be aware and which may throw some light on the issues.
It is based on my paper Intuitionistic Sets and Ordinals, in the Journal of Symbolic Logic 61 (1996) 705-744, particularly Section 3. This in turn built on Categorical Set Theory: a characterisation of the Category of Sets by Gerhard Osius in the Journal of Pure and Applied Algebra 4 (1974) 79-119.
We are working in some given elementary topos, whose objects I will call carriers in order to avoid the word set.
A model of a fragment of set theory is given by a carrier $X$ equipped with a binary relation $\epsilon$ that it is convenient to regard as a map $\epsilon:X\to P X$ to the powerset.  That is, it is a coalgebra for the covariant powerset functor.
We say that $(X,\epsilon)$ is extensional if the map $\epsilon:X\to P X$ is mono (1-1).
The definition of when the coalgebra is well founded involves a pullback diagram and is given in the paper.
Then an ensemble is an extensional well founded coalgebra.
Applying the covariant powerset functor to one ensemble gives another.
Between any two ensembles there is at most one coalgebra homomorphism, and it is mono.  This captures inclusion in the set-theoretic sense.
The category of ensembles is therefore a preorder. It is a large category in the same sense that familiar categories such as that of groups in a topos are large.
We can rehearse the standard definitions of pairing, functions, etc from set theory using ensembles and show that this preorder provides a model of the Zermelo axioms.
Natural numbers (infinity) and the axiom of choice are inherited from the given topos if it has them.
As to the axiom-scheme of replacement, understanding this from a categorical perspective was one of my principal aims in this work.  The comments in my JSL paper are really quite naive and should be discounted in favour of those at the very end of my book, However, I got interested in other things and never pursued this to a satisfactory conclusion.
