  We prove the Hurewicz theorem in homotopy type theory, i.e., that for $X$ a
pointed, $(n-1)$-connected type $(n \geq 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.

Algebraic Topology;Logic