Homotopy Type Theory Sandbox (Rev #21, changes)

Showing changes from revision #20 to #21: 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 power? semiadditive dagger category that is locally a Heyting algebra.

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.

On real numbers, part 2

Real numbers aren’t actually physically real, because they cannot be physically measured in the real world. What are real are estimates of real numbers, which are rational closed intervals. However, rational closed intervals are not a field, because any rational closed interval with zero as a member is not invertible. Like the real numbers, rational closed intervals do not satisfy $=$-trichotomy, instead they only satisfy a weaker version of trichotomy, $[a, b] \lt [c, d]$, $[a, b] \gt [c, d]$, or $[a, b] \cap [c, d]$ is inhabited. Furthermore, it doesn’t satisfy connectedness, which means that $\lt$ is only an asymmetric irreflexive comparison rather than a strict order.

On English grammar

English verb conjugation ought to be like Swedish in that verbs with a singular third person subject are conjugated the same as all other combinations of grammatical person and number, and English pronouns ought to be like Finnish in which there is only one pronoun referring to human beings. Then get rid of as many irregular verb conjugations (i.e. catch-caught, seek-sought, tell-told) as possible. These are just relics of the complex Germanic verb conjugation and noun declension system of Old English.