I came up with this question when trying to give a more detailed answer to a question by Tim Campion in [a comment](https://mathoverflow.net/questions/424356/examples-of-statements-that-are-valid-in-every-spatial-topos?rq=1#comment1121603_435325) to Ingo Blechschmidt's answer to https://mathoverflow.net/q/424356/41291.

There is an obvious internalized form of Zorn's lemma for toposes. 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 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 Zorn's lemma 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 in more generality?