Homotopy Type Theory Sandbox (Rev #5, changes)

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

Rant 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 combinatorial spans directed graphs 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 partial. and 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$.

see: Thus, Fred in Richman’s 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.Algebraic functions, calculus style