Is The Power Object Functor Faithful?

Question

In an elementary topos, can we conclude that the power object functor $P:\mathcal{E}\to\mathcal{E}^\text{op}$ is faithful, i.e. if $Pf=Pg:PY\to PX$ then $f=g:X\to Y$?

Scroll down for (incomplete) textbook proof!

If $f\neq g$ then the equalizer of $f$ and $g$ must be different from $X$, but I don't see directly how that would help.

My idea was the following:

We can construct the singleton map $\{\cdot\}_Y:Y\to PY$. Then I believe that we can construct $\ulcorner x\in Pf(\{y\})\urcorner$ as a subobject of $X\times Y$ hence we have a map $f':X\to PY$ constructed from $Pf$. For this map, the subobject $\ulcorner f'(x)\text{ is singleton}\urcorner$ should be equal to $X$ (but I don't know how to prove it). Now I wonder if this suffices, i.e. when we have $f,g:X\to Y$ with $\ulcorner f(x)\in f'(x)\urcorner$ and $\ulcorner g(x)\in f'(x)\urcorner$ both equal to $X$ (i.e. true on all of $X$), would $f=g$ follow from here?

Or in other words, given a map $f':X\to PY$, can we construct $f'':X'\to Y$, where $X'$ is the subobject $\ulcorner f'(x)\text{ is singleton}\urcorner$, with the property $\ulcorner f''(x)\in f(x)\urcorner$, something like choice for singletons?

[EDIT] I Found a proof in Sheaves In Geometry And Logic:

But there is still some argument left out. Overall, it seems not too far from my own thoughts. But I still fail to put everything together.

Answer 1

Let us look at the problem from the point of view of Yoneda's lemma. Then $P(f) : P(Y) \to P(X)$ corresponds to a morphism of functors $\operatorname{Sub}({-} \times Y) \to \operatorname{Sub}({-} \times X)$, which takes a subobject of $U \times Y$ to the pullback along $\operatorname{id}_U \times f : U \times X \to U \times Y$, which is a subobject of $U\times X$. Now, if we take the special case where $U = Y$ and the subobject is the diagonal $(\operatorname{id}_Y, \operatorname{id}_Y) : Y \hookrightarrow Y \times Y$, then it is straightforward to check that the pullback is the transpose of the graph of $f$, $(f, \operatorname{id}_X) : X \hookrightarrow Y \times X$.

Therefore, if $P(f) = P(g)$, then $(f, \operatorname{id}_X)$ and $(g, \operatorname{id}_X)$ must give the same subobject of $Y \times X$. In other words, there is some $h : X \to X$ such that $(f, \operatorname{id}_X) \circ h = (g, \operatorname{id}_X)$. However, composing with $\pi_2$, we see that we must have $h = \operatorname{id}_X$; and then composing with $\pi_1$ gives that $g = f \circ h = f$.

Answer 2

This answer is probably not what you want, but I felt that it might still be interesting. Because every elementary topos supports constructive reasoning via its "internal language", it is enough to give a constructive proof of the set/type-theoretic naive element-based analog:

Let $x \in X$. By definition, we have $x \in (Pf)(\{f(x)\})$. By $Pf = Pg$, we also have $x \in (Pg)(\{f(x)\})$. By definition, this amounts to $g(x) \in \{f(x)\}$, so $f(x) = g(x)$.