The Hurewicz Theorem in Homotopy Type Theory