The Hurewicz theorem in Homotopy Type Theory

Abstract

We prove the Hurewicz theorem in homotopy type theory, i.e., that for $X$ a pointed, $(n-1)$-connected type $(n\ge 1)$ and $A$ an abelian group, there is a natural isomorphism ${\pi }_n(X{)}^{ab}\otimes A\cong {\tilde{H}}_n(X;A)$ relating the abelianization of the homotopy groups with the homology. We also compute the connectivity of a smash product of types and express the lowest non-trivial homotopy group as a tensor product. Along the way, we study magmas, loop spaces, connected covers and prespectra, and we use $1$-coherent categories to express naturality and for the Yoneda lemma. As homotopy type theory has models in all $\infty$-toposes, our results can be viewed as extending known results about spaces to all other $\infty$-toposes.

arXiv comment26 pages; v2 has minor clarifications; v3 has minor improvements throughout and is very close to AGT version

References in corpus (8)

• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Univalence for inverse diagrams and homotopy canonicity
• Semantics of higher inductive types
• The homotopy theory of type theories
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
• Synthetic Homology in Homotopy Type Theory
• Nilpotent Types and Fracture Squares in Homotopy Type Theory
• Localization in Homotopy Type Theory

Cited by in corpus (3)

• Computational Synthetic Cohomology Theory in Homotopy Type Theory
• Epimorphisms and Acyclic Types in Univalent Foundations
• Central H-spaces and banded types