@Gro-Tsen in type theory one could directly construct the initial Cauchy complete Archimedean ordered field: etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf

@FrançoisG.Dorais According to mathoverflow.net/questions/302037/… the principle of unique choice should be valid in my variety of constructivism.

Minor question, which I probably should have made it clear in the questions above, and in my original reference request, but are the constructive ordered fields here Heyting fields, with respect to the canonical tight apartness relation defined by $a \# b := a \lt b \vee b \lt a$? Other definition of fields do exist which are not Heyting, such as the residue fields from Peter Johnstone's Rings, Fields, and Spectra.

and in constructive mathematics, the join $\max$ and the meet $\min$ are well defined binary operations in the Cauchy real numbers and the Dedekind real numbers, but this follows not from the order structure on the Cauchy or Dedekind real numbers, but from the construction of the Cauchy and Dedekind real numbers in terms of Cauchy sequences of rational numbers and Dedekind cuts respectively.

The issue isn't whether $\leq$ is a total order on the field $K$, but whether every pair of element of $K$ has a join and a meet, which is a weaker condition than $\leq$ being a total order. In the two sources above, the join is written as $\max$ and the meet is written as $\min$, even though $\leq$ is not a total order.