It's three decades since I wrote Intuitionistic Sets and Ordinals, at which time I knew how to express well founded relations as coalgebras, but I had very little understanding of the subject.

In recent years I have come back to this topic and written two substatial draft papers, the second being Ordinals as Coalegbras. So I would encourage people who are interested in constructive or categorical ordinals to look at those works.

Since it's more than three decades since I believed Excluded Middle, I have long since got out of the habit of looking for ways in which the classical ideas might almost hold. Really, constructive mathematics is much more interesting when you let it lead you where it wants to go, instead of tracking its heresies against classical logic.

However, I would point out that almost all of the (counter)examples in Ordinals as Coalegbras appear in the simplest non-classical topos, ie presheaves on a single arrow. The classical ideas about ordinals really are very fragile.

I do have a constructive result there (Lemma 9.13) that looks a bit like trichotomy: if the join $x\curlyvee y$ exists with respect to the reflexive(-transitive) closure of the well foundd relation then $x$ and $y$ are comparable ($x\prec y$ or $x=y$ or $y\prec x$).

However, the purpose of writing that paper was not to give a new "official" account of ordinals using category theory, but to destroy the single notion.

The point is that set theory provides partial models for the (non-existent) free algebra for the covariant powerset functor. So there should be other, different kinds of ordinals that do the same for other functors and constructions.

See (http://www.paultaylor.eu/ordinals) for all the papers (including the old ones).

It's three decades since I wrote Intuitionistic Sets and Ordinals, at which time I knew how to express well founded relations as coalgebras, but I had very little understanding of the subject.

In recent years I have come back to this topic and written two substantial draft papers, the second being Ordinals as Coalgebras. So I would encourage people who are interested in constructive or categorical ordinals to look at those works.

Since it's more than three decades since I believed Excluded Middle, I have long since got out of the habit of looking for ways in which the classical ideas might almost hold. Really, constructive mathematics is much more interesting when you let it lead you where it wants to go, instead of tracking its heresies against classical logic.

However, I would point out that almost all of the (counter)examples in Ordinals as Coalgebras appear in the simplest non-classical topos, ie presheaves on a single arrow. The classical ideas about ordinals really are very fragile.

I do have a constructive result there (Lemma 9.13) that looks a bit like trichotomy: if the join $x\curlyvee y$ exists with respect to the reflexive(-transitive) closure of the well founded relation then $x$ and $y$ are comparable ($x\prec y$ or $x=y$ or $y\prec x$).

However, the purpose of writing that paper was not to give a new "official" account of ordinals using category theory, but to destroy the single notion.

The point is that set theory provides partial models for the (non-existent) free algebra for the covariant powerset functor. So there should be other, different kinds of ordinals that do the same for other functors and constructions.

See (http://www.paultaylor.eu/ordinals) for all the papers (including the old ones).

It's three decades since I wrote Intuitionistic Sets and Ordinals, at which time I knew how to express well founded relations as coalgebras, but I had very little understanding of the subject.

In recent years I have come back to this topic and written two substatial draft papers, the second being Ordinals as Coalegbras. So I would encourage people who are interested in constructive or categorical ordinals to look at those works.

Since it's more than three decades since I believed Excluded Middle, I have long since got out of the habit of looking for ways in which the classical ideas might almost hold. Really, constructive mathematics is much more interesting when you let it lead you where it wants to go, instead of tracking its heresies against classical logic.

However, I would point out that almost all of the (counter)examples in Ordinals as Coalegbras appear in the simplest non-classical topos, ie presheaves on a single arrow. The classical ideas about ordinals really are very fragile.

I do have a constructive result there (Lemma 9.13) that looks a bit like trichotomy: if the join $x\curlyvee y$ exists with respect to the reflexive(-transitive) closure of the well foundd relation then $x$ and $y$ are comparable ($x\prec y$ or $x=y$ or $y\prec x$).

However, the purpose of writing that paper was not to give a new "official" account of ordinals using category theory, but to destroy the single notion.

The point is that set theory provides partial models for the (non-existent) free algebra for the covariant powerset functor. So there should be other, different kinds of ordinals that do the same for other functors and constructions.

See (http://www.paultaylor.eu/ordinals) for all the papers (including the old ones).

That page also links to various questions on MathOverflow where I have tried to discuss constructive notions of induction but have received down-votes or more serious abuse. So please go there and give me some up-votes.

It's three decades since I wrote Intuitionistic Sets and Ordinals, at which time I knew how to express well founded relations as coalgebras, but I had very little understanding of the subject.

In recent years I have come back to this topic and written two substatial draft papers, the second being Ordinals as Coalegbras. So I would encourage people who are interested in constructive or categorical ordinals to look at those works.

Since it's more than three decades since I believed Excluded Middle, I have long since got out of the habit of looking for ways in which the classical ideas might almost hold. Really, constructive mathematics is much more interesting when you let it lead you where it wants to go, instead of tracking its heresies against classical logic.

However, I would point out that almost all of the (counter)examples in Ordinals as Coalegbras appear in the simplest non-classical topos, ie presheaves on a single arrow. The classical ideas about ordinals really are very fragile.

I do have a constructive result there (Lemma 9.13) that looks a bit like trichotomy: if the join $x\curlyvee y$ exists with respect to the reflexive(-transitive) closure of the well foundd relation then $x$ and $y$ are comparable ($x\prec y$ or $x=y$ or $y\prec x$).

However, the purpose of writing that paper was not to give a new "official" account of ordinals using category theory, but to destroy the single notion.

The point is that set theory provides partial models for the (non-existent) free algebra for the covariant powerset functor. So there should be other, different kinds of ordinals that do the same for other functors and constructions.

See (http://www.paultaylor.eu/ordinals) for all the papers (including the old ones).