Hi, first many thanks to all who answered my question (in the list and in mathoverflow). I feel now the need to further clarify my question which I thought was clear enough. A) Three answers respond to the intended interpretation of my question and say the same, that the arguing is correct. 1) Looks valid to me: I would possibly expand it to: COPRODUCT_{all f: C ---> X, all C in CC} FC ---> FC, is an epimorphism, therefore for any a: * ---> FX there exists c: * ---> COPRODUCT_{all f: C ---> X, all C in CC} FC lifting a, and since coproducts in SS are disjoint, c factors through some component FC and you're done. ? David Roberts. It is mysterious however for what stands the symbol "*" ? 2) This argument looks OK as long as everything is understood to be in the internal logic of SS. In particular, the implicit existential quantifiers "there exists C and there exists c" should be understood internally (i.e., as local existence); similarly for the quantifier "for some i \in I". Andreas Blass. This is very clear. 3) Your statement is valid internally in SS, that is once formalized in the internal language of the topos SS; this can be done in geometric logic, by considering a (possibly infinitary) disjunction over all the arrows f: C ---> X for C in CC (interpreted by the arrows Ff in SS) and existential quantifications. Olivia Caramello. This seems somehow less clear, the wording "(possibly infinitary) disjuntions" opens the door for a misunderstanding, and should be explained. Well, I had some other private answers on the negative, and also in the form "yes and no". All these answers do not interpret my question the way it was intended. They talk about fibrations, coverings, atoms, etc, nothing to do with my question. They interpret my question essentially by an external view, while it is purely internal. Now, two new postings to the list made me think it is pertinent to clarify and expand the question: Answering Olivia 3), Thomas Streicher writes: 4) Since CC is internal to SS which is assumed as different from Set it doesn't make sense to consider an infinite disjunction over all arrows f: C --> X for C in CC. Thomas And Olivia answers: 5) It seems to me that Eduardo assumed CC to be a site for EE in the classical sense, i.e. not a site internal to SS but to Set (since he wrote that "CC has objects, and that these objects are objects of EE which are generators in the sense that given any X in EE, the family of all f: C ---> X, all C in CC, is epimorphic"); so an infinite disjunction makes sense in this case. Olivia Well, it seems to me things are now mixed up, and I will intent to clarify, expecting also to be not quite right. First, I said in my original posting and in mathoverflow: "As usual in the literature (Joyal-Tierney, Moerdijk, Bunge, and many more) consider that CC has objects, and that these objects are objects of EE which are generators in the sense that given any X in EE, the family of all f: C ---> X, all C in CC, is epimorphic." "As usual in the literature", Olivia miss this point when she answers Thomas. Technically speaking I am assuming CC to be an internal site in SS. My question is purely refered to the validity in the internal language of the topos SS. I give two examples: 6) "Thus, we take the point of view that an arbitrary, but fixed, (elementary) topos is our basic universe of sets, We work in this universe as we would in naive set theory, except that, of course, we cannot use the axiom of choice, or the law of excluded middle. This has been shown to be correct by various authors (e.g. Boileau-Joyal). Joyal-Tierney, An extension of the galois theory of grothendieck, Memoirs 309." 7) "Throughout this paper SS denotes a fixed base topos, all toposes are assumed to be Grothendieck toposes over SS, and all geometric morphisms are taken to be bounded. Moerdijk, Continuos fibrations and inverse limits of toposes Compositio Mathematica 58." Then, in these two papers their sites happily have objects, their objects happily have elements (as if they were sets, not externally in the sense of sections from an object in the site), etc etc. But one has to work carefully, see for example the definition of open site in 6). For the validity of all this only (e.g. Boileau-Joyal) is needed (no theory of indexed categories or fibrations, etc). Then, thats it !, the arguing is correct !, why bother more ?, as answers 1) 2) and 3) point out. Well, it seems I still need some more reassuring facts. I quote a (private, but since then Thomas has written to the list, I feel he would not object) knowledgeable answer by Thomas 8) my reply would be that given a g.m. F -| U : EE -> SS this corresponds to a fibration P_F of toposes over SS (P_F is obtained by pulling back the codomain fibration along F). In the internal language of SS one can speak about the fibration P_F only in a restricted way. 1) Does it make sense to take E = COPRODUCT_{all f: C ---> X, all C in CC} FC ? We have g: E ---> FX an epimorphism, so we can take c in E such that a = g(c). Well, the g.m. F -| U : EE -> SS being bounded is already equivalent to the existence of a generic family G -> FI. Since P_F is a locally small fibration (because U has a right adjoint) by Th.10.5 of www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf your claim 1)follows. See also footnote 15 on p.78 of loc.cit. Maybe you find pp.51-52 of Bunge and Funk's book more illuminating in this respect. Then we would need the validity of: 2) Given x in COPRODUCT_{i in I} S_i , then x in S_i for some i in I. Depends on how you read this. If you read it externally for a Grothendieck topos SS over Set it is wrong if SS is not connected. But the answer is trivially YES if you think of (S_i)_{i \in I} as a map S -> I in SS. But for general toposes SS there is no other meaning of family of objects in SS indexed by I. Then, this justify that the arguing is correct, according with 1) and 2). From this I figured out and wrote (privately to Thomas) 9) Thanks for your answer, it confirms that the arguing is correct. Given an internal site CC in SS, the expression {all f: C ---> X, all C in CC} actually determines an object in SS which legitimates the index in the coproduct expression COPRODUCT_{all f: C ---> X, all C in CC} FC, then the answer for 2) is trivially yes as you say. and he answered "right!". But he also writes later in the Mail: 10) The problem rather is that in (the language of) SS you can't quantify over such families (nor can you quantify over objects of SS in SS). Well, there are possibilities arising from Algebraic Set Theory but that means that you work in a category of classes constructed from SS. In any case reasoning "like in Set" doesn't work for arbitrary base toposes. How we should understand this ?. Luckily in my question there is no quantification of this sort. I understand that you can quantify (abusing notation) over objects of SS when these objects are objects of an internal site CC, as it is done in 6) and 7). So, this seems to be no objection to the validity of the arguing in my original question. I am really sorry if the experts find this long discussion banal, but I am posting it since I know it would be useful to many interested non experts in the subject. And now, I rise a new question to the list: B) 1) To do many mathematical reasonings and constructions over an arbitrary base topos, in several places in the literature classical category theory (pull-backs, subobject classifiers, colimits, effective epimorphisms, etc etc) is painfully and carefully used (e.g. the books Topos theory, Vol. 10, Academic Press, London, 1977, or Sheaves in Geometry and Logic, Springer, 1992). Why bother ? Take for example Diaconescu Theorem, Can we reason as follows ?: 2) This theorem needs no proof, since the proof of the statement with the topos of sets as a base topos (SGA4 expose IV, Proposition 4.9.4, p356, SLN 269) can be done with an arbitrary base topos since "we work in this universe as we would in naive set theory". Just check that no use is made of choice, the excluded middle, quantification over "large" families or any other non kosher things. e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]