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

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

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~~ Dedekind real numbers.

Defintion

An Archimedean ordered ~~field~~ integral domain $F$ is interval-complete if

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

α ζ : \prod_{a : F} [(a, ∞)] \prod_{b : F} [(a, b)]

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

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

β α : \prod_{a : F} [(- ∞, a, ∞)]

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

For all terms $a:F$ , ~~and~~ the ~~$b:F$~~ upper bounded open interval , $(- ∞, a <) b$ a (-\infty,a) ~~\lt~~ b if is ~~and~~ inhabited. ~~only~~ if ~~$(b,\infty)$~~ ~~is a subinterval of~~ ~~$(a,\infty)$~~

γ β : \prod_{a : F} \prod_{b : F} [(- ∞, a)] (a < b) ≅ ((b, ∞) \subseteq (a, ∞)

~~\gamma:\prod_{a:F}~~ \beta:\prod_{a:F} ~~\prod_{b:F}~~ \left[(-\infty, (a a)\right] ~~\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$ , $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$

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

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

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

(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$ , ~~the~~ ~~intersection~~ of $(b < a, ∞)$ ~~(a,\infty)~~ b \lt a if and only if $(-\infty,b)$ is a subinterval of ~~theopen interval~~ $(-\infty,a)$ ~~$(a,b)$~~

η δ : \prod_{a : F} \prod_{b : F} ((b < a, ∞) \cap ≅ ((- ∞, b)) \subseteq (a - ∞, b a)

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

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 #2, changes)

Idea

Defintion

See also