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 ${𝕊}^1$ is represented by the type family $(x\mapsto (\mathrm{𝖻𝖺𝗌𝖾}=x))$.We have also already seen a good candidate for the universal cover of ${𝕊}^1$: it’s none other than the type family $c:{𝕊}^1\to 𝒰$ which we defined in sec:pi1s1-initial-thoughts!By definition, the fiber of this family over $\mathrm{𝖻𝖺𝗌𝖾}$ is $\mathbb{Z}$, while the effect of transporting around $\mathrm{𝗅𝗈𝗈𝗉}$ is to add one — thus it behaves just as we would expect from fig: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 ${\mathrm{S}}^{\mathrm{1}}$).

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

$\mathrm{𝖼𝗈𝖽𝖾}(\mathrm{𝖻𝖺𝗌𝖾})$$:\equiv \mathbb{Z}$

${\mathrm{𝖺𝗉}}_{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉})$$:=\mathrm{𝗎𝖺}(\mathrm{𝗌𝗎𝖼𝖼}).$

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 aloop in the codomain. In this case, the codomain is $𝒰$, and the pointwe choose is $\mathbb{Z}$, corresponding to our expectation that thefiber of the universal cover should be the integers. The loop we chooseis the successor/predecessorisomorphism on $\mathbb{Z}$, whichcorresponds to the fact that going around the loop in the base goes upone level on the helix. Univalence is necessary for this part of theproof, 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$\mathrm{𝖼𝗈𝖽𝖾}$ takes $\mathrm{𝗅𝗈𝗈𝗉}$ to the successor function, and${\mathrm{𝗅𝗈𝗈𝗉}}^{-1}$ to the predecessor function:

Lemma 8.1.2.

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉},x)=x+1$ and${\mathrm{transport}}^{\mathrm{code}}\mathit{}\mathrm{(}{\mathrm{loop}}^{\mathrm{-}\mathrm{1}}\mathrm{,}x\mathrm{)}\mathrm{=}x\mathrm{-}\mathrm{1}$.

Proof.

For the first equation, we calculate as follows:

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉},x)$$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{A\mapsto A}((\mathrm{𝖼𝗈𝖽𝖾}\left(\mathrm{𝗅𝗈𝗈𝗉}\right)),x)$(by \\autorefthm:transport-compose)

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{A\mapsto A}(\mathrm{𝗎𝖺}(\mathrm{𝗌𝗎𝖼𝖼}),x)$(by computation for $\\mathsf{rec}_{\\mathbb{S}^{1}}$)

$=x+1.$(by computation for $\\mathsf{ua}$)

The second equation follows from the first, because ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,\text{–})$ and ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p^{-1},\text{–})$ are always inverses, so ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗅𝗈𝗈𝗉}}^{-1},\text{–})$ must be the inverse of $\mathrm{𝗌𝗎𝖼𝖼}$.∎

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

${\displaystyle \prod _{x:{𝕊}^1}}$$((\mathrm{𝖻𝖺𝗌𝖾}=x)\to \mathrm{𝖼𝗈𝖽𝖾}(x))\mathit{\hspace{1em}\hspace{1em}}\text{and/or}$(1)

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

instead of only the special cases of these when $x$ is $\mathrm{𝖻𝖺𝗌𝖾}$.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 $\mathrm{\Omega }({𝕊}^1)=\mathbb{Z}$ fits into the same pattern as the characterization of the identity types of coproducts and natural numbers in sec:compute-coprod,sec: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 $\mathrm{\Omega }({𝕊}^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 sec:compute-coprod,sec: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 $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$—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 (subsec:pi1s1-homotopy-theory).