analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A notion of real numbers that is sequentially modulated Cauchy complete, because the modulated Cauchy real numbers are not sequentially modulated Cauchy complete in constructive mathematics
Note: everything in this particular section was copied from the Sandbox of the HoTT wiki and is likely to be original research.
The HoTT book real numbers is the (homotopy)-initial sequentially Cauchy complete Archimedean ordered pointed halving group. There should be a corresponding definition as a higher inductive-inductive type, but that still has to be worked out.
We define a sequentially Cauchy complete Archimedean ordered pointed halving group below as follows:
A pointed abelian group is a set $A$ with an element $1:A$ called one and a binary operation $(-)-(-):A \times A \to A$ called subtraction such that
for all elements $a:A$, $a - a = 1 - 1$
for all elements $a:A$, $(1 - 1) - ((1 - 1) - a) = a$
for all elements $a:A$ and $b:A$, $a - ((1 - 1) - b) = b - ((1 - 1) - a)$
for all elements $a:A$, $b:A$, and $c:A$, $a - (b - c) = (a - ((1 - 1) - c)) - b$
$0$ is defined as $1 - 1$, $-a$ is defined as $0 - a$, and $a + b$ is defined as $a - (-b)$. It is left to the reader as an exercise to prove from the given axioms and definitions that $(A,0,+,-,1)$ is an abelian group with an extra point $1$.
A pointed halving group is a pointed abelian group G with a function $(-)/2:G \to G$ called halving or dividing by two such that for all elements $g:G$, $g/2 = g - g/2$.
A pointed halving group $R$ is a strictly ordered pointed abelian group if it comes with a type family $\lt$ such that
The homotopy initial strictly ordered pointed halving group is the dyadic rational numbers $\mathbb{D}$.
A strictly ordered pointed halving group $A$ is an Archimedean ordered pointed halving group if for all elements $a:A$ and $b:A$, if $a \lt b$, then there merely exists a dyadic rational number $d:\mathbb{D}$ such that $a \lt h(d)$ and $h(d) \lt b$.
Let
be the positive dyadic rational numbers.
A sequence in $A$ is a function $x:\mathbb{N} \to A$.
A sequence $x:\mathbb{N} \to A$ is a Cauchy sequence if for all positive dyadic rational numbers $\epsilon:\mathbb{D}_{+}$, there merely exists a natural number $N:\mathbb{N}$ such that for all natural numbers $i:\mathbb{N}$ and $j:\mathbb{N}$ such that $N \leq i$ and $N \leq j$, $x_i - x_j \lt \epsilon$ or $x_j - x_i \lt \epsilon$.
An element $l:A$ is said to be a limit of the sequence $x:\mathbb{N} \to A$ if for all positive dyadic rational numbers $\epsilon:\mathbb{D}_{+}$, there merely exists a natural number $N:\mathbb{N}$ such that for all natural numbers $i:\mathbb{N}$ such that $N \leq i$, $x_i - l \lt \epsilon$ or $l - x_i \lt \epsilon$
$A$ is sequentially Cauchy complete if every Cauchy sequence in $A$ merely has a limit.
Let $F$ be an Archimedean field. $F$ is sequentially modulated Cauchy complete if every Cauchy sequence in $F$ with a modulus of convergence converges. The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of sequentially modulated Cauchy complete Archimedean fields.
The set of HoTT book real numbers $\mathbb{R}_H$ is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.
Let $\mathbb{Q}$ be the rational numbers and let
be the positive rational numbers. The HoTT book real numbers $\mathbb{R}_H$ are inductively generated by the following:
a function $inj: \mathbb{Q} \to \mathbb{R}_H$
a function $lim: C(\mathbb{R}_H) \to \mathbb{R}_H$, where $C(\mathbb{R}_H)$ is the type of Cauchy approximations in $\mathbb{R}_H$.
a dependent family of terms
and the premetric type family $\sim$ is simultaneously inductively generated by the following:
a dependent family of terms
a dependent family of terms
a dependent family of terms
a dependent family of terms
a dependent family of terms
The analytic functions, such as the exponential function, the sine function, and the cosine function are well defined in the HoTT book real numbers, since all modulated Cauchy sequences converge in the HoTT book real numbers.
Last revised on July 2, 2022 at 11:05:40. See the history of this page for a list of all contributions to it.