Homotopy Type Theory Dedekind complete Archimedean ordered field > history (Rev #3)

Defintion

An Archimedean ordered field FF is Dedekind complete if

α: 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, if a<ba \lt b, then FF is a subinterval of the union of (a,)(a, \infty) and (,b)(-\infty, b)
ϵ: a:F b:F(a<b)(F((a,)(,b)))\epsilon:\prod_{a:F} \prod_{b:F} (a \lt b) \to (F \subseteq ((a, \infty) \cup (-\infty, b)))
  • 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

References

  • Steve Vickers, “Localic Completion Of Generalized Metric Spaces I”, TAC

Revision on April 22, 2022 at 20:19:43 by Anonymous?. See the history of this page for a list of all contributions to it.