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?

Caveat: this is a large site and it's not clear that it will work in only one shot. – François G. Dorais♦ Jan 3 '13 at 3:11