The universal covering component conjecture for connected types

About 1 year old · traced to

Let AA be a connected type, let A~\tilde A denote its universal nn-covering, and let \Covering[n](A)\Covering[n](A) denote the type of nn-coverings of AA. The connected component of A~\tilde A in \Covering[n](A)\Covering[n](A) is the component equivalent to \truncn+1A\trunc{n+1}A.

Universal covering component conjecture. The connected component of A~\tilde A in \Covering[n](A)\Covering[n](A) is \truncn+1A\trunc{n+1}A.

This conjecture is proposed as a means of constructing deloopings of higher groups from universal coverings. The supplied text does not indicate whether it has been proved or remains open.

References

Primary source

Samuel Mimram and Émile Oleon, “Classifying covering types in homotopy type theory”, arXiv:2512.10064 (2026).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.