ordinals

Stream: maths

[Reid Barton]

If I am interested in sequences indexed by $\{\,\alpha \mid \alpha \le \gamma\,\}$ for varying ordinals $\gamma$, is it likely to be more convenient to just work with sequences indexed by arbitrary well-ordered sets?
The problem I found is that if you just write down { \a // \a \le \g }, it lives in the wrong universe.

[Reid Barton]

I think the alternative is to use quot.out to turn an ordinal into a well-ordered set of that order type, where in math I'd just use the set of smaller ordinals.

[Reid Barton]

But if I use quot.out then I basically get an arbitrary well-ordered set anyways, so I might as well just work with an arbitrary well-ordered set from the start, I guess.

[Johannes Hölzl]

Oh yes, I would expect that its far easier assume that γ is a type with well-order. And use the elements of the type as indices.

[Kenny Lau]

I wrote some code a month ago

[Reid Barton]

And if I use the variable name γ, then everyone is happy :)

[Kenny Lau]

I uploaded them here.

[Reid Barton]

Oh interesting, will take a look

[Reid Barton]

I'm going to need to take colimits indexed by these partially ordered sets of ordinals less than $\gamma$--that's why I need the type to live in the correct universe

[Reid Barton]

I think the ZFC stuff would also leave me in the wrong universe, though maybe I could prove once and for all that categories which admit small colimits also admit colimits by "categories in ZFC", or something like that...

[Mario Carneiro]

You can measure the cofinality of any preorder, I think. Maybe it's easier to work without even using well orders

[Mario Carneiro]

but yes, you almost certainly want to reason about ordered types rather than ordinals directly