I came up with this question when trying to give a more detailed answer to a question by Tim Campion in a comment to Ingo Blechschmidt's answer to Examples of statements that are valid in every spatial topos.

There is an obvious internalized form of Zorn's lemma for toposes. Basically, you can use the Mitchell-Bénabou language to spell out the following:

given a poset $(P,\leqslant)$, consider the object of pairs $(C,u)$ where $C$ is a chain in $P$ and $u$ is an upper bound of $C$ in $P$. We say that the internal Zorn's lemma IZ holds if whenever the projection $(C,u)\mapsto C$ from this object to all chains of $P$ is epi, the object of maximal elements of $P$ is "as inhabited as $P$ itself", that is, has the same support as $P$.

If you do not care for a more rigorous formulation, skip everything until the questions.

Here is this more rigorous formulation. Given a poset $P$ in a topos $\mathscr S$, we can form the objects $\max(P)\rightarrowtail P$ of maximal elements of $P$ and $\operatorname{chains}(P)\rightarrowtail\Omega^P$ of chains of $P$. We can also form the object of upper-bounded-chains of $P$, call it, say, $\operatorname{ubc}(P)$: it is uniquely determined by saying that $\hom(X,\operatorname{ubc}(P))$ must be in one-to-one correspondence with pairs $(C,u)$, where $C\rightarrowtail X\times P$ is a subobject of $X\times P$ and $u:X\to P$ is a morphism, such that $C$ is a chain and $u$ is an upper bound of $C$, if one considers $u$ as an element of $X^*(P)$ and $C$ as a subobject of $X^*(P)$, in the slice topos $\mathscr S/X$.

Clearly there is a canonical projection $\pi:\operatorname{ubc}(P)\to\operatorname{chains}(P)$, given by sending $(C,u)$ to $C$.

We can then formulate the internal version IZ of the Zorn lemma as follows:

If $\pi:\operatorname{ubc}(P)\to\operatorname{chains}(P)$ is epi, then $\max(P)$ has the same support as $P$; that is, the image of $\max(P)\to1$ is the same as the image of $P\to1$ (where $1$ is the terminal object of $\mathscr S$).

Minimal question: do all toposes satisfy this?

I suspect that, arguing internally, one might deduce from IZ internal choice IC which in turn implies booleannes, but somehow I don't see how to actually do it.

Extended question (again in case the answer to the minimal question is negative): there might be more sophisticated internalizations of the Zorn's lemma. For example, one can consider, for an object $P$, the object $\operatorname{Orders}(P)$ of partial orders on $P$ and then internalize the statement "partial orders with all chains upper-bounded are included in partial orders having a maximal element". Is there a form which would be weaker, in the sense that it holds for some topos which does not satisfy IZ?

Here is, specifically, a version about which I would like to ask. This actually corresponds on the "classical" side to the variant of the Zorn's lemma with requiring upper bounds for nonempty chains only.

Call an internal poset $(P,\leqslant)$ internally inductive if for any object $X$ and any $C\rightarrowtail X\times P$ which is a chain of $X^*(P)$ in $\mathscr S/X$, the object $U_C\rightarrowtail X\times P$ of upper bounds of $C$ has support no less than $C$. That is, the image of the composite $U_C\rightarrowtail X\times P\to X$ contains the image of $C\rightarrowtail X\times P\to X$, where $X\times P\to X$ is the projection.

We then say that IZ' holds in $\mathscr S$ if for every internally inductive poset $P$, the object $\max(P)$ has the same support as $P$, as above.

And the specific instance of my Extended question is,

Which toposes satisfy IZ'?

Important correction

As Gro-Tsen points out in a comment, this does not make much sense unless I restrict to Grothendieck toposes with Axiom of Choice holding in my set theory. Slightly more generally, one may consider toposes bounded over a topos with AC. Maybe still more generality is possible, but let us stick to this for definiteness.