Homotopy Type Theory interval-complete strict order > history (Rev #1)

Idea

Dedekind completeness but without the located requirement, resulting in an Archimedean ordered field that behaves like the arithmetic of closed intervals on the rational numbers.

Defintion

An Archimedean ordered field $F$ is interval-complete if

For all terms $a:F$ , the lower bounded open interval $(a,\infty)$ is inhabited.

\alpha:\prod_{a:F} \left[(a, \infty)\right]

For all terms $a:F$ , the upper bounded open interval $(-\infty,a)$ is inhabited.

\beta:\prod_{a:F} \left[(-\infty, a)\right]

For all terms $a:F$ and $b:F$ , $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$

\gamma:\prod_{a:F} \prod_{b:F} (a \lt b) \cong ((b,\infty) \subseteq (a,\infty)

(for all propositions $A$ and $B$ , $p:(A \cong B) \cong ((A \to B) \times (B \to A))$ )

For all terms $a:F$ and $b:F$ , $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$

\delta:\prod_{a:F} \prod_{b:F} (b \lt a) \cong ((-\infty,b) \subseteq (-\infty,a)

For all terms $a:F$ and $b:F$ , the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of the open interval $(a,b)$

\eta:\prod_{a:F} \prod_{b:F} ((a, \infty) \cap (-\infty, b)) \subseteq (a, b)

Homotopy Type Theory interval-complete strict order > history (Rev #1)

Idea

Defintion

See also