Covering spaces are one of the important topics in classical homotopy theory, and this post summarizes what we have done in HoTT. We have formulated the covering spaces and (re)proved the classification theorem based on (right) -sets, i.e., sets equipped with (right) group actions of the fundamental group . I will explain the definition and why we need some constancy factorization trick in the proof.
So, what are covering spaces in HoTT? The core ingredient of covering spaces is a fibration, which is easy in HoTT, because every function or dependent type in HoTT can be viewed as a fibration (up to homotopy). The only problem is the possible higher structures accidentally packed into the space (which are usually handled separately in classical homotopy theory). To address this, we have another condition that each fiber is a set. These two conditions together match the classical definition. More precisely, given a base space , a covering is a mapping from to some universe (or, a type family indexed by ) where for each we know is a set.
One can also formulate coverings as mappings instead of type families. I personally prefer the latter because they seem easier to work with in type theory. Note that we did not assert that the base space is path-connected or pointed, which are required by interesting theorems (ex: the classification theorem) but not by the definition.
The classification theorem says there is an isomorphism between -set and covering spaces. Here we assume is path-connected and pointed (based) at .
The direction from covering spaces to -sets is easier, since the set can simply be the fiber over the point , and the group action can be defined as transporting along an element in the homotopy group. The other direction is more challenging, requiring an explicit construction of the covering space from the given -set. Naturally, the fiber over should be the underlying set, but what about other fibers? For arbitrary point in , due to the connectedness of the base space , there exists a (truncated) path from to , which can be used to transport everything in the fiber over to the fiber over . However, unless the homotopy group is trivial, one needs to identify multiple copies produced by different paths. We simply threw in gluing 1-cells and then made each fiber a set.
The above higher inductive type, which is called
ribbon in the library, goes as follows: It is parametrized by the -set, the underlying set , the group action , and the point in focus. The
trace constructor “copies” everything from the fiber over to the fiber over along some path in the base type, and the
paste constructor glues multiple copies made by different paths.
data ribbon (Y : Set) (∙ : Action Y) (x : X) : Set where trace : Y → Truncated 0 (x₀ = x) → ribbon x paste : (y : Y) → (loop : Truncated 0 (x₀ = x₀)) → (p : Truncated 0 (x₀ = x)) → trace (y ∙ loop) p ≡ trace y (loop ∘ p)
The most interesting part is to show that creating ribbons is left inverse to constructing -sets as mentioned in the beginning of the section. It suffices to show that ribbons indeed form the original covering space, which is, by functional extensionality, equivalent to demonstrating that they are fiberwise equivalent. The trouble is that, for a point and a point in the fiber of the input covering over , one needs a path to even make one point in the ribbon; while we can get a -truncated path out of the connectedness condition, the constructor requires a -truncated path.
The constancy comes to rescue! It can be shown that, if there is a function from to a set , and is constant, then factors through with ideal computational behaviors. In our case, different points generated by different paths will be glued together by the
paste constructor and moreover each fiber is a set. Therefore we can apply this lemma to establish the fiberwise equivalence, and hence the theorem!
We also proved that the homotopy group itself corresponds to the universal covering, where universality is defined as being simply-connected. The
ribbon construction, as an explicit description for covering spaces, comes in handy. In addition, we calculated (again) with the new library; however, even with aggressive Agda optimization, the complexity remains—one still needs to prove the contractibility of some covering of for universality. Perhaps there are other better examples which can show the real power of this isomorphism?
The Agda code is currently available at http://hott.github.io/HoTT-Agda/Homotopy.Cover.HomotopyGroupSetIsomorphism.html but we are rebuilding the whole library. This link might not be valid after the migration.