Ord

Stream: maths

[Yaël Dillies]

Am I right in thinking that docs#ordinal forms a category? Do we have something similar somewhere? docs#simplex_category I assume.

[Patrick Stevens]

You mean the category that any partial order induces? Or a different one?

[Yaël Dillies]

I was more thinking about the fact that ordinal is made of linear orders, so we could get morphisms as maps between these linear orders.

[Reid Barton]

The one that comes from the partial order (o -> o' if o <= o') could also be described as given by maps between ordinals that are inclusions of initial segments. You could also allow all nondecreasing maps between ordinals, but then you're not really making any use of the fact that they are ordinals.