Homotopy Type Theory Sandbox (Rev #9)

The rational numbers are a Cauchy space and also a uniform space. They are also a vector space, and depending on which definition of limit is used, limits do exist for some rational sequences and nets, and so some infinitely-differentiable functions and analytic functions over the rational numbers exist. However, they are not Cauchy-complete.

Comments about school mathematics

On functions

The “functions” taught in school mathematics at many levels aren’t functions on a type $T$ as presented in type theory, but rather they are partial and/or multivalued “functions”, which are basically just spans on $T$. In school algebra, the reciprocal function $\frac{1}{x}$ for $x:F$ in a field $F$ is a partial function and the principal square root function $\sqrt{x}$ is partial. Many implicit functions are multivalued. In school calculus, the derivative $\frac{\partial}{\partial x}$ is a partial function on the function type $\mathbb{R} \to \mathbb{R}$ because certain functions are nowhere-differentiable, and the antiderivative implicit function $\frac{\partial^{-1}}{\partial x^{-1}}$ is multivalued even for the zero function $f(x) \coloneqq 0$.

Thus, in this particular context, I would rather prefer to use the homotopy theoretic terminology instead of the type theoretic terminology in many cases, i.e. the objects of the object theory are “spaces” rather than “types”, “points” rather than “terms”, “path spaces” rather than “identity types”, “mappings” rather than “functions”, “mapping spaces” rather than “function types”, and so forth.

On continuous functions

The domains and codomains of (pointwise and uniform) continuous functions are not required to be “continuous” in the sense of not having gaps in the space. The former sense is a concept pertaining to general convergence spaces, while the latter sense of continuous is a concept pertaining to compact Hausdorff connected spaces. For example, the identity function is pointwise and uniform continuous on the p-adic rational numbers with the usual absolute value topology, but the p-adic rational numbers with the usual absolute value topology is totally disconnected and thus not continuous.