Non-accessible localizations
J. Daniel Christensen
TL;DR
The paper develops a general method for constructing reflective subuniverses (localizations) in homotopy type theory from a possibly large family of maps, and shows these localizations are well-defined within any $\mathcal{U}$ and correspond to CSS-style localizations in spaces when interpreted in the $\infty$-topos. It introduces a robust smallness framework and an extended family construction $\bar{f}$ to realize $n$-truncated localizations for any $n\ge -1$, without smallness assumptions on indexing data, and proves that the resulting localization is reflective. It further analyzes when a family can be replaced by a single map, using HoTT tools (set-indexing reductions, $\mathrm{tot}(f)$) and a strong choice principle in the simplicial model, linking to accessibility and LEM/sets-cover phenomena. The work connects with CSS, CORS, and RSS to situate the new constructions within the landscape of localized ∞-topoi, and the formalization in Coq/HoTT demonstrates the soundness of the proofs and methods. Overall, it shows how non-accessible localizations can be realized in HoTT and how their properties reflect foundational set-theoretic assumptions.
Abstract
In a 2005 paper, Casacuberta, Scevenels and Smith construct a homotopy idempotent functor $E$ on the category of simplicial sets with the property that whether it can be expressed as localization with respect to a map $f$ is independent of the ZFC axioms. We show that this construction can be carried out in homotopy type theory. More precisely, we give a general method of associating to a suitable (possibly large) family of maps, a reflective subuniverse of any universe $\mathcal{U}$. When specialized to an appropriate family, this produces a localization which when interpreted in the $\infty$-topos of spaces agrees with the localization corresponding to $E$. Our approach generalizes the approach of [CSS] in two ways. First, by working in homotopy type theory, our construction can be interpreted in any $\infty$-topos. Second, while the local objects produced by [CSS] are always 1-types, our construction can produce $n$-types, for any $n$. This is new, even in the $\infty$-topos of spaces. In addition, by making use of universes, our proof is very direct. Along the way, we prove many results about "small" types that are of independent interest. As an application, we give a new proof that separated localizations exist. We also give results that say when a localization with respect to a family of maps can be presented as localization with respect to a single map, and show that the simplicial model satisfies a strong form of the axiom of choice which implies that sets cover and that the law of excluded middle holds.