We live in a topos. Given $x\in X$ write $\neg\neg \left\{ x \right\}$ for the subobject comprised of $x^\prime \in X$ satisfying $\neg\neg(x=x^\prime)$, i.e $x,x^\prime$ are indistinguishable. In (1.6) of this paper by Bunge, we have the following.
Claim. Let $x\in X$ and let $x^\prime\in \neg\neg \left\{x \right\}$. Let $f:\neg\neg \left\{ x \right\}\to Y$. Then $fx^\prime \in \neg\neg \left\{ fx \right\}$.
The proof:
This holds on account of the monotonicity of $\neg\neg$.
This is probably super basic, but what is meant by the monotonicity of $\neg\neg$, and why is $\neg\neg$ monotonic in this sense? I'm guessing this has something to do with Lawvere-Tierney topologies, but I don't really know anything about them.
"Monotonicity of $\lnot\lnot$" means that if $X \to Y$ is provable then so is $\lnot\lnot X \to \lnot\lnot Y$ (in the intuitionistic language of the toposes in question). This isn't too hard to see, e.g., using the provable assertion $(X \to Y) \to (\lnot Y \to \lnot X)$.