## Stream: maths

### Topic: ordinals

#### Reid Barton (Oct 04 2018 at 18:00):

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 (Oct 04 2018 at 18:05):

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 (Oct 04 2018 at 18:08):

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 (Oct 04 2018 at 18:09):

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 (Oct 04 2018 at 18:10):

I wrote some code a month ago

#### Reid Barton (Oct 04 2018 at 18:10):

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

#### Kenny Lau (Oct 04 2018 at 18:11):

I uploaded them here.

#### Reid Barton (Oct 04 2018 at 18:11):

Oh interesting, will take a look

#### Reid Barton (Oct 04 2018 at 18:15):

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 (Oct 04 2018 at 18:16):

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 (Oct 04 2018 at 18:58):

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

#### Mario Carneiro (Oct 04 2018 at 18:59):

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

Last updated: May 12 2021 at 08:14 UTC