Hello, I have the following question: Assume a topos SS as the base topos, and work in this topos as in naive set theory (without choice or excluded middle). Take a Grothendieck topos EE ---> SS with a site of definition CC. 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. Consider F: CC ---> SS to be the inverse image of a point. Then the family Ff: FC ---> FX is epimorphic in SS. My question is: Can I do the following ? (meaning, is it correct the following arguing, certainly valid if SS is the topos of sets): Given a in FX, take f:C ---> X and c in FC such that a = Ff(c). We can break this question in two: 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). 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. greetings e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]