IN CONSTRUCTION
Note that, we will start off with introduction of homotopy theory. Since I haven’t been exposed to topology, that would be very interesting.
The current target is to understand P78,79 of the HoTT Book completely.
I think we need to recall some topology concepts here, because the audience might be pure computer science student who can only manipulate axiom and $Proof$ and syntax terms.
Given a topology $X$
Recall
A path between $a, b \in X$ is a continuous function $f: [0,1] \rightarrow X$
Continuous is something only topology can define.
A path $p$ has inverse $p^{-1}$, and two paths $p \centerdot q$ can concatenate to another path.
$Proof$: A concatenation of two path (continuous) functions lead to another path (continuous function).
Now we can define homotopy.
Given $X_ 1, X_ 2$, a homotopy between two continuous functions $p, q: X_ 1 \rightarrow X_ 2$ is a continuous function $H : X_ 1 \times [0,1] \rightarrow X_2$ s.t.
$H(x,0) = p(x)$ and $H(x,1) = q(x) \ \ \forall x$
What’s more, if there is a homotopy between two continuous functions, we say they are homotopic.
It is easy to see when $p,q$ are paths, $H:[0,1] \times [0,1] \rightarrow X_ 2$. In this context, we can say $H$ is a 2-dimensional path between paths.
Interestingly, since product is the left adjoint of the exponential, it is basically mapping $[0,1]$ to the functional space. But if defined in that way, the definition of continuous is not trivial (for me).
$Proof$: Homotopy is an equivalent relationship (on the set of all continuous function).
$Proof$: Concatenation and inverses respects homotopy equivalence.
Example: $p \centerdot p^{-1}$ can be shrinked into the identity path (i.e. $_ \mapsto p(0)$)
Now let’s focus on homotopy on path.
More definition,
When $H : [0,1] \times [0,1] \rightarrow X$ is a homotopy (between path),
if $H(0,t) = x$ and $H(1,t) = y$ for all $t$ (i.e. for each fixed $t$, $H(\cdot, t)$ is again a path from $x$ to $y$)
then $H$ is said to be endpoint preserving (rel ending).
Now:
A path-homotopy is an endpoint preserving homotopy between paths;
A loop-homotopy is a path homotopy when the path is a loop (i.e. start and end at the same point)
The terminology here is a little confusing since path-homotopy is a stronger notion than a homotopy between paths.
$Proof$: Path-homotopy is again an equivalence relation; this equivalence class is called homotopy equivalence class.
$Proof$: These homotopy equivalence class of loops at the same point (say $x_0$) forms a group, we call it fundamental group.
Another definition:
Two spaces are homotopy equivalent when
there are continuous maps back and forth whose composites are homotopic to the identity map
$Proof$: Homotopy equivalent spaces has isomorphic fundamental groups.
We seem to have enough homotopy knowledge, where we can abstract the analytic details and proceed axiomatically – I hope one day I can introduce the concept of $\infty$-groupoid.
I may give up HoTT for a while because I am going to get a PhD and there is no programming language focus on the study of HoTT yet (more mathematical foundational focus). The next topic should be a deep investigation of “Lecture on Curry Howard Correspondence” – the syntacital approach (and the most tranditional approach) to the type theory.