Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Just on aesthetics:
It seems a little heavy to markup an article reference as a section
_Localization in Homotopy Type Theory_, [[Daniel Christensen]], [[Morgan Opie]], [[Egbert Rijke]], [[Luis Scoccola]],
## Links ##
[arXiv:1807.04155](https://arxiv.org/abs/1807.04155)
Why not use more usual bibitem formatting, such as:
Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola,
Localization in Homotopy Type Theory,
Higher Structures 4 1 (2020) 1-32
$[$arXiv:1807.04155, doi$]$
This looks more professional, and has the advantage that one can copy-and-paste it for use as an actual reference.
In fact, this is the form in which this article is being referenced at various places on the nLab, for instance here.
In adding the missing publication data, I have taken the liberty of re-formatting as follows, what do you think:
J. Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola:
Localization in Homotopy Type Theory
Higher Structures 4 1 (2020) 1-32
on localization in homotopy type theory.
Abstract. 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 \to 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_0$. Furthermore, we prove results establishing that $L_0$ 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.
1 to 3 of 3