I'm looking for references presenting a constructive treatment of the theory of ordinals. By constructive I mean valid in the internal logic of a topos (so no axiom of choice and no law of excluded middle).

I can easily guess that there is several non equivalent approaches to this question: for example it makes sense to define ordinal as being well ordered sets as such do exist internally in toposes (For example the Higgs object) but this would mean that the natural number object when it exist is not an ordinal.

For this reasons I will clarify a bit what kind of properties I want on ordinals:

The natural number object should be an ordinal.

I want to be able to do proof by induction over ordinals and induction over the natural number object should be a special case of ordinal indcution.

In the topos of sheaf over a topological space $X$ ordinals should be described the following way: For every (classical) ordinal $\alpha$, one can define the sheaf $F_{\alpha}$ over $X$ of (local) continuous functions from $X$ to $\alpha$ (I guess with the order topology on $\alpha$, although I'm open to suggestion on that point). If $\alpha' > \alpha$ there is a canonical inclusion $F_{\alpha} \hookrightarrow F_{\alpha'}$ and one can define $Ord_X$ as the (large) sheaf obtain as the union of all the $F_{\alpha}$. Ordinals over $X$ should corresponds to sections of this large sheaf $Ord_{X}$.

One should be able to pullback ordinal along geometric morphisms (although it might not be exactly a pullback of sheaf), and if $f$ is a bounded geometric morphism there should be an operation of pushforward of ordinals, right adjoint to the pullback for the order relation.

Maybe ordinal of the effective topos are related to recursive ordinal ? (this is suggested by the look of the NNO of the effective topos, but this last one is just a guess)

I'm relatively convince that such a notion exists, and the third point can be used to answer any question that one might have about the properties ordinals should have (at least for the "geometric" properties): For example, it should not be expected that ordinals are totaly ordered, but any two ordinals should have a supremum (because the function max(a,b) is continuous in the order topology but $\{a \leqslant b \}$ is not open in $\alpha \times \alpha$).

What I was wondering is if this kind of constructive theory of ordinals has been already developed and appears in the literature or not ?

Edit : It seems that the more restricitve notion of Ordinals among those that has been proposed in answer and comment is Paul Taylor notion of Plump ordinals (with an equivalent inductive-indutive definition in type theory given here ) but this definition seems already too weak for what I had in mind : one has the following Plump ordinals $0 = \emptyset$, $1 = \{ \emptyset \}$, $2 = \Omega$, $3 = \{$Initial segement of $\Omega \}$, $n = \{ $ Initial segment of $ n -1 \}$. And as any element of an ordinal is again ordinal there is already way too many of them to be describe by a geometric theory as I mentioned in my third point (the elements of $3$ are already non geometric). SO there must be a more restrictive notion but it seems that no one has considered it yet...

Homotopy type theory? $\endgroup$1more comment