Dear Eduardo,
Thank you for keeping me au courant. Difficult as it is to write in my iPad, I want to tell you my position and what I think of your question.
My position (as that of any topos theorist) is that
1) If you work in an elementary topos SS, then it is true that you can do so "as in Sets", provided you do not use excluded middle ( as the internal logic is intuitionistic) or use Choice (as the set theory intrinsic to SS is constructive).
2) If on the other hand you work in a topos EE that is bounded over SS, then you cannot work "as in Sets" concerning constructions in EE that involve SS. Here it is necessary to resort to either the "teoria delle categorie sopra un topos di base" (indexed categories) or to the theory of fibrations.
Concerning your question, let me point out that, although you pretend to work entirely inside SS, you do not, as your construction involves EE. It certainly makes sense, since EE is locally small, and CC is small ( meaning internal to SS). What I want to warn you about is how you proceed from there without resorting to EE as a bounded SS- topos.
I apologize for previous (private) irrelevant remarks as I misunderstood your question - until now, that is.
Concerning Diaconescu's theorem, AC implies Booleaness can be done "as in Sets" but the proof is not trival. If you mean the theorem which gives a characterization of bounded SS-toposes as a classifying topos, it requires fibrations over SS.
Regards, Marta
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]