8.1.5 The homotopy-theoretic proof

In \autorefsec:pi1s1-universal-cover, we defined the putative universal cover $\mathsf{code}:\mathbb{S}^{1}\to\mathcal{U}$ in type theory, and in \autorefsubsec:pi1s1-homotopy-theory we defined a map $\mathsf{encode}:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{% \textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(% x:\mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}(\mathsf{base}=x)\to\mathsf{code}(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 \autorefthm:contr-paths we saw that the total space $\mathchoice{\sum_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb% {S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:% \mathbb{S}^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x% :\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}{% \mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}(\mathsf{base}=x)$ is contractible. For the other, we have:

Lemma 8.1.1.

The type $\mathchoice{\sum_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb% {S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:% \mathbb{S}^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x% :\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}{% \mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}\mathsf{code}(x)$ is contractible.

Proof.

We apply the flattening lemma (\autorefthm:flattening) with the following values:

•

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

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

$D:\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:% B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}(\mathbb{Z}\simeq\mathbb{Z})$ is constant at $\mathsf{succ}$ .

Then the type family $P:\mathbb{S}^{1}\to\mathcal{U}$ defined in the flattening lemma is equivalent to $\mathsf{code}:\mathbb{S}^{1}\to\mathcal{U}$ . Thus, the flattening lemma tells us that $\mathchoice{\sum_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb% {S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:% \mathbb{S}^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x% :\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}{% \mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}\mathsf{code}(x)$ is equivalent to a higher inductive type with the following generators, which we denote $R$ :

•

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

For each $z:\mathbb{Z}$ , a path $\mathsf{p}_{z}:\mathsf{c}(z)=\mathsf{c}(\mathsf{succ}(z))$ .

We might call this type the homotopical reals; it plays the same role as the topological space $\mathbb{R}$ in the classical proof.

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

$\displaystyle q_{0}$	$\displaystyle:\!\!\equiv\mathsf{refl}_{\mathsf{c}(0)}$
$\displaystyle q_{n+1}$	$\displaystyle:\!\!\equiv q_{n}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{p}_{n}$	for $n\geq 0$
$\displaystyle q_{n-1}$	$\displaystyle:\!\!\equiv q_{n}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{p}_{n-1}}^{-1}}$	for $n\leq 0$ .

Secondly, we must show that for any $z:\mathbb{Z}$ , the path $q_{z}$ is transported along $\mathsf{p}_{z}$ to $q_{z+1}$ . By transport of paths, this means we want $q_{z}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathsf{p}_{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 $\mathchoice{\sum_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb% {S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:% \mathbb{S}^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x% :\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}{% \mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}\mathsf{code}(x)$ . ∎

Corollary 8.1.2.

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

\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}(\mathsf{base}=x)\to% \mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}\mathsf{code}(x)

is an equivalence.

Proof.

Both types are contractible. ∎

Theorem 8.1.3.

$\Omega(\mathbb{S}^{1},\mathsf{base})\simeq\mathbb{Z}$ .

Proof.

Apply \autorefthm:total-fiber-equiv to $\mathsf{encode}$ , using \autorefthm: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.

Title	8.1.5 The homotopy-theoretic proof
\metatable