| Title:
|
Localization in Homotopy Type Theory (English) |
| Author:
|
Christensen, J. Daniel |
| Author:
|
Opie, Morgan |
| Author:
|
Rijke, Egbert |
| Author:
|
Scoccola, Luis |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
4 |
| Issue:
|
1 |
| Year:
|
2020 |
| Pages:
|
1-32 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type $X$, the natural map $X \rightarrow X_{(p)}$ induces algebraic localizations on all homotopy groups. In order to prove this, we further develop the theory of reflective subuniverses. In particular, we show that for any reflective subuniverse $L$, the subuniverse of $L$-separated types is again a reflective subuniverse, which we call $L'$. Furthermore, we prove results establishing that $L'$ is almost left exact. We next focus on localization with respect to a map, giving results on preservation of coproducts and connectivity. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space $K(G,n)$ with $G$ abelian. We also include a partial converse to the main theorem. (English) |
| Keyword:
|
Homotopy type theory |
| Keyword:
|
synthetic homotopy theory |
| Keyword:
|
univalence axiom |
| Keyword:
|
localization |
| Keyword:
|
reflective subuniverse |
| Keyword:
|
separated type |
| MSC:
|
03B15 |
| MSC:
|
18E35 |
| MSC:
|
55P60 |
| idZBL:
|
Zbl 1439.18023 |
| idMR:
|
MR4074272 |
| DOI:
|
10.21136/HS.2020.01 |
| . |
| Date available:
|
2026-03-11T10:53:29Z |
| Last updated:
|
2026-03-11 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153416 |
| . |
| Reference:
|
[1] Avigad, J., Kapulkin, K., Lumsdaine, P. LeFanu: Homotopy limits in type theory.Math. Structures Comput. Sci., Vol. 25, Iss. 5, 1040-1070, DOI:10.1017/S0960129514000498 10.1017/S0960129514000498 |
| Reference:
|
[2] Bousfield, A. K.: Localization and periodicity in unstable homotopy theory.J. Amer. Math. Soc., Vol. 7, Iss. 4, 831-873, DOI:10.2307/2152734 10.1090/S0894-0347-1994-1257059-7 |
| Reference:
|
[3] Brunerie, G.: On the homotopy groups of spheres in homotopy type theory.https://arxiv.org/abs/1606.05916 |
| Reference:
|
[4] Buchholtz, U., Doorn, F., Rijke, E.: Higher groups in homotopy type theory.Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, pp 205-214, DOI:10.1145/3209108.3209150 10.1145/3209108.3209150 |
| Reference:
|
[5] Casacuberta, C., Peschke, G.: Localizing with respect to self-maps of the circle.Trans. Amer. Math. Soc., Vol. 339, Iss. 1, 117-140, DOI:10.2307/2154211 10.1090/S0002-9947-1993-1123451-X |
| Reference:
|
[6] Doorn, F., Rijke, E., Sojakova, K.: Identity types of sequential colimits.In preparation |
| Reference:
|
[7] Farjoun, E. D.: Cellular spaces, null spaces and homotopy localization.Lecture notes in mathematics, Springer-Verlag, Berlin, DOI:10.1007/BFb0094429 10.1007/BFb0094429 |
| Reference:
|
[8] Kapulkin, K., Lumsdaine, P. LeFanu: The homotopy theory of type theories.Advances in Mathematics, Vol. 337, 1-38, DOI:10.1016/j.aim.2018.08.003 10.1016/j.aim.2018.08.003 |
| Reference:
|
[9] Licata, D. R., Finster, E.: Eilenberg-MacLane spaces in homotopy type theory.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), pp Article No. 66, DOI:10.1145/2603088.2603153 10.1145/2603088.2603153 |
| Reference:
|
[10] Lumsdaine, P. LeFanu, Shulman, M.: Semantics of higher inductive types.Mathematical Proceedings of the Cambridge Philosophical Society, DOI:10.1017/S030500411900015X 10.1017/S030500411900015X |
| Reference:
|
[11] May, J. P., Ponto, K.: More concise algebraic topology.Chicago lectures in mathematics, University of Chicago Press, Chicago, IL |
| Reference:
|
[12] Rijke, E.: The join construction.https://arxiv.org/abs/1701.07538 |
| Reference:
|
[13] Rijke, E., Shulman, M., Spitters, B.: Modalities in homotopy type theory.https://arxiv.org/abs/1706.07526v4 |
| Reference:
|
[14] Scoccola, L.: Nilpotent types and fracture squares in homotopy type theory.https://arxiv.org/abs/1903.03245 |
| Reference:
|
[15] Shulman, M.: All (\infty,1)-toposes have strict univalent universes.https://arxiv.org/abs/1904.07004 |
| Reference:
|
[16] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics.Institute for Advanced Study, Princeton, NJ |
| Reference:
|
[17] Vergura, M.: L'-localization in an \infty-topos.https://arxiv.org/abs/1907.03837 |
| Reference:
|
[18] Vergura, M.: Localization theory in an \infty-topos.https://arxiv.org/abs/1907.03836 |
| . |
