Homotopy Type Theory UMyn8W7b (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

Comment about school mathematics

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.