# work in a topos as in sets: disjoint coproducts

Assume a topos $\mathcal{S}$ as the base topos, and we work in this topos as in naive set theory (without choice or excluded middle). Take a Grothendieck topos $\mathcal{E} \to \mathcal{S}$ with a site of definition $\mathcal{C}$. As usual in the literature consider that $\mathcal{C}$ has objects, and that these objects are objects of $\mathcal{E}$ which are generators in the sense that given any $X \in \mathcal{E}$ the family of all $f: C \to X$ all $C$ in $\mathcal{C}$ is epimorphic.

Consider $F: \mathcal{E} \to \mathcal{S}$ to be the inverse image of a point. Then the family $Ff: FC \to FX$ is epimorphic in $\mathcal{S}$. My question is the following:

Can I do the following ? (meaning, is it correct the following arguing, certainly valid if $\mathcal{S}$ is the topos of sets):

Given $a \in FX$, take $f: C \to X$ and $c \in FC$ such that $a = Ff(c)$

This is related to the validity in $\mathcal{S}$ of the following:

Given $x \in \coprod_{i \in I}{S_i}$, then $x \in S_i$ for some $i \in I$.

-
Looks valid to me: I would possibly expand it to: $\coprod_C FC \to FX$ is an epimorphism, therefore for any $a\colon\ast\to FX$ there exists $c\colon\ast\to \coprod_C FC$ lifting $a$, and since coproducts in $S$ are disjoint, $c$ factors through some component $FC$ and you're done. – David Roberts Jul 23 '13 at 22:20
Thanks David, question now is: Can I belive it ?. I guess it is a question to get used to. – Eduardo J. Dubuc Jul 23 '13 at 22:54

This argument looks OK as long as everything is understood to be in the internal logic of $\mathcal S$. 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$".
(By the way, I assume that when you regard objects of $\mathcal C$ as objects of $\mathcal E$, you implicitly identify any $C$ with the associated sheaf of the presheaf represented by $C$.)
Thanks David and Andreas, your answers were just what I needed even to formulate correctly the question. On spite of my comment to David's answer, I am quite convinced now that the arguing is correct. If CC is an internal site in SS, the expression $\{all \; f: C \to X,\; all \;C \;in\; CC\}$ I guess it determines an object in SS which legitimates the index in the coproduct expression. Then as David says, disjointness finishes to validate the arguing.