Proper definition of ordered field in constructive mathematics The nLab article on ordered fields defines ordered fields to be a field $K$ with a strict linear order $<$ such that $0 < 1$ and for all elements $a \in K$ and $b \in K$, if $a > 0$ and $b > 0$ then $a + b > 0$ and $a \cdot b > 0$. The nLab article goes on to claim that this definition is also valid in constructive mathematics.
In classical mathematics, the relation $\leq$ defined as $a \leq b := \neg (b < a)$ could be proved to be a total order, and thus a lattice with binary meets $\min$ and joins $\max$. However, in constructive mathematics, $\leq$ cannot be proved to be a total order without excluded middle, although it still can be proved that $\leq$ is a partial order. As a result, it isn't provable that the field $K$ has lattice structure.
The nLab article does not provide any sources that ordered fields in constructive mathematics do not have a lattice structure $(K, \leq, \min, \max)$. On the other hand, I have found two sources in the constructive mathematics literature where the definition of ordered field explicitly has lattice structure:

*

*Univalent Foundations Project (2013), Homotopy Type Theory -- Univalent Foundations of Mathematics, section 11.2.1, pdf

*Auke B. Booij (2020), Analysis in univalent type theory (2020), section 4.1, pdf
Are there any references in the constructive mathematics literature which define ordered fields without the lattice structure?
Edit: The nLab article on ordered fields has been edited to say that in constructive mathematics there are multiple definitions of an ordered field. However, the original definition provided in the first paragraph remains unsourced.
 A: The word "constructive" has many variations. Some might even say that it's a moving target. This is not a one-size-fits-all situation, so I would contend that maybe the proper definition of ordered field changes from one context to context. This is not immediately clear since there are ubiquitous ordered fields like $\mathbb Q$, $\mathbb R$, and maybe more. The varieties of constructivism could conceivably be forced to agree on the basis of this common ground. This is not the case: here are two contexts which superficially appear to be closely connected but diverge on whether an ordered field should have a lattice structure or not.
The first context is constructive real analysis. Infinite sequences and their convergence are at the very heart of this topic. In this context, it is essential that $\mathbb R$ be Cauchy complete (at least in the weak sense that a Cauchy sequence with a modulus of convergence has a limit). In another answer, I argued that this ensures that $\mathbb R$ has a lattice structure. So, in this context, the lattice structure is quite natural and a practitioner might be tempted to disregard ordered fields without lattice structure as mere curiosities.
The second context is smooth infinitesimal analysis. This isn't what is normally meant by "constructivism" but the idea does have some constructive roots, albeit with perhaps stronger roots in nonstandard analysis. Also models of smooth infinitesimal analysis take the form of smooth toposes. [SIA is not really my cup of tea, perhaps someone with more intimate knowledge could provide a better defense or rebuttal(!) of SIA as a variety of constructivism.] Now, in any such model, $\mathbb R$ cannot have a lattice structure since that directly leads to functions that are not smooth, e.g. $|x| = \max(x,-x)$. Nevertheless, $\mathbb R$ has a reasonable ordered structure and a practitioner would like this to be an ordered field.
This is definitely not the strongest argument I've ever made but this does provide good evidence that there is no "proper definition of ordered field in constructive mathematics", or even a proper definition of ordered field in constructive analysis if "analysis" is understood in a broader sense that includes both real analysis and differential geometry.
