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. 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.