Dear Eduardo, I understand your point better now. For you FX is already given as the respective colimit. This was shown by Celeyrette in his 1974 Th'ese directed by B'enabou (Ch.VI Theorem de Kan where you also find a proof of Diaconescu's theorem over arbitrary bases). But you have to rely on a theorem characterizing colimits of small diagrams in SS from which it follows that the source tupling (in the sense of internal sums) of the cone is epic. Even if you think it is splitting hairs you cannot express the property of being epic in SS within the internal language of SS. You can express in the internal language of SS that a map is surjective and show externally that SS validates f being surjective iff f is epic in SS. (For expressing "epic" in SS one would have to quantify over all objects in SS which one cannot do in the internal language of SS.) So my conclusion is that the argument you give is ok for most purposes. What I wrote above (and previously) gives some additional justification of its correctness. I will be offline till next weekend and therefore have no time to continue a discussion with many mails back and forth. Moreover, I think things have been clarified to quite some extent. Best, Thomas PS "purely external categorical construction in SS" is a contradiction in terms formulations like these have given me the impression that you have wrong reason for a correct result [For admin and other information see: http://www.mta.ca/~cat-dist/ ]