Homotopy Type Theory Sandbox (Rev #4)

Rant 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 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 square root function $\sqrt{x}$ is partial and 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 $\frac{\partial^{-1}}{\partial x^{-1}}$ is multivalued even for the zero function $f(x) \coloneqq 0$.

see: Fred Richman’s Algebraic functions, calculus style