Tutorial 7: Hypertorus Homotopy

In the last tutorial, you learned that normal paths are used to reason about functions similar to how complex numbers are used to reason about real numbers.

For every real number x, there is a complex number:

x + 0 * i

Every function f has a normal path:

f[id] <=> f

In Homotopy Theory, this can be thought of as a loop id around a point f.

The loop is so small that it becomes indistinguishable from the point itself.

Notice! Path Semantics does not require an interpretation in Homotopy Theory to be used for formal theorem proving. A such interpretation is meant to help intuition about cases that are hard to reason about from a normal programming perspective. For example, a loop only works as a correct metaphor when the domain of a function can be sub-divided into contractible sets. You should keep in mind that there are more advanced mathematical arguments behind the Homotopy Theory interpretation.

When we compose normal paths, we project the loop around f onto new loops.

For example:

f[id][g]

Here, we go from the id loop around f to the g loop around f.

In order to do this, we need to relate the two loops with a homotopy:

f[id][g] <=> f[g . id]

The transformation itself, between these two expressions, is the homotopy.

We can always add new loops around points.

However, we can also always add new loops around loops!

For example:

f[g[id]]

Here, id is a torus around the loop g around the point f.

The torus is so small that is becomes indistinguishable from the loop g around the point f.

Similarly, we can create arbitrary higher hypertoruses around points.

f[id[id[id[id[id...]]]]]

Now, f[g] might be another point h:

f[g] <=> h

We can write this in another way:

f[g] <=> h[id]

It means the loop g around f can be substituted with the loop id around h.

In logic, we say that these two loops are propositionally related.

The idea of creating hypertoruses and relate them propositionally, is called "Hypertorus Homotopy".

Hypertorus Homotopy is the interpretation of Homotopy Theory using normal paths.

In the next tutorial, you will learn about holes, tunnels and spheres.