Homotopy Type Theory Sandbox (Rev #7, changes)

The geometric definition of an ordered field:

• an ordered local ring $R$ where for all elements $x \in R$, $x$ is invertible or $x = 0$

• equivalently, an ordered local ring which satisfies trichotomy.

The limited principle of omniscience implies that the discrete (i.e. Cauchy, Escardo-Simpson, decidable Dedekind) real numbers are the terminal such an ordered field.

More importantly, it implies that every pointwise continuous function is uniformly continuous via the lesser limited principle of omniscience.