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.

2more comments