Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
For a more faithful type-theoretic reflection of traditional covering-space theory one ought to understand it as a topic in cohesive homotopy type theory:
What deserves to be called the fundamental groupoid of a geometric homotopy type $X$ is not really $\Vert X \Vert_1$, but $\Vert \esh X \Vert_1$, where $\esh$ is the shape modality (see at shape via cohesive path ∞-groupoid). With this, the fundamental theorem of covering space theory is a reflection of the defining adjunction $\esh \dashv \flat$ with the flat modality, which is such that $\flat Sets$ is the actual classifier for covering spaces over geometric homotopy types.
I have appended (here) a paragraph along these lines.
added pointer to
which explicitly states and proves the cohesive HoTT-version of the theorem.
1 to 5 of 5