Is "points lift along surjections" equivalent to choice in the internal logic?

53 Views Asked by At

I'm wondering about the following proposition in the internal logic of a topos:

Given an epimorphism $e : E \to B$, then for every points $p : 1 \to B$, there is a point $\tilde{p} : 1 \to E$ for which $e\tilde{p} = p$.

Is this the same as the (internal) axiom of choice, ``all surjections have a section'' in the internal logic?