The Hurewicz theorem in homotopy type theory

DOI10.2140/agt.2023.23.2107arXiv2007.05833WikidataQ121749163 ScholiaQ121749163MaRDI QIDQ6112530

Luis Nerio Scoccola, J. Daniel Christensen

Publication date: 7 August 2023

Published in: Algebraic \& Geometric Topology (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2007.05833

zbMATH Keywords

homotopy grouphomology grouptensor productloop spacehomotopy type theoryHurewicz theoremmagma

Mathematics Subject Classification ID

Homology and cohomology theories in algebraic topology (55N99) Homotopy groups (55Q99) Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60) Category theory; homological algebra (18-XX)

Related Items (1)

Eilenberg-MacLane spaces and stabilisation in homotopy type theory

Cites Work

• The homotopy theory of type theories
• The simplicial model of univalent foundations (after Voevodsky)
• Eilenberg-MacLane spaces in homotopy type theory
• Semantics of higher inductive types
• Nilpotent types and fracture squares in homotopy type theory
• Higher Groups in Homotopy Type Theory
• Cellular Cohomology in Homotopy Type Theory
• Sequential Colimits in Homotopy Type Theory
• Localization in Homotopy Type Theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: The Hurewicz theorem in homotopy type theory