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.

翻译：在一篇2005年的论文中，Casacuberta、Scevenels和Smith在单纯集范畴上构造了一个同伦幂等函子$E$，其是否能表示为关于某个映射$f$的局部化与ZFC公理无关。我们证明该构造可在同伦类型论中实现。更精确地说，我们提出一种通用方法，将合适的（可能大的）映射族关联到任意宇宙$\mathcal{U}$中的反射子宇宙。将其应用于特定族时，会生成一个局部化，该局部化在空间$\infty$-拓扑斯中解释时与对应于$E$的局部化一致。我们的方法在两方面推广了[CSS]的方法：首先，通过在同伦类型论中工作，我们的构造可在任意$\infty$-拓扑斯中解释；其次，[CSS]产生的局部对象始终是1-类型，而我们的构造可为任意$n$产生$n$-类型。即使在空间$\infty$-拓扑斯中，这也是全新的结果。此外，利用宇宙使我们的证明非常直接。过程中我们证明了若干关于"小"类型的独立有趣结果。作为应用，我们给出了分离局部化存在性的新证明。我们还给出了关于何时可将关于映射族的局部化表示为关于单个映射的局部化的结果，并证明单纯模型满足强形式的选择公理，该公理蕴含集合覆盖性及排中律成立。