8.1.3 The universal cover in type theory

Let us consider how we might express the preceding proof in type theory. We have already remarked that the path fibration of $\mathbb{S}^{1}$ is represented by the type family $(x\mapsto(\mathsf{base}=x))$ . We have also already seen a good candidate for the universal cover of $\mathbb{S}^{1}$ : it’s none other than the type family $c:\mathbb{S}^{1}\to\mathcal{U}$ which we defined in \autorefsec:pi1s1-initial-thoughts! By definition, the fiber of this family over $\mathsf{base}$ is $\mathbb{Z}$ , while the effect of transporting around $\mathsf{loop}$ is to add one — thus it behaves just as we would expect from \autoreffig:winding.

However, since we don’t know yet that this family behaves like a universal cover is supposed to (for instance, that its total space is simply connected), we use a different name for it. For reference, therefore, we repeat the definition.

Definition 8.1.1 (Universal Cover of $\mathbb{S}^{1}$ ).

Define $\mathsf{code}:\mathbb{S}^{1}\to\mathcal{U}$ by circle-recursion, with

	$\displaystyle\mathsf{code}(\mathsf{base})$	$\displaystyle:\!\!\equiv\mathbb{Z}$
	$\displaystyle\mathsf{ap}_{\mathsf{code}}({\mathsf{loop}})$	$\displaystyle:=\mathsf{ua}(\mathsf{succ}).$

We emphasize briefly the definition of this family, since it is so different from how one usually defines covering spaces in classical homotopy theory. To define a function by circle recursion, we need to find a point and a loop in the codomain. In this case, the codomain is $\mathcal{U}$ , and the point we choose is $\mathbb{Z}$ , corresponding to our expectation that the fiber of the universal cover should be the integers. The loop we choose is the successor/predecessor isomorphism on $\mathbb{Z}$ , which corresponds to the fact that going around the loop in the base goes up one level on the helix. Univalence is necessary for this part of the proof, because we need to convert a non-trivial equivalence on $\mathbb{Z}$ into an identity.

We call this the fibration of “codes”, because its elements are combinatorial data that act as codes for paths on the circle: the integer $n$ codes for the path which loops around the circle $n$ times.

From this definition, it is simple to calculate that transporting with $\mathsf{code}$ takes $\mathsf{loop}$ to the successor function, and $\mathord{{\mathsf{loop}}^{-1}}$ to the predecessor function:

Lemma 8.1.2.

$\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},x)=x+1$ and $\mathsf{transport}^{\mathsf{code}}(\mathord{{\mathsf{loop}}^{-1}},x)=x-1$ .

Proof.

For the first equation, we calculate as follows:

$\displaystyle{\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},x)}$	$\displaystyle=\mathsf{transport}^{A\mapsto A}(({\mathsf{code}}\mathopen{}\left% ({\mathsf{loop}}\right)\mathclose{}),x){}$	(by \autorefthm:transport-compose)
	$\displaystyle=\mathsf{transport}^{A\mapsto A}(\mathsf{ua}(\mathsf{succ}),x){}$	(by computation for $\mathsf{rec}_{\mathbb{S}^{1}}$)
	$\displaystyle=x+1{}.$	(by computation for $\mathsf{ua}$)

The second equation follows from the first, because $\mathsf{transport}^{B}(p,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ and $\mathsf{transport}^{B}(\mathord{{p}^{-1}},\mathord{\hskip 1.0pt\text{--}\hskip 1% .0pt})$ are always inverses, so $\mathsf{transport}^{\mathsf{code}}(\mathord{{\mathsf{loop}}^{-1}},\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt})$ must be the inverse of $\mathsf{succ}$ . ∎

We can now see what was wrong with our first approach: we defined $f$ and $g$ only on the fibers $\Omega(\mathbb{S}^{1})$ and $\mathbb{Z}$ , when we should have defined a whole morphism of fibrations over $\mathbb{S}^{1}$ . In type theory, this means we should have defined functions having types

	$\displaystyle\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})}}}$	$\displaystyle((\mathsf{base}=x)\to\mathsf{code}(x))\qquad\text{and/or}$		(1)
	$\displaystyle\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})}}}$	$\displaystyle(\mathsf{code}(x)\to(\mathsf{base}=x))$		(2)

instead of only the special cases of these when $x$ is $\mathsf{base}$ . This is also an instance of a common observation in type theory: when attempting to prove something about particular inhabitants of some inductive type, it is often easier to generalize the statement so that it refers to all inhabitants of that type, which we can then prove by induction. Looked at in this way, the proof of $\Omega(\mathbb{S}^{1})=\mathbb{Z}$ fits into the same pattern as the characterization of the identity types of coproducts and natural numbers in \autorefsec:compute-coprod,\autorefsec:compute-nat.

At this point, there are two ways to finish the proof. We can continue mimicking the classical argument by constructing (1) or (2) (it doesn’t matter which), proving that a homotopy equivalence between total spaces induces an equivalence on fibers, and then that the total space of the universal cover is contractible. The first type-theoretic proof of $\Omega(\mathbb{S}^{1})=\mathbb{Z}$ followed this pattern; we call it the homotopy-theoretic proof.

Later, however, we discovered that there is an alternative proof, which has a more type-theoretic feel and more closely follows the proofs in \autorefsec:compute-coprod,\autorefsec:compute-nat. In this proof, we directly construct both (1) and (2), and prove that they are mutually inverse by calculation. We will call this the encode-decode proof, because we call the functions (1) and (2) encode and decode respectively. Both proofs use the same construction of the cover given above. Where the classical proof induces an equivalence on fibers from an equivalence between total spaces, the encode-decode proof constructs the inverse map (decode) explicitly as a map between fibers. And where the classical proof uses contractibility, the encode-decode proof uses path induction, circle induction, and integer induction. These are the same tools used to prove contractibility—indeed, path induction is essentially contractibility of the path fibration composed with $\mathsf{transport}$ —but they are applied in a different way.

Since this is a book about homotopy type theory, we present the encode-decode proof first. A homotopy theorist who gets lost is encouraged to skip to the homotopy-theoretic proof (\autorefsubsec:pi1s1-homotopy-theory).

Title	8.1.3 The universal cover in type theory
\metatable

8.1.3 The universal cover in type theory

Definition 8.1.1 (Universal Cover of S1).

Lemma 8.1.2.

Proof.

Definition 8.1.1 (Universal Cover of $\mathbb{S}^{1}$ ).