Skip to content

Instantly share code, notes, and snippets.

View jul1u5's full-sized avatar
:shipit:

Julius Marozas jul1u5

:shipit:
View GitHub Profile
@JakobBruenker
JakobBruenker / visual.md
Last active January 4, 2024 03:13
The paths of homotopy type theory visualized

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:

image