The paths of homotopy type theory visualized

visual.md

Path Visualization

As example, we're using the proof that there's a path between homotopy1 and homotopy2 from Exercise 4.

Instead of looking at a circle, let's look at a general path $p$ between some points $x, y : A$, just because it makes it less confusing to visualize. We'll come back to using the circle later on.

A path is a continuous function of type $[0, 1] \rightarrow A$. If we say $x$ is blue and $y$ is red, we can visualize the path $p$ as a colored image of the interval:

$p^{-1}$ would be going the other way:

We can say that path concatenation splits the image in two halves and compresses each of the two paths, so e.g. $p \cdot p^{-1}$ would be

And the first endpoint of homotopies 1 and 2, $(p \cdot p^{-1}) \cdot p$, would be

Note how the second instance of $p$ in the last image is twice as wide as the first one, because the first one is inside a nested concatenation and thus compressed twice.

Homotopy 1

Let's define

  homotopy1 : (loop ∙ ! loop) ∙ loop ≡ loop
  homotopy1 = (loop ∙ ! loop) ∙ loop ≡⟨ ap (_∙ loop) (!-inv-r loop) ⟩
              refl _ ∙ loop          ≡⟨ ∙unit-l loop ⟩
              loop                   ∎

Though note again that we're using $p$ for now instead of $\text{loop}$.

This means we first transform the left part of the path into refl, and then transform it such that $p$ is the entire path rather than just the right-hand side:

$\qquad \qquad \qquad \qquad \qquad \downarrow$

$\qquad \qquad \qquad \qquad \qquad \downarrow$

We can visualize this as one two-dimensional continuous path:

We can take any horizontal slice of this image and it should still be a valid path from $x$ to $y$, e.g.

is a path that starts at $x$, moves only partway along $p$, goes back to $x$ and finally goes all the way along $p$ to $y$.

Note that the left and right edges in this square should stay constant - otherwise, the horizontal slices wouldn't be paths between $x$ and $y$.

Homotopy 2

We can do the same with the other homotopy:

  homotopy2 : (loop ∙ ! loop) ∙ loop ≡ loop
  homotopy2 = (loop ∙ ! loop) ∙ loop  ≡⟨ ! (∙assoc loop (! loop) loop) ⟩
               loop ∙ (! loop ∙ loop) ≡⟨ ap (loop ∙_) (!-inv-l loop) ⟩
               loop ∙ refl _          ≡⟨ ∙unit-r loop ⟩
               loop                   ∎

means

$\qquad \qquad \qquad \qquad \qquad \downarrow$

$\qquad \qquad \qquad \qquad \qquad \downarrow$

$\qquad \qquad \qquad \qquad \qquad \downarrow$

Or, as one image:

A Path Between

In the exercise, we were supposed to prove that homotopies 1 and 2 are equal. We can do this by showing that there's a continuous transformation between them:

Here, too, all (four) edges should stay as they are, we're only changing the interior of the square.

As before, we can take any slice of this and it will be another valid homotopy, e.g.

goes via paths that move towards the middle of $p$, hang out there for a while, and only then continue on to $y$.

Back to Loops

Let's look at this again, but with $S^1$, as in the exercise.

Let's say the $\text{base}$ point is black, and the $\text{loop}$ moves through cyan and blue, before going back to $\text{base}$:

Note that we have to move through two colors (other than black), to ensure that $\text{loop}$ is not the same as $\text{loop}^{-1}$.

The rest works much the same, so homotopy 1 is

and homotopy 2 is this:

A possible transformation between them looks like this:

Counterexamples

Sphere

These are some nice examples of when paths are homotopic, but when are they not?

To illustrate, let's define one particular version of the 2-Sphere: We can take the loop and add two paths, both from $\text{refl}_\text{base}$ to $\text{loop}$. This essentially means we're adding an upper and lower hemisphere.

Let's say the upper hemisphere moves through yellow:

and the lower hemisphere moves through fuchsia:

When looking at these, remember that only the bottom edge is $\text{loop}$, so the left, right, and top edge are all collapsed onto the $\text{base}$ point.

If we really want to have a sphere, rather than a ball or a disk, we must not be able to construct a continuous transformation between these hemispheres.
Now, you might be thinking, that's easy - just crossfade between the images:

That seems to work - but we move through colors that aren't on any path we've defined:

This is neither yellow nor purple, and thus neither on the upper nor the lower hemisphere. Effectively, we can't just move through empty space - our transformation has to stick to the surface we have.

More on the circle

When you see an image like this, of $\text{loop} \cdot \text{loop}^{-1}$:

You might think you should be able to transform that into an image that has $\text{loop} \cdot \text{loop}^{-1}$ at the top, but only $\text{loop}$ at the bottom, by turning the blue color black, and the cyan color first blue and then black, somewhat like this:

However, we wouldn't expect to be able to show that there's a path between $\text{loop}$ and $\text{loop} \cdot \text{loop}^{-1}$... The image might look reasonable at first, but the problem is that on the right border, there is a region where a color between cyan and blue touches black - and thus this region must contain a color that's not part of the $\text{loop}$, since no such transition exists there.

If I actually try to do this in the script I've been using to visualize these instead of faking it, this is what I get:

Note how it changes the color of the border, which means in the middle, we actually have a path from $\text{base}$ to some point in the middle of the $\text{loop}$, rather than from $\text{base}$ to $\text{base}$.

Maybe you think that the fake path looks suspiciously similar to the cyan-blue region in the background in the hemisphere paths from above - and you'd be right. The difference is that there, we are defining new paths, so we can use new colors, rather than ones we've used before.

Another consequence of this is that for the hemispheres, you cannot crossfade from yellow to black to fuchsia, since then you'd again have a transition from a blue-cyan mixture to black.