Classifying Covering Types in Homotopy Type Theory

By definition of morphisms and initiality of $1$, the type $1$ is initial among pointed types over $A$. A universal pointed type $p:B\to A$ is also initial among pointed types over $A$, by the universal property, and thus $B$ is equivalent to $1$, i.e. contractible. $◀$ By immediate computations, we have:

It is very illuminative to translate the previous definitions and properties under the Grothendieck duality (see Theorem 1). A pointed type over $A$ corresponds to a fibration $P:A\to 𝒰$ together with a distinguished element ${\star }_P$ of $P\star$, and, by Proposition 6, such a fibration is universal precisely when the total space $\mathrm{\Sigma }A.P$ is contractible. The universal pointed type thus corresponds to the universal fibration, which is the map ${ℱ}_A:A\to 𝒰$ defined by ${ℱ}_{A}x\equiv (\star =x)$, and pointed by ${\mathrm{refl}}_{\star }$. By Theorem 1, a morphism between fibrations $P,Q:A\to 𝒰$ corresponds to a family of maps $f:(x:A)\to Px\to Qx$ together with an identification $f\star {\star }_P={\star }_Q$. The initiality property of universal pointed types (Definition 5) then translates as the fundamental theorem of identity types [12, Theorem 11.2.2]:

Under the Grothendieck duality of Theorem 1, the type family $P$ corresponds to the pointed type $p:\mathrm{\Sigma }A.P\to A$ over $A$, given by the first projection. The family of maps $F$ then corresponds to a morphism between the universal type over $A$ and $p$, i.e. to a pointed map $f:1\to \mathrm{\Sigma }A.P$. Then $F$ is a family of equivalences if and only if the induced map $f$ is an equivalence, i.e. if and only if $\mathrm{\Sigma }A.P$ is contractible. $◀$

Follows immediately from Grothendieck duality (Theorem 1). $◀$

A morphism $f$ between $n$-coverings $p:B\to A$ and $q:C\to A$ is a map $f:B\to C$ together with an equality $p=q\circ f$.

A pointed $n$-covering is a pointed map $p:B{\to }_{\star }A$ between pointed types, whose underlying map is an $n$-covering. This corresponds exactly to the following notion:

In the following, we sometimes assimilate the covering to the map $p:B\to A$ leaving the data of the pointing $i:1\to B$ of $B$ implicit. As expected, a morphism $f$ between pointed $n$-coverings $p$ and $q$ is a pointed map which is a morphism between the underlying $n$-coverings, i.e. such that the factorization of the target is $q\circ (f\circ i)$:

We sometimes write $\tilde{A}$ for the universal $n$-covering. This is justified by the fact that, being defined by a universal property, it is uniquely characterized:

We have the following characterization of universal $n$-coverings:

By [14, Theorem 7.6.6], the map $a:1\to A$ admits a unique factorization $a=p\circ i$ as required. Moreover, given a $n$-covering $q:B\to A$ pointed by $b:1\to B$, we have a commuting square as on the left

The commutation of the two triangles being given by the fact that we have two pointed $n$-coverings of $A$ pointed by $a$. By [14, Theorem 7.6.7], because $i$ is $n$-connected and $p$ is $n$-truncated, there is a unique map $\tilde{A}\to B$ making the two triangles on the right commute, and $p$ is thus universal in the sense of Definition 13. $◀$

In practice, the universal $n$-covering can be constructed as follows. We recall from [14, Definition 7.6.3] that, given a map $f:B\to A$ and a natural number $n$, its $n$-image is

We write $i_n:B\to {\mathrm{im}}_{n}f$ for the canonical map such that $i_n(x)=(f(x),{|{\mathrm{refl}}_x|}_n)$ and $p_n:{\mathrm{im}}_{n}f\to A$ for the first projection map.

By [14, Lemma 7.6.4], this factorization satisfies the conditions of Theorem 16. $◀$

The universal $n$-covering can also be characterized as the covering whose total space is $(n+1)$-connected. This can be shown using the following lemma proved in appendix.

By Definition 12, a pointed $n$-covering $p:B\to A$ is a factorization of the pointing map $a:1\to A$ as $a=p\circ i$ with $p$ $n$-truncated. By Theorem 16, it is universal if and only if $i:1\to B$ is $n$-connected which, by Lemma 21 is equivalent to the fact that $B$ is $(n+1)$-connected. $◀$

We now formalize the intuition that the universal $n$-covering $\tilde{A}$ of $A$ provides a way to “kill” all the homotopy in dimension $i\le n+1$. This is based on what we call the fundamental fibration associated to the universal $n$-covering:

We have

where middle equality is [14, Theorem 7.3.12] and right one is Proposition 17. $◀$ This was actually taken to be the definition of $n$-coverings in [2]. As a corollary, we have the following characterization of the homotopy groups of the universal $n$-covering:

In particular, this suggests that the universal covering should be contractible when $A$ has no homotopy in dimension $i>n+1$:

Since $A$ is supposed to be $(n+1)$-truncated, the pointing map $a:1\to A$ is $n$-truncated by Lemma 21 and the factorization $a=a\circ {\mathrm{id}}_1$ of the pointing map as an $n$-connected map followed by an $n$-truncated map has to be the factorization of the universal covering (Theorem 16) by uniqueness. $◀$

We would like to end this section with the following conjecture, which would allow constructing deloopings of higher groups based on the previous construction. Note that, below, the coverings are not supposed to be pointed.

Provided that this conjecture holds, the connected component of $\tilde{A}$ in $A$ would be a pointed $(n+1)$-connected groupoid, which can thus be thought of as a delooping of the fundamental $n$-group of $A$. The following proposition shows that we have right underlying type (it would remain to be shown that we have the right higher operations for the $n$-group):

By universal property of $\tilde{A}$ (Definition 5), an automorphism $f:\tilde{A}\to \tilde{A}$ is uniquely determined by $f\star$ which is an element of ${\mathrm{fib}}_p\star$. The type of automorphisms of $\tilde{A}$ is thus ${\mathrm{fib}}_p\star$. Now, by Proposition 17, we can consider that $p$ is the first projection $p:\mathrm{\Sigma }(x:A).\parallel {\mathrm{fib}}_{a}x{\parallel }_n\to A$ whose fiber at $\star$ is $\parallel {\mathrm{fib}}_a\star {\parallel }_n$ by [14, Lemma 4.8.1], i.e. ${\Vert \mathrm{\Omega }A\Vert }_n$. $◀$

We take $|\star {|}_1$ to be the distinguished point of ${\Vert A\Vert }_1$. Connectedness is preserved by truncation: we have ${\Vert {\Vert A\Vert }_1\Vert }_0={\Vert A\Vert }_0=1$ (the first equality is [14, Lemma 7.3.15] and the second one is the fact that $A$ is connected) and thus ${\Vert A\Vert }_1$ is connected. Finally, we have $\mathrm{\Omega }{\Vert A\Vert }_1={\Vert \mathrm{\Omega }A\Vert }_0\equiv {\pi }_{1}A$ by [14, Corollary 7.3.13]. $◀$ The previous discussion suggests defining:

Its target is $\mathrm{B}{\pi }_{1}A$ by Proposition 30 and we have the expected fiber as the case $n=0$ of Theorem 24:

As an interesting immediate consequence of this result, we recover the fact that the fibers of the universal covering are the fundamental group:

By [14, Section 8.4], the fiber sequence of Proposition 32 can be extended on the left by $\mathrm{\Omega }\mathrm{B}{\pi }_{1}A$, which is ${\pi }_{1}A$ by definition of the delooping. $◀$

A careful reader could wonder why the action encoded by Proposition 32 is actually the “right” one in the sense that it corresponds to the traditional one in topology. We can expect that there are other such actions, i.e. maps $f:A\to \mathrm{B}{\pi }_{1}A$ with $\ker f=\tilde{A}$ (what will be important here is that $\tilde{A}$ is 1-connected by Remark 23). In fact, it turns out is only one possible such action, up to an automorphism of $\mathrm{B}{\pi }_{1}A$:

By naturality of truncation [14, equation (7.3.4)], we have a commutative square

By definition, the upper map is $g_A$. The lower map is $g_{\mathrm{B}{\pi }_{1}A}$, which is an equivalence because $\mathrm{B}{\pi }_{1}A$ is a groupoid [14, Corollary 7.3.7]. The right vertical map is also an equivalence by [14, Lemma 7.5.14], because $f$ is supposed to be 1-connected. Finally, $e\equiv g_{\mathrm{B}{\pi }_{1}A}^{-1}\circ {\Vert f\Vert }_1$ is an equivalence as a composite of equivalences. $◀$ The situation above is a bit subtle. It states that a 1-connected map as $f$ has to be the Galois fibration. However, this is up to an automorphism of $\mathrm{B}{\pi }_{1}A$, which might itself bear some information. Indeed, pointed automorphisms of $\mathrm{B}{\pi }_{1}A$ correspond to group automorphisms of ${\pi }_{1}A$ which might be non-trivial. In all the applications below, insights from the corresponding constructions in algebraic topology allow us to make sure that we indeed have the right action.

Given a subgroup $i:G\hookrightarrow {\pi }_1(A)$, the corresponding covering $X$ is obtained as pullback of the Galois fibration along the delooping of group inclusion:

We need to show that $C_G$ is a connected covering, i.e. it is connected and $p_G$ has $0$-truncated fibers. The fiber of the covering is given by pasting pullbacks

and thus we have

by Lemma 35 (to be precise, we only have the existence of such an equality, which is sufficient for our purposes exposed in next sentence). As a consequence, the fibers of $p_G$ are sets. Also, by vertical pasting of pullbacks,

we have that the upper square is a pullback, i.e. a fibration sequence of the form

which describes, by action-fibration duality, an action of $G$ on $\tilde{A}$ such that

Therefore, $C_G$ is connected as a homotopy quotient of a connected space.

Conversely, given a connected covering $f:X\to A$, we have

This is a mono, because we have the long exact sequence associated to the fibration:

where $F\equiv \ker f$ is a set (because $f$ is covering) and thus ${\pi }_1(F)=1$.

We now have to show that these two operations are mutually inverse. Given a connected covering $f:X\to A$, the associated connected covering (by performing the two operations) is obtained as the pullback on the left, which can be rewritten as on the right.

The outer square of the diagram below commutes by naturality of the unit of the truncation, and we thus have a universal map $e:X\to C_{{\pi }_{1}X}$ such that

More explicitly,

and $e(x)=(f(x),{|x|}_1,{\mathrm{refl}}_{{|f(x)|}_1})$. Because the lower-left triangle commutes, $e$ is a map between types over $A$, and thus corresponds by Grothendieck duality (Theorem 1) to a family of fiberwise maps

indexed by $a:A$, with $p:a=f(x)$. Let us consider the case $a\equiv \star$. We have

We can construct an inverse map to $e_{\star }$

where we assume that $y={|x|}_1$ because we are eliminating to ${\mathrm{fib}}_f\star$ which is a set (and thus a groupoid). Above, we have $p:{|a|}_1={\Vert f\Vert }_1(x)$, which is equivalent to $\parallel a=f(x){\parallel }_0$ (by [14, Theorem 7.3.12]) and we can thus suppose that $q={|\tilde{q}|}_0$ with $\tilde{q}:a=f(x)$ because we are eliminating to a set. We have

Conversely,

(we can suppose that the second and third arguments are truncations as above, because we are eliminating to a set). We thus have to show

with $p:\star =a$ and $q:a=f(x)$. Abstracting over $a$, we can suppose that $q$ is $\mathrm{refl}$ by J, and we conclude immediately.

Conversely, given a subgroup $i:G\hookrightarrow {\pi }_{1}A$, the associated subgroup (by performing the two transformations) is

we thus have to show that ${\pi }_1{C}_G=G$ and the map ${\pi }_1{p}_G=i$ (note that to be precise, we should identify the sources and the targets of the maps up to equality). We have a pullback square

which can be extended as (see above)

The map $C_G\to \mathrm{B}G$ is 1-connected because the fiber is $\tilde{A}$ which is 1-connected by Theorem 22. By [14, Lemma 7.5.14], it thus induces an equivalence ${\Vert C_G\Vert }_1\simeq {\Vert \mathrm{B}G\Vert }_1$, and thus ${\pi }_1(C_G)={\pi }_1(\mathrm{B}G)=G$. We should have the fact that ${\pi }_1{p}_G=i$ similarly, by applying ${\pi }_1$ to the above square (which is not anymore a pullback but remains commutative). $◀$

We write $X$ for pullback of ${\varphi }_n^l$ and $\mathrm{B}{i}_m$ as shown on the left below:

The type $X$ is pointed (because both maps ${\varphi }_n^l$ and $\mathrm{B}{i}_m$ are) and connected (this can be shown as in [9, Lemma 26]). Finally, since loop spaces commute to pullbacks because they are right adjoints, we have a pullback square of groups as on the right above. From this, we can deduce that $\mathrm{\Omega }X\cong \mathbb{Z}$ as follows. The preceding pullbacks means that we have

We write $f:\mathbb{Z}\to \mathrm{\Omega }X$ for the map sending $1$ to $(p,l)$, and we claim that this is an isomorphism.

First, $f$ is injective because $(p,l)$ is free. Indeed, suppose that $f(x)\equiv (xp,xl)=0$. In particular, $xp{=}_{\mathbb{Z}}0$ and since $p\ne 0$ we have $x=0$. Second, $f$ is surjective. Fix $(a,b):\mathrm{\Omega }X$. There is $y\in \mathbb{Z}$ such that $al=bp+yn=p(b+ym)$. Therefore $p\mid al$, but $l$ is prime with $n$ and $p\mid n$ so that $l$ is prime with $p$ and thus $p\mid a$. There thus exists $x$ such that $a=px$. Thus $pxl-bp{=}_{{\mathbb{Z}}_n}0$, i.e. $p(xl-b){=}_{{\mathbb{Z}}_n}0$, that is $mp\equiv n\mid p(xl-b)$ and thus $m\mid xl-b$, i.e. $b{=}_{{\mathbb{Z}}_m}xl$. Finally, $(a,b)=(xp,xl)\equiv f(x)$ and $f$ is surjective. The maps of the pullback are the projections from $\mathrm{\Omega }X$ and are thus the expected ones. $◀$

By Theorem 36, the coverings of $L_n^{l_1,\mathrm{\dots },l_k}$ correspond to subgroups of ${\pi }_1{L}_n^{l_1,\mathrm{\dots },l_k}$, i.e. the subgroups of ${\mathbb{Z}}_n$, and those are of the form ${\mathbb{Z}}_m$ for $m\mid n$. More precisely, by Theorem 36, given such a subgroup $i_m:{\mathbb{Z}}_m\to {\mathbb{Z}}_n$, the corresponding covering space is given by the pullback of the delooping this map along the Galois fibration:

As remarked in Proposition 34, we can replace the bottom map by ${\varphi }_n^{l_1,\mathrm{\dots },l_k}$. By [9, Theorem 25], pullback commute with joins of maps, so the map $X\to \mathrm{B}{\mathbb{Z}}_m$ can be computed as the iterated join of the maps obtained by pulling back ${\varphi }_n^{l_i}$ along $\mathrm{B}{i}_m$, which, by Proposition 39, are the ${\varphi }_m^{l_i}:{\mathrm{S}}^1\to \mathrm{B}{\mathbb{Z}}_m$. The pullback of ${\varphi }_n^{l_1,\mathrm{\dots },l_k}$ along $\mathrm{B}{i}_m$ is thus ${\varphi }_m^{l_1,\mathrm{\dots },l_k}$. Similarly, by [9, Theorem 25] and Proposition 39, the vertical map $X\to L_n^{l_1,\mathrm{\dots },l_k}$ is obtained as the join of $n$ instances of $s_p$. Finally, we obtain the pullback square

$◀$

We have defined and studied in [10] a type corresponding to the hypercubical manifold. Topologically, this manifold $K$ was defined by Poincaré as a space obtained by identifying the opposite faces of a cube after a quarter-turn rotation, and can be pictured as below. The fundamental group of this space is the quaternion group $Q$ and its universal covering is the 3-sphere ${\mathrm{S}}^3$. Thus, $K$ can also be obtained as a quotient of ${\mathrm{S}}^3$ under $Q$.

In homotopy type theory, a type corresponding to $K$ is easily defined as a higher inductive type. However, in order to work with it and validate its construction, we need to show that it can be obtained as a quotient of ${\mathrm{S}}^3$ under the action of $Q$, i.e. from a map $\mathrm{B}Q\to 𝒰$ such that the image of $\star$ is ${\mathrm{S}}^3$. However, such a map is difficult to construct directly using the elimination principle of $\mathrm{B}Q$ because ${\mathrm{S}}^3$ is not $n$-truncated for any $n$. As explained above, we can instead adopt a fibrational point of view and construct a map $\varphi :K\to \mathrm{B}Q$ whose fiber is ${\mathrm{S}}^3$, i.e. a fiber sequence

thus showing that $K$ is a quotient of ${\mathrm{S}}^3$ under an action of $Q$. Details can be found in [10].

When investigating the notion of homology, it was not clear at first whether homology would be fine enough in order to characterize homotopy types. It turns out that this is not the case, which was first shown by Poincaré by introducing a space, the homology sphere (also known as the Poincaré dodecahedral space), which has the same homology type as the sphere ${\mathrm{S}}^3$, but not the same homotopy type [11].

Following [5], we define the homology sphere $D$ as a higher inductive type corresponding to a dodecaedron where each face is identified with the opposite one after a rotation of a fifth-turn. The classes of 0-, 1- and 2-cells respectively have 4, 3 and 2 elements, and edges are identified as indicated by the colors on the above picture. The resulting space has one 3-cell, 6 2-cells, 10 1-cells and 5 0-cells. The fundamental group ${\pi }_1(D)$ is the group of order 120, known as the binary icosahedral group, which can be presented as $⟨r,s,t|r^2=s^3=t^5=rst⟩$. To exhibit $D$ as a quotient of the $3$-sphere under the action of the binary icosagedral group, we need to show that we have a fibration

As for the hypercubical manifold, we can build a model for the fundamental group of $D$ in two steps: we first construct the fundamental groupoid (whose 0-, 1- and 2-cells are generated by the 0-, 1- and 2-cells involved in the description of $D$ as a cellular complex), and then we contract 1-cells in order to obtain a type with only one 0-cell, which is thus a delooping of a group, i.e. $\mathrm{B}{\pi }_1(D)$. The map $\varphi$ is then the canonical one induced by this process. Finally, since $D$ is constructed by attaching cells, i.e. has a canonical description as a colimit, we can use the flattening lemma in order to compute its fiber, which we claim to be ${\mathrm{S}}^3$. This will be detailed in subsequent works.