Non-accessible localizations (Q6564515)

The article is concerned with smallness and accessibility criteria for reflective localizations of universes in homotopy type theory (in the following ``HoTT'' for short). Throughout the paper, the author works relative to a fixed universe of small types and a fixed super-universe of large types. The main result (Theorem 3.3) states for any integer \(n\geq -1\) that inside HoTT any reflective localization of the universe of large types at a large set of \((n-1)\)-connected maps restricts to a reflective localization of the universe of small \(n\)-types. The motivating application is non-provability of the statement that all (small) reflective localizations are necessarily accessible inside HoTT, which goes back to the construction of a non-accessible reflective homotopical localization of spaces due to [\textit{C. Casacuberta} et al., Forum Math. 18, No. 6, 967--982 (2006; Zbl 1214.55009)].\N\NSection 1 is a comprehensive introduction. In Section 2, the author gives techniques to derive smallness of a large type \(X\) from smallness of various associated invariants of \(X\) under suitable assumptions. This includes proofs of smallness of \(X\) whenever it can be suitably covered by a small type (notably Proposition 2.2) or suitably embedded into a small (enough) type. In Section 3, the author shows that a reflective localization of the universe of large types always restricts to a reflective localization of the universe of small types whenever the associated localization endofunctor does so. Using the Axiom of Propositional Resizing and the techniques of Section 2, the author derives the main result (Theorem 3.3) referred to above. Section 4 contains a brief application to the universe of separated types with respect to a given reflective localization. In Section 5.1, the author gives a set of conditions under which a given accessible localization -- that is, a reflective localization at a family \(f\colon\prod_{i: I}A_i\rightarrow B_i\) of maps internally indexed by a set \(I\) -- is equivalent to a localization at a single map -- given by the map of associated total types \(\mathrm{tot}(f)\colon\Sigma_i A_i\rightarrow \Sigma_i B_i\). This set of conditions consists of the Law of Excluded Middle, the axiomatic assumption that ``sets cover in the universe'', and the condition that the empty type is local for the given localization. Section 5.2 largely consists of a proof that this set of conditions is satisfied in the standard HoTT-model of simplicial sets. Section 6 is a brief recollection of the construction of a non-accessible reflective localization of spaces under the assumption of a large cardinal axiom from [loc. cit.]. It also explains how the constructions in loc.\ cit.\ relate to the synthetic constructions presented in this paper, and hence it presents an argument of non-provability of the statement that all (small) reflective localizations are accessible inside HoTT. Section 7 comments about formalized implementations of the results of this paper using the Coq HoTT library.