It occurs to me that since choice object exists and choice set redirects to it, the link here *should* go to choice set, just in case we ever separate the two. But the other will have to wait until the page is made.

Yep, I just learnt about it from Martín's post there. (And since it's mostly discussed in the context of topos theory rather than constructive set theory, I set the link to Higgs object, much like the link just before it to ‘choice set’ actually goes to choice object.)

]]>The Higgs object $\{ q \colon \Omega \mid \forall p \colon \Omega . p \vee ( p \Rightarrow q) \}$ of Set (see https://mathstodon.xyz/@MartinEscardo/110979071875659866), I guess?

]]>What’s the Higgs set? (I don’t suppose you mean Hartogs number?)

]]>Zmberber’s guest comment in #5 is correct. Classically, the difference between a total order and a linear order is the difference between a weak and strict order, so that's the difference between the first two variations. Although perhaps this would all be easier to understand if we just listed the strict variations and then noted that they could all (classically) be done weakly as well.

]]>Mention the Higgs set as an example of a classical well-order that’s nontrivial in constructive mathematics.

]]>yes but i made the critical mistake that i was not logged in, it was commented as a guest, and i can’t edit that

]]>Amazingly, here you can edit your comments indefinitely. Just hit “edit” at the top right.

]]>Sorry I screwed up the previous comment, (EDIT: and I can’t change it because i wasn’t logged in), I meant to write

$\text{A well-order is precisely } \lneq \text{ for a well-founded total order } \leq$ ]]>There is a subtlety that I believe to be wrong.

The page reads that “a well-order is precisely a well-founded total order”. The way a total order relation is defined in nLab, equality is allowed, and by applying the definition of well-founded relation on say the natural numbers, the empty set would be an inductive subset. So what it should read is that

$\text{ A well-order is precisely $\lneq$ for a well-founded total order $\leq$ }$Or one could just add the notion of a strict order (orders and strict orders are in one to one correspondence), and just say a well-founded strict total order.

]]>I linked well-order and well-quasi-order. I do wonder whether there are constructions that assume an index set needs to be well-ordered that could use the weaker notion. I don’t know the consistency of asking that every set admits a well-quasi-order, but surely it’s weaker than full AC.

]]>At *well-order* I found it non-trivial to extract the usual classical definition. (Before I reached the second-but-last bullet item that states it, I was following a dozen links to other kinds of orderings and their properties).

For the sake of the reader, I have now given the usual definiton the first paragraph in the Definition section (I didn’t remove it from that bullet list).

But I think some expert might still make that entry a bit user-friendly.

]]>Good; I added redirects such as partial map.

]]>I made some edits at well-order. I am removing a query box, having duly extracted some punchlines. These edits also forced an edit to partial function, where I added the generalization to partial maps in any category with pullbacks.

]]>+– {: .query} This need not exist; in particular, $S_a$ may be empty. What do we really want to say here? (We could talk about the successor

ofa well-ordered set.) —Toby Mike: Yeah, or we could say that successor is a partial function. One definition of a limit ordinal is one on which successor is totally defined. =–