Homotopy Type Theory Sandbox (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Test Rant about school mathematics

testing The stuff “functions” here 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$.