# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorBartek
• CommentTimeDec 20th 2021

Added the proof of the fundamental theorem of covering spaces in HoTT

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeDec 21st 2021
• (edited Dec 21st 2021)

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.

• CommentRowNumber3.
• CommentAuthorHurkyl
• CommentTimeDec 21st 2021

Added another paragraph to the idea section describing this as related to the equivalence $\infty Grpd_{/X} \simeq \infty Grpd^X$.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeDec 21st 2021

As before, since “$X$” denotes a topological space in the preceding sentences, I have changed it to $\esh X$ and added brief commentary.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeDec 26th 2021