ct.category theory – Reflection principle vs universes

In category-theoretic discussions, there is often the temptation to look at the category of all abelian groups, or of all categories, etc., which quickly leads to the usual set-theoretic problems. These are often avoided by using Grothendieck universes. In set-theoretic language, one fixes some strongly inaccessible cardinal $kappa$ — this means that $kappa$ is some uncountable cardinal such that for all $lambda<kappa$, also $2^lambda<kappa$, and for any set of $<kappa$ many sets $S_i$ of size $<kappa$, also their union is of size $<kappa$. This implies that the stage $V_kappasubset V$ of “sets of size $<kappa$” is itself a model of ZFC — by applying any of the operations on sets, like taking powersets or unions, you can never leave $V_kappa$. These sets are than termed “small”, and then the category of small abelian groups is definitely well-defined.

Historically, this approach was first used by Grothendieck; a more recent foundational text is Lurie’s work on $infty$-categories. However, their use has always created somewhat of a backlash, with some people unwilling to let axioms beyond ZFC slip into established literature. For example, I think at some point there was a long discussion whether Fermat’s Last Theorem has been proved in ZFC. More recently, I’ve seen similar arguments come up for theorems whose proofs refer to Lurie’s work. (Personally, I do not have strong feelings about this and understand the arguments either way.)

On the other hand, it has also always been the case that a closer inspection revealed that any use of universes was in fact unnecessary. For example, the Stacks Project does not use universes. Instead, (see Tag 000H say) it effectively weakens the hypothesis that $kappa$ is strongly inaccessible, to something like a strong limit cardinal of uncountable cofinality, i.e.: for all $lambda<kappa$, one has $2^lambda<kappa$, and whenever you have a countable collection of sets $S_i$ of size $<kappa$, also the union of the $S_i$ has size $<kappa$. ZFC easily proves the existence of such $kappa$, and almost every argument one might envision doing in the category of abelian groups actually also works in the category of $kappa$-small abelian groups for such $kappa$. If one does more complicated arguments, one can accordingly strengthen the initial hypothesis on $kappa$. I’ve had occasion to play this game myself, see Section 4 of www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf for the result. From this experience, I am pretty sure that one can similar rewrite Lurie’s “Higher Topos Theory”, or any other similar category-theoretic work, in a way to remove all strongly inaccessible cardinals, replacing them by carefully chosen $kappa$ with properties such as the ones above.

In fact, there seems to be a theorem of ZFC, the reflection principle (discussed briefly in Tag 000F of the Stacks project, for example), that seems to guarantee that this is always possible. Namely, for any given finite set of formulas of set theory, there is some sufficiently large $kappa$ such that, roughly speaking, these formulas hold in $V_kappa$ if and only if they hold in $V$. This seems to say something like that that for any given finite set of formulas, one can find some $kappa$ such that $V_kappa$ behaves like a universe with respect to these formulas, but please correct me in my very naive understanding of the reflection principle! (A related fact is that ZFC proves the consistency of any given finite fragment of the axioms of ZFC.)

On the other hand, any given mathematical text only contains finitely many formulas (unless it states a “theorem schema”, which does not usually happen I believe). The question is thus, phrased slightly provocatively:

Does the reflection principle imply that it must be possible to rewrite Higher Topos Theory in a way that avoids the use of universes?