Homotopy Type Theory UMyn8W7b (Rev #13, changes)

Showing changes from revision #12 to #13: Added | Removed | Changed

left Z-modules

A left $\mathbb{Z}$-module is a set $S$ with a term $0:S$ and a binary function $(-)+(-):S \times S \to S$, and a left multiplicative $\mathbb{Z}$-action $(-)\cdot_l(-):\mathbb{Z} \times S \to S$, such that

$$\prod_{a:S} \prod_{b:S} a + b = b + a$$

$$\prod_{a:S} \prod_{b:S} \prod_{c:S} a + (b + c) = (a + b) + c$$

$$\prod_{a:S} 1 \cdot_l a = a$$

$$\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a \cdot b) \cdot_l c = a \cdot_l (b \cdot_l c)$$

$$\prod_{a:S} 0 \cdot_l a = 0$$

$$\prod_{a:\mathbb{Z}} \prod_{b:S} \prod_{c:S} a \cdot_l (b + c) = a \cdot_l b + a \cdot_l c$$

$$\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a + b) \cdot_l c = a \cdot_l c + b \cdot_l c$$

We define the functions $-:S \to S$ and $(-)\cdot_r(-):S \times \mathbb{Z} \to S$ to be

$$-a \coloneqq (-1) \cdot_l a$$

$$a \cdot_r b \coloneqq b \cdot_l a$$

and $S$ is an abelian group and a $\mathbb{Z}$-bimodule

$$a = 1 \cdot_1 a = (1 + 0) \cdot_1 a = (1 \cdot_1 a) + (0 \cdot_1 a) = a + 0$$

$$a = 1 \cdot_1 a = (0 + 1) \cdot_1 a = (0 \cdot_1 a) + (1 \cdot_1 a) = 0 + a$$

$$0 = 0 \cdot_1 a = (1 + -1) \cdot_1 a = (1 \cdot_1 a) + (-1 \cdot_1 a) = a + -a$$

$$0 = 0 \cdot_1 a = (-1 + 1) \cdot_1 a = (-1 \cdot_1 a) + (1 \cdot_1 a) = -a + a$$

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

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

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

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

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

and the initial condition $f(1) = 1$.

In particular, the square root function is defined when $r = \frac{1}{2}$.

The binary power function

The power function $\pow:\mathbb{R}_{+} \times \mathbb{R} \to \mathbb{R}$ written as $\pow(x, y) \coloneqq x^y$ is defined by the following partial differential equations

with the initial conditions $\pow(x, 0) = 1$ and $\pow(1, y) = 1$.