In a document about constructive maths, I saw the following exercise : prove that $f^{-1}: \mathcal{P}(Y) \to \mathcal{P}(X)$ is injective if and only if $f$ is surjective.
There is an easy constructive proof of the "if $f$ is surjective part".
However the "if $f^{-1}$ is injective" part eludes me: Let $y\in Y$. Then $\{y\}\neq \emptyset$ so $f^{-1}(\{y\}) \neq f^{-1}(\emptyset)=\emptyset$.
But how can I conclude from $A\neq \emptyset$ that there is $x\in A$ constructively ? If I'm not mistaken, you can't (in the topos $\mathbf{Set}^2$, $(1, 0)$ has no global element though it's not the initial object - I don't know much about topos theory yet so I can't formalize this but heuristically this seems to indicate that there is no proof of $A\neq \emptyset \vdash \exists x, x\in A$)
So this route seems doomed. Obviously I can't use the contrapositive because I would only get "If $f^{-1}$ is injective then $f$ is not not surjective" (and I'm not even sure there's an easy constructive proof of the contrapositive)
I'm afraid I'm missing something obvious, but I'm not used to constructive reasoning at all so it would be of great help ! And also, can my argument about $\mathbf{Set}^2$ be formalized ?
Suppose $f^{-1}$ is injective. Then $f^{-1}(\operatorname{im}(f)) = f^{-1}(Y) = X$; therefore, $\operatorname{im}(f) = Y$.
Note that in a general topos, surjectivity of a function $f : X \to Y$ does not in general imply that the corresponding map of global sections $f(1) : X(1) \to Y(1)$ is surjective. For example, if $\mathscr{F}$ and $\mathscr{G}$ are sheaves of sets on some topological space $X$, then surjectivity of $f : \mathscr{F} \to \mathscr{G}$ means: for each open $U \subseteq X$ and $y \in \mathscr{G}(U)$, there is an open cover $\{ V_i : i \in I \}$ of $U$ and sections $x_i \in \mathscr{F}(V_i)$ such that $f(V_i) (x_i) = y |_{V_i}$ for each $i \in I$.
In fact, the failure of global sections of a general surjective map to be surjective is studied in detail in sheaf cohomology theory.
However, you are correct in stating that for $A \in \mathcal{P}(X)$, then $A \ne \emptyset$ does not in general imply $\exists x \in X, x \in A$. For a counterexample, consider the topos of sheaves of sets on $\mathbb{R}$, $X := 1$, and $A$ is the section of $\mathcal{P}(X)(1) \simeq \operatorname{Sub}(X)$ corresponding to $\mathbb{R} \setminus \{ 0 \}$. Then it turns out $A = \emptyset$ corresponds to $\emptyset \in \Omega(1)$, so $A \ne \emptyset$ corresponds to $\mathbb{R} \in \Omega(1)$, whereas $\exists x \in X, x \in A$ corresponds to $\mathbb{R} \setminus \{ 0 \} \in \Omega(1)$.
In fact, in general, $A \ne \emptyset$ is equivalent to $\lnot \lnot (\exists x \in X, x \in A)$.