Unions and inverse image in a topos I'm not an expert on topos theory, but I have some knowledge of category theory. I know that finite intersections are preserved by inverse image in a topos. Are unions preserved by inverse image in a topos too? That is, if $m$ and $n$ are subobjects of the object $A$ and $f:C\rightarrow A$ is an arrow in a topos $\mathcal{E}$, then $f^{-1}(n)\cap f^{-1}(m)\cong f^{-1}(n\cap m)$. Is it the case that $f^{-1}(n)\cup f^{-1}(m)\cong f^{-1}(n\cup m)$? In $\mathbf{Set}$, this is true.
 A: Yes, this is true in a general topos.  The brief proof is using the theory of the internal language and internal logic of a topos: the standard proof in $\mathbf{Set}$ that this statement is true doesn't use any instances of purely classical reasoning such as double negation elimination or law of excluded middle.  Therefore, the argument translates straightforwardly into a formal proof in the internal logic of a topos that
$$A \mathrm{~type}, C \mathrm{~type}, f : C \multimap A, m : P(A), n : P(A) \vdash f^{-1}(m \cup n) = f^{-1}(m) \cup f^{-1}(n) \mathrm{~true}.$$
The general theory then tells us: for any topos, if we have objects $U, A, C$, along with morphisms $f \in \operatorname{Hom}(U, C \multimap A)$, and $m, n \in \operatorname{Hom}(U, P(A))$, then $f^{-1}(m \cup n) = f^{-1}(m) \cup f^{-1}(n)$ as elements of $\operatorname{Hom}(U, P(C))$.  In the special case where $U := 1$, this is equivalent to: for $f \in \operatorname{Hom}(C, A)$, $m, n \in \operatorname{Sub}(A)$, we have $f^{-1}(m \cup n) = f^{-1}(m) \cup f^{-1}(n)$ as subobjects of $C$.

Furthermore, it is straightforward to unfold the general proof to give an idea of why this particular result holds.  The general results from the theory that will be relevant are:

Proposition: For subobjects $m, n$ of $A$, $m = n$ (i.e. $m$ and $n$ are equivalent subobjects of $A$) if and only if for every object $U$ and every morphism $a \in \operatorname{Hom}(U, A)$, $a$ factors through $m$ if and only if $a$ factors through $n$.


Proposition: For objects $U, C, A$ and morphisms $f \in \operatorname{Hom}(C, A)$, $c \in \operatorname{Hom}(U, C)$, and subobject $m$ of $A$, we have that $c$ factors through $f^{-1}(m)$ if and only if $f \circ c$ factors through $m$.


Proposition: For objects $U, A$ and subobjects $m, n$ of $A$, and morphism $a \in \operatorname{Hom}(U, A)$, we have that $a$ factors through $m \cup n$ if and only if there exist morphisms $\pi_1 \in \operatorname{Hom}(V_1, U), \pi_2 \in \operatorname{Hom}(V_2, U)$ such that $a \circ \pi_1$ factors through $m$; $a \circ \pi_2$ factors through $n$; and $\pi_1 + \pi_2 : V_1 \sqcup V_2 \to U$ is an epimorphism.


Proposition: For objects $V, U, A$ and a subobject $m$ of $A$, along with morphisms $a \in \operatorname{Hom}(U, A)$ and $\pi \in \operatorname{Hom}(V, U)$ where $\pi$ is an epimorphism, if $a \circ \pi$ factors through $m$, then $a$ factors through $m$.

Now, to prove the desired result, first suppose that $c : U \to C$ factors through $f^{-1}(m \cup n)$.  Then $f \circ c$ factors through $m \cup n$, so there exist $\pi_1 : V_1 \to U$ and $\pi_2 : V_2 \to U$ as in the third proposition above with $f \circ c \circ \pi_1$ factoring through $m$ and $f \circ c \circ \pi_2$ factoring through $n$.  Therefore, $c \circ \pi_1$ factors through $f^{-1}(m)$ and $c \circ \pi_2$ factors through $f^{-1}(n)$, so $c$ factors through $f^{-1}(m) \cup f^{-1}(n)$.
Conversely, suppose that $c : U \to C$ factors through $f^{-1}(m) \cup f^{-1}(n)$.  Then there exist $\pi_1 : V_1 \to U$ and $\pi_2 : V_2 \to U$ as in the third proposition above with $c \circ \pi_1$ factoring through $f^{-1}(m)$ and $c \circ \pi_2$ factoring through $f^{-1}(n)$.  Therefore, $f \circ c \circ \pi_1$ factors through $m$; and similarly, $f \circ c \circ \pi_2$ factors through $n$.  Therefore, it follows that $f \circ c$ factors through $m \cup n$, and so $c$ factors through $f^{-1}(m \cup n)$.  $\square$

As for some illustration as to where the above propositions come from, it might be useful to show what the analogs are in a category of sheaves on a topological space.  The first is an analog of the extensionality of subsheaves principle: for subsheaves $\mathscr{F}', \mathscr{F}''$ of $\mathscr{F}$, $\mathscr{F}' = \mathscr{F}''$ if and only if for every open $U$ and $x \in \mathscr{F}(U)$, $x \in \mathscr{F}'(U)$ if and only if $x \in \mathscr{F}''(U)$.  The second is an analog of the definition of inverse image of a subsheaf: for $\phi : \mathscr{F} \to \mathscr{G}$ and subsheaf $\mathscr{G}'$ of $\mathscr{G}$, for $x \in \mathscr{F}(U)$, $x \in (\phi^{-1}\mathscr{G}')(U)$ if and only if $\phi_U(x) \in \mathscr{G}'(U)$.  The third is an analog of the definition of the union of two subsheaves: given subsheaves $\mathscr{F}', \mathscr{F}''$ of $\mathscr{F}$, for $x \in \mathscr{F}(U)$, $x \in (\mathscr{F}' \cup \mathscr{F}'')(U)$ if and only if there exist open $V_1, V_2 \subseteq U$ such that $x |_{V_1} \in \mathscr{F}'(V_1)$; $x |_{V_2} \in \mathscr{F}''(V_2)$; and $V_1 \cup V_2 = U$.  The fourth is an analog of the gluing condition of a subsheaf: for a subsheaf $\mathscr{F}'$ of $\mathscr{F}$, and an open cover $\{ V_i \mid i \in I \}$ of $U$, we have $x \in \mathscr{F}(U)$ is in $\mathscr{F}'(U)$ if and only if $x |_{V_i} \in \mathscr{F}'(V_i)$ for all $i \in I$.
