Download this article
 Download this article For screen
For printing
Recent Issues

Volume 24
Issue 3, 1225–1808
Issue 2, 595–1223
Issue 1, 1–594

Volume 23, 9 issues

Volume 22, 8 issues

Volume 21, 7 issues

Volume 20, 7 issues

Volume 19, 7 issues

Volume 18, 7 issues

Volume 17, 6 issues

Volume 16, 6 issues

Volume 15, 6 issues

Volume 14, 6 issues

Volume 13, 6 issues

Volume 12, 4 issues

Volume 11, 5 issues

Volume 10, 4 issues

Volume 9, 4 issues

Volume 8, 4 issues

Volume 7, 4 issues

Volume 6, 5 issues

Volume 5, 4 issues

Volume 4, 2 issues

Volume 3, 2 issues

Volume 2, 2 issues

Volume 1, 2 issues

The Journal
About the Journal
Editorial Board
Editorial Interests
Submission Guidelines
Submission Page
Policies for Authors
Ethics Statement
ISSN (electronic): 1472-2739
ISSN (print): 1472-2747
Author Index
To Appear
Other MSP Journals
The Hurewicz theorem in homotopy type theory

J Daniel Christensen and Luis Scoccola

Algebraic & Geometric Topology 23 (2023) 2107–2140

We prove the Hurewicz theorem in homotopy type theory, ie that for X a pointed, (n1)–connected type, with n 1, and A an abelian group, there is a natural isomorphism πn(X)ab AH~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 nontrivial 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 –toposes, our results can be viewed as extending known results about spaces to all other –toposes.

Hurewicz theorem, homotopy group, homology group, magma, loop space, tensor product, homotopy type theory
Mathematical Subject Classification
Primary: 55Q99
Secondary: 03B38, 18N60, 55N99
Received: 29 September 2020
Revised: 24 January 2022
Accepted: 16 February 2022
Published: 25 July 2023
J Daniel Christensen
Department of Mathematics
University of Western Ontario
London, ON
Luis Scoccola
Department of Mathematics
University of Western Ontario
London, ON

Open Access made possible by participating institutions via Subscribe to Open.