Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
New page: plump ordinal. Is there a general name for a pair of inequalities and which satisfy the expected laws? They’re kind of weird from a categorical perspective; is a poset (or preorder), of course, and is an endo-profunctor of it, but has a multiplication and a counit, so it’s neither a monad nor a comonad in .
I don't know a name, but there should be one! Another place that this pair comes up is in non-located (one-sided or MacNeille) real numbers.
We can leave transitivity of out of the list of axioms (since it follows in two ways), but we also should add its irreflexivity: If , then False.
An unbiased list of axioms is (in addition to ) this:
The entire forward direction of the second item here is missing from your list; it may be too strong.
I think it is too strong. Consider the ordinal . Then and and , but “ or ” makes P decidable.
(And all those ordinals are plump.)
Another way to say what we’re talking about is that the same set is equipped with both a partial order and a quasiorder in a “compatible” way.
Yes, this would restrict attention to some sort of super-plump ordinal (and so not be for the page plump ordinal).
But I don't exactly understand Taylor's motivation for restricting to plump ordinals in the first place.
I don’t entirely understand his motivation myself, but it seems to be at least partly that he wants a successor satisfying iff . Joyal-Moerdijk also arrived at an equivalent notion of plump ordinal from algebraic-set-theory considerations.
My recent interest in plump ordinals comes from the fact that they embed constructively in the surreals.
My recent interest in plump ordinals comes from the fact that they embed constructively in the surreals.
Yes, I noticed that! I also see that you have a higher inductive definition of plump ordinals themselves. This makes them more interesting to me too.
1 to 9 of 9