Definition of ordinals in Grothendieck toposes

Question

What is a useful definition of an ordinal in Grothendieck toposes. Useful in this context means that I would like to construct fixed points of monotone maps on complete lattices using iteration from $\bot$. Can this be done? I know one can prove that there exists the least fixed point by constructing it as the intersection of all the pre-fixed points.

To define the chains I presumably need some form of well-founded induction principle, but the definitions of ordinals that are classically equivalent turn out to not be equivalent intuitionistically, and I can't find a proper reference explaining the relationship among them.

Any references explaining these issues are also very welcome.

Answer 1

In the homotopy type theory book, the following definition is used:

• Given a binary relation $<$ on a set $A$, the set of accessible elements of $A$ is the smallest subset $X \subseteq A$ with the following property: if $a$ is an element of $A$ and for all $b < a$ we have $b \in X$, then $a \in X$ as well.
• A binary relation on a set $A$ is well-founded if every element of $A$ is accessible.
• An ordinal is a set with an extensional well-founded transitive binary relation.

This can be interpreted in any elementary topos in a straightforward way, but I do not know how useful ordinals are in the intuitionistic context.

Answer 2

In intuitionistic logic there are several different ways to define the notion of ordinal, depending on what property you want, and in general these notions are not equivalent. For a good description of these different definitions and their relations you can check out Paul Taylors Intuitionistic Sets and Ordinals