left Z-modules
A left -module is a set with a term and a binary function , and a left multiplicative -action , such that
We define the functions and to be
and is an abelian group and a -bimodule
On functions
The “functions” taught in school mathematics at many levels aren’t functions on a type as presented in type theory, but rather they are partial and/or multivalued “functions”, which are basically just spans on . In school algebra, the reciprocal function for in a field is a partial function and the principal square root function is partial. Many implicit functions are multivalued. In school calculus, the derivative is a partial function on the function type because certain functions are nowhere-differentiable, and the antiderivative implicit function is multivalued even for the zero function .
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 written as is defined by the following differential equation
and the initial condition .
Base logarithms
Given a positive real number , the base logarithm written as is defined by the following differential equation
and the initial condition .
Exponential functions
The exponential function written as is defined by the following differential equation
and the initial condition .
Given a positive real number , the base exponential function written as is defined by the following differential equation
and the initial condition .
Non-integer power functions
Given a real number , the power function written as is defined by the following differential equation
and the initial condition .
In particular, the square root function is defined when .
The binary power function
The power function written as is defined by the following partial differential equations
with the initial conditions and .