## 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. ### Function definitions ### #### Natural logarithm #### The natural logarithm $f:\mathbb{R}_{+} \to \mathbb{R}$ written as $f(x) \coloneqq \ln(x)$ is defined by the following differential equation $$\frac{\partial}{\partial x} f(x) = \frac{1}{x}$$ and the initial condition $f(1) = 0$. #### Base $r$ logarithms #### Given a positive real number $r:\mathbb{R}_{+}$, the base $r$ logarithm $f:\mathbb{R}_{+} \to \mathbb{R}$ written as $f(x) \coloneqq \log_r(x)$ is defined by the following differential equation $$\frac{\partial}{\partial x} f(x) = \frac{1}{\ln(r) x}$$ and the initial condition $f(1) = 0$. #### Exponential functions #### The exponential function $f:\mathbb{R} \to \mathbb{R}$ written as $f(x) \coloneqq \exp(x)$ is defined by the following differential equation $$\frac{\partial}{\partial x} f(x) = f(x)$$ and the initial condition $f(0) = 1$. Given a positive real number $r:\mathbb{R}_{+}$, the base $r$ exponential function $f:\mathbb{R} \to \mathbb{R}$ written as $f(x) \coloneqq r^x$ is defined by the following differential equation $$\frac{\partial}{\partial x} f(x) = \ln(r) f(x)$$ and the initial condition $f(0) = 1$. #### Non-integer power functions #### Given a real number $r:\mathbb{R}$, the power function $f:\mathbb{R}_{+} \to \mathbb{R}$ written as $f(x) \coloneqq x^r$ is defined by the following differential equation $$\frac{\partial}{\partial x} f(x) = \frac{r}{x} f(x)$$ and the initial condition $f(1) = 1$. In particular, the square root function is defined when $r = \frac{1}{2}$.