Are inverse images of separated presheaves separated? $\newcommand{\Sh}{\operatorname{Sh}}$
Let $f: X \to Y$ be a continuous map, so that there is an induced geometric morphism $f^* \dashv f_* : \Sh X \to \Sh Y$, where
$$
(f^*G)(U) = (f^\dagger G)^a(U) = (\operatorname{colim}_{V \supseteq f(U)} G(V))^a
$$
where $\cdot^a$ denotes sheafification and $f^\dagger$ denotes the inverse image presheaf.

Question. Is $f^\dagger G$ separated when $G$ is separated?

My guess is yes. Here's why.
First of all, we gotta get an hold on $f^\dagger G$. My intuition is that sections $s \in f^\dagger G(U)$ are the same things as sections of $G$ defined on an open neighbourhood of $f(U)$, up to the equivalence defined by
$$
(s, V_1) \sim (t, V_2) \quad\text{iff}\quad \exists V_1 \cap V_2 \supseteq W \supseteq f(U),\ s\vert_W = t\vert_W.
$$
This is the same intuition behind the definition of stalk, which is indeed an inverse image.
Now, let $U$ be an open of $X$, and $\{U_i\}_{i \in I}$ an open cover of $U$. We want to check whether, given $s, t \in f^\dagger G(U)$, then $s\vert_{U_i} = t\vert_{U_i}$ for all $i \in I$ implies $s = t$.
Unpacking this, it means we are given $s \in G(V_1)$ and $t \in G(V_2)$, where $V_1,V_2 \supseteq f(U)$, and we know that $s\vert_{U_i} = t\vert_{U_i}$ for every $i \in I$. Notice that restriction here is 'trivial', since $V_1,V_2 \supseteq f(U_i)$ so $s$ and $t$ are valid elements of $f^\dagger G(U_i)$ (up to equivalence, of course). What changes is the equivalence relation which is now larger, so when we say $s\vert_{U_i} = t\vert_{U_i}$ we now mean
$$
\exists V_1 \cap V_2 \supseteq W_i \supseteq f(U_i),\ s\vert_{W_i} = t\vert_{W_i}.
$$
Therefore we know $s$ and $t$ coincide on a neighbourhood of every $f(U_i)$. Let $T = \bigcup_{i \in I}W_i$. This is an open neighbourhood of $f(U)$ and it's contained in $V_1 \cap V_2$. We know $G$ is separated: thus from $s\vert_{W_i} = t\vert_{W_i}$ for every $i \in I$ we can conclude $s\vert_T = t\vert_T$, which is enough to conclude $s \sim t$ in $f^\dagger G(U)$, proving the claim.
 A: Here's a higher-tech proof:
By definition, the geometric morphism induced by $f$ makes the following square commute:
$\require{AMScd}$
\begin{CD}
[\mathcal{O}(X)^{\mathrm{op}},\mathbf{Set}] @>{f'}>>
[\mathcal{O}(Y)^{\mathrm{op}},\mathbf{Set}];\\
@A{i}AA @AA{j}A \\
\mathrm{Sh}(X) @>{f}>> \mathrm{Sh}(Y),
\end{CD}
where $f'$ is the geometric morphism whose direct image is composition with (the opposite of) the functor $f^{\#}:\mathcal{O}(Y) \to \mathcal{O}(X)$ and the vertical maps are the inclusions of subtoposes.
Now, a presheaf $G$ on $\mathcal{O}(Y)$ is separated if and only if its unit $\eta_G: G \to j_*j^*(G)$ is monic. So we want to know whether $\delta_{f'^*(G)}: f'^*(G) \to i_*i^*f'^*(G)$ is monic, where $\delta$ is the unit of $i$. Considering the naturality of $\delta$ along $f'^*\eta_G$, we have a commutative square:
\begin{CD}
f'^*(G) @>{\delta_{f'^*(G)}}>> 
i_*i^*f'^*(G);\\
@V{f'^*\eta_G}VV @VV{i_*i^*f'^*\eta_G}V \\
f'^*j_*j^*(G) @>{\delta_{f'^*j_*j^*(G)}}>>
i_*i^*f'^*j_*j^*(G),
\end{CD}
The left hand vertical morphism is a mono since $f'^*$ preserves monos. The right hand vertical morphism is equal to $i_*f^*j^*\eta_G$ by commutativity of the diagram above, and so is an isomorphism, since $j^*\eta_G$ is the canonical isomorphism $j^*(G) \cong j^*j_*j^*(G)$. Finally, we use the fact that $f'^*$ preserves sheaves to deduce that $\delta_{f'^*j_*j^*(G)}$ is an isomorphism, whence $\delta_{f'^*(G)}$ is a monomorphism, as required.
Of course, verifying that last step directly is just as much work as your proof, but it's a better known result, since it follows from the fact that $f^{\#}$ is a morphism of sites, and this proof will generalise to any similar situation involving a morphism of sites.
