Egbert Rijke: The Hurewicz Theorem in Homotopy Type Theory

I will present a proof of Dan Christensen and Luis Scoccola fo the Hurewicz Theorem in homotopy type theory. Te theorem states that for a pointed (n-1)-connected type X and an abelian group A, there is a natural isomorphism π_n(X)ᵃᵇ ⊗ A ≅ Ȟ_n(X;A), where Ȟ_n(X;A) is the n-th reduced homology group of X with coefficients in A.