Homotopy Type Theory Sandbox (Rev #18, changes)

Showing changes from revision #17 to #18: 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

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

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

Rel

The 2-poset of sets and binary relations? is a locally posetal? semiadditive dagger category (disjoint that union is and locally empty a set) where composition of relations preserve the poset order,locally posetal?Heyting algebra ,cartesian bicategory? (product set and unit set), and power allegory? (power set) set), whose subobject inclusions form a Heyting algebra, and that every set with an equivalence relation has a quotient set.

Span

The 3-poset of groupoids, spans? between groupoids and binary relations? between spans.

Comments about school mathematics

On real numbers

There are many different types of real numbers, which are suited for different subjects taught in school mathematics.

Linear algebra and some of scalar differential calculus does not need any type of real numbers at all. The rational numbers or any other Archimedean ordered field suffices. Linear algebra is about vector spaces which is defined for general fields.

Archimedean ordered fields suffice for scalar differential calculus, because according to a result by Otto Hoelder, any Archimedean ordered field embeds in the Dedekind real numbers, and therefore is a metric space. The epsilon-delta defintion of a limit of a function is thus well defined for any Archimedean ordered field, and one could define continuous functions, differentiable functions, smooth functions, power series, and analytic functions, as well as ordinary differential equations.

For vector differential calculus and extensions such as geometric differential calculus and tensor differential calculus, one only needs the real constructible numbers or any Euclidean Archimedean ordered field, so that the square root function and the Euclidean metric on the vector space is well defined. For the same reason as for scalar differential calculus, one could define partial derivatives, directional derivatives, the geometric derivative, the div, the curl, systems of ordinary differential equations, and partial differential equations.

For pre-algebra, numerical analysis, the theory of equations, and trigonometry, the Cauchy real numbers suffice. The Cauchy real numbers suffice for pre-algebra and numerical analysis because according to a result by Auke Booij, every Cauchy real number is a Dedekind real number with a locator, and every Dedekind real number with a locator is a Cauchy real number and has an infinite decimal representation. Thus, every Cauchy real number has a locator. Conversely, one could prove that every infinite decimal representation of a real number has a corresponding Cauchy sequence. The Cauchy real numbers suffice for the theory of equations because according to a result by Wim Ruitenberg, the Cauchy real numbers are a real closed field and its algebraic closure is the Cauchy complex numbers. However, this is only true for the Cauchy real numbers. In trigonometry, the transcendental functions such as $\exp$, $\sin$, and $\cos$ are defined as limits of a certain Cauchy sequence or series, and Auke Booij showed that the limit of a sequence of Cauchy real numbers has a locator and is thus a Cauchy real number.

For geometry one needs the Dedekind real numbers because the Dedekind real numbers are the only type of real numbers that are Dedekind complete and connected, or where the shape of the type of real numbers is contractible. The connected components of every other type of real numbers defined above could be shown to be homotopy contractible, and thus the shape of the type is equivalent to the type itself.

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$.