# Homotopy Type Theory interval-complete strict order > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

## Idea

Dedekind completeness but without the located requirement.

## Defintion

A type $F$ with a strict order is interval-complete if

• For all terms $a:F$ and $b:F$, the open interval $(a,b)$ is inhabited.
$\zeta:\prod_{a:F} \prod_{b:F} \left[(a, b)\right]$
• 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)$