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.
Best Answer
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)$.