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) $latex pi_1(X)$-sets, i.e., sets equipped with (right) group actions of the fundamental group $latex pi_1(X)$. 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…
View original post 713 more words