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

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

Idea

< Dedekind completion

Dedekind completeness but without the located requirement.

Defintion

A type FF with a strict order is interval-complete if

  • For all terms a:Fa:F and b:Fb:F, the open interval (a,b)(a,b) is inhabited.
ζ: a:F b:F[(a,b)]\zeta:\prod_{a:F} \prod_{b:F} \left[(a, b)\right]
α: a:F[(a,)]\alpha:\prod_{a:F} \left[(a, \infty)\right]
β: a:F[(,a)]\beta:\prod_{a:F} \left[(-\infty, a)\right]
  • For all terms a:Fa:F and b:Fb:F, a<ba \lt b if and only if (b,)(b,\infty) is a subinterval of (a,)(a,\infty)
γ: a:F b:F(a<b)((b,)(a,)\gamma:\prod_{a:F} \prod_{b:F} (a \lt b) \cong ((b,\infty) \subseteq (a,\infty)

(for all propositions AA and BB, p:(AB)((AB)×(BA))p:(A \cong B) \cong ((A \to B) \times (B \to A)))

  • For all terms a:Fa:F and b:Fb:F, b<ab \lt a if and only if (,b)(-\infty,b) is a subinterval of (,a)(-\infty,a)
δ: a:F b:F(b<a)((,b)(,a)\delta:\prod_{a:F} \prod_{b:F} (b \lt a) \cong ((-\infty,b) \subseteq (-\infty,a)
  • For all terms a:Fa:F and b:Fb:F, the intersection of (a,)(a,\infty) and (,b)(-\infty,b) is a subinterval of the open interval (a,b)(a,b)
η: a:F b:F((a,)(,b))(a,b)\eta:\prod_{a:F} \prod_{b:F} ((a, \infty) \cap (-\infty, b)) \subseteq (a, b)

See also

Revision on June 10, 2022 at 14:50:21 by Anonymous?. See the history of this page for a list of all contributions to it.