Homotopy Type Theory Sandbox (Rev #25, changes)

Showing changes from revision #24 to #25: Added | Removed | Changed

Span Classical mathematics in predicative constructive Homotopy Type Theory

The An 3-poset attempt of to construct the classical Dedekind real numbers in predicative constructive mathematics, and perhaps to show that it is not Dedekind complete constructively or predicatively…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.