8.1.5 The homotopy-theoretic proof

In sec:pi1s1-universal-cover, we defined the putative universal cover $\mathrm{𝖼𝗈𝖽𝖾}:{𝕊}^1\to 𝒰$ in type theory, and in subsec:pi1s1-homotopy-theory we defined a map $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}:{\prod }_{(x:{𝕊}^1)}(\mathrm{𝖻𝖺𝗌𝖾}=x)\to \mathrm{𝖼𝗈𝖽𝖾}(x)$ from the path fibration to the universal cover.What remains for the classical proof is to show that this map induces an equivalence on total spaces because both are contractible, and to deduce from this that it must be an equivalence on each fiber.

In thm:contr-paths we saw that the total space ${\sum }_{(x:{𝕊}^1)}(\mathrm{𝖻𝖺𝗌𝖾}=x)$ is contractible.For the other, we have:

Lemma 8.1.1.

The type ${\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}\mathrm{)}}\mathrm{code}\mathit{}\mathrm{(}x\mathrm{)}$ is contractible.

Proof.

We apply the flattening lemma (thm:flattening) with the following values:

• $A:\equiv \mathrm{𝟏}$ and $B:\equiv \mathrm{𝟏}$, with $f$ and $g$ the obvious functions.Thus, the base higher inductive type $W$ in the flattening lemma is equivalent to ${𝕊}^1$.

• $C:A\to 𝒰$ is constant at $\mathbb{Z}$.

• $D:{\prod }_{(b:B)}(\mathbb{Z}\simeq \mathbb{Z})$ is constant at $\mathrm{𝗌𝗎𝖼𝖼}$.

Then the type family $P:{𝕊}^1\to 𝒰$ defined in the flattening lemma is equivalent to $\mathrm{𝖼𝗈𝖽𝖾}:{𝕊}^1\to 𝒰$.Thus, the flattening lemma tells us that ${\sum }_{(x:{𝕊}^1)}\mathrm{𝖼𝗈𝖽𝖾}(x)$ is equivalent to a higher inductive type with the following generators, which we denote $R$:

• A function $𝖼:\mathbb{Z}\to R$.

• For each $z:\mathbb{Z}$, a path ${𝗉}_z:𝖼(z)=𝖼(\mathrm{𝗌𝗎𝖼𝖼}(z))$.

We might call this type the homotopical reals;it plays the same role as the topological space $ℝ$ in the classical proof.

Thus, it remains to show that $R$ is contractible.As center of contraction we choose $𝖼(0)$; we must now show that $x=𝖼(0)$ for all $x:R$.We do this by induction on $R$.Firstly, when $x$ is $𝖼(z)$, we must give a path $q_z:𝖼(0)=𝖼(z)$, which we can do by induction on $z:\mathbb{Z}$:

$q_0$$:\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{𝖼(0)}$

$q_{n+1}$$:\equiv q_n{𝗉}_n$for $n\ge 0$

$q_{n-1}$$:\equiv q_n𝗉_{n-1}{}^{-1}$for $n\le 0$.

Secondly, we must show that for any $z:\mathbb{Z}$, the path $q_z$ is transported along ${𝗉}_z$ to $q_{z+1}$.By transport of paths, this means we want $q_z{𝗉}_z=q_{z+1}$.This is easy by induction on $z$, using the definition of $q_z$.This completes the proof that $R$ is contractible, and thus so is ${\sum }_{(x:{𝕊}^1)}\mathrm{𝖼𝗈𝖽𝖾}(x)$.∎

Corollary 8.1.2.

The map induced by $\mathrm{encode}$:

$${\sum }_{(x:{𝕊}^1)}(\mathrm{𝖻𝖺𝗌𝖾}=x)\to {\sum }_{(x:{𝕊}^1)}\mathrm{𝖼𝗈𝖽𝖾}(x)$$

is an equivalence.

Proof.

Both types are contractible.∎

Theorem 8.1.3.

$\mathrm{\Omega }({𝕊}^1,\mathrm{𝖻𝖺𝗌𝖾})\simeq \mathbb{Z}$.

Proof.

Apply thm:total-fiber-equiv to $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$, using thm:encode-total-equiv.∎

In essence, the two proofs are not very different: the encode-decode one may be seen as a “reduction” or “unpackaging” of the homotopy-theoretic one.Each has its advantages; the interplay between the two points of view is part of the interest of the subject.