Algebraic & Geometric Topology Volume 23, issue 5 (2023)

Download this article
	For screen
	For printing

Recent Issues

The Journal

About the Journal

Editorial Board

Subscriptions

Submission Guidelines

Submission Page

Policies for Authors

Ethics Statement

ISSN 1472-2739 (online)

ISSN 1472-2747 (print)

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

DOI: 10.2140/agt.2023.23.2107

Bibliography

1	A Bauer, J Gross, P L Lumsdaine, M Shulman, M Sozeau, B Spitters, The HoTT library : A formalization of homotopy type theory in Coq, from: "Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs", ACM (2017) 164
2	M de Boer, A proof and formalization of the initiality conjecture of dependent type theory, licentiate thesis, Stockholm University (2020)
3	M de Boer, G Brunerie, A formalized proof of a version of the initiality conjecture, (2020)
4	U Buchholtz, F van Doorn, E Rijke, Higher groups in homotopy type theory, from: "LICS ’18—33rd Annual ACM/IEEE Symposium on Logic in Computer Science", ACM (2018) 205 MR3883727
5	U Buchholtz, K B Hou, Cellular cohomology in homotopy type theory, from: "LICS ’18—33rd Annual ACM/IEEE Symposium on Logic in Computer Science", ACM (2018) 521 MR3883759
6	J D Christensen, A Caglayan, Hurewicz formalzation, fork of HoTTCoq (2020)
7	J D Christensen, M Opie, E Rijke, L Scoccola, Localization in homotopy type theory, High. Struct. 4 (2020) 1 MR4074272
8	F van Doorn, On the formalization of higher inductive types and synthetic homotopy theory, PhD thesis, Carnegie Mellon University (2018) arXiv:1808.10690
9	R Graham, Synthetic homology in homotopy type theory, preprint (2017) arXiv:1706.01540
10	, The HoTT library, a Coq library for homotopy type theory (2012)
11	K Kapulkin, P L Lumsdaine, The homotopy theory of type theories, Adv. Math. 337 (2018) 1 MR3853043
12	K Kapulkin, P L Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), J. Eur. Math. Soc. 23 (2021) 2071 MR4244523
13	D R Licata, E Finster, Eilenberg–Mac Lane spaces in homotopy type theory, from: "Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)", ACM (2014) 66 MR3397687
14	D R Licata, M Shulman, Calculating the fundamental group of the circle in homotopy type theory, from: "2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)", IEEE Computer Soc. (2013) 223 MR3323808
15	P L Lumsdaine, M Shulman, Semantics of higher inductive types, Math. Proc. Cambridge Philos. Soc. 169 (2020) 159 MR4120789
16	T U F Program, Homotopy type theory: Univalent foundations of mathematics, Institute for Advanced Study (2013) MR3204653
17	L Scoccola, Nilpotent types and fracture squares in homotopy type theory, Math. Structures Comput. Sci. 30 (2020) 511 MR4122450
18	M Shulman, Univalence for inverse diagrams and homotopy canonicity, Math. Structures Comput. Sci. 25 (2015) 1203 MR3340541
19	M Shulman, All (∞,1)–toposes have strict univalent universes, preprint (2019) arXiv:1904.07004
20	K Sojakova, F van Doorn, E Rijke, Sequential colimits in homotopy type theory, from: "Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)", ACM (2020) 845 MR4171551