UniMath
definition of well ordered set
My definition of well ordered set is this:
Definition hasSmallest {X : UU} (R : hrel X) : hProp
:= ∀ S : hsubtype X, (∃ x, S x) ⇒ ∃ x:X, S x ∧ ∀ y:X, S y ⇒ R x y.
Definition isWellOrder {X : hSet} (R : hrel X) : hProp := isTotalOrder R ∧ hasSmallest R.
But an alternative definition would be to say that any subset S of X with the property that an element x of X lies in S if all elements less than x lie in S, is all of X, together with the condition that two elements sharing the same predecessors are equal. That's the definition in
Richman, Fred The constructive theory of countable abelian p-groups. Pacific J. Math. 45 (1973), 621–637.
Perhaps if we adopt this definition, there will be fewer uses of LEM.
@DanGrayson Generally, is the hope to minimize uses of LEM? If so, perhaps this should be noted in your PR #999, where I was surprised to see that it is broadly accepted. Perhaps a phrase like "accepted with reservations" would be more accurate?
Well, we don't want to discourage people interested in formalizing classical mathematics, so I wouldn't use the word "reservations". I'd be happy to make the point that the underlying framework is constructive, except for the Univalence Axiom as used with Coq until it's cubical, so those who want to pursue constructive proofs can do so easily if they omit AC and LEM.
The alternative by Fred Richman is indeed better for constructive purposes. This is also in a chapter in the HoTT book, half of which is constructive, where the non-constructive part proves the equivalence with the classical notion. I also developed some new constructive results about ordinals, in Agda, There are 7 files Ordinal*.lagda here https://github.com/martinescardo/TypeTopology/tree/master/source , where one of them does the constructive part of the HoTT Book (OrdinalOfOrdinals). For browsing purposes, perhaps it is better to look here: http://www.cs.bham.ac.uk/~mhe/agda-new/index.html
