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_\kappa\subset 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 then 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, now settled by McLarty. 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 similarly 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 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?

**Edit (28.01.2021):** Thanks a lot for all the very helpful answers! I think I have a much clearer picture of the situation now, but I am still not exactly sure what the answer to the question is.

From what I understand, (roughly) the best meta-theorem in this direction is the following (specialized to HTT). Recall that HTT fixes two strongly inaccessible cardinals $\kappa_0$ and $\kappa_1$, thus making room for small (in $V_{\kappa_0}$), large (in $V_{\kappa_1}$), and very large (in $V$) objects. One can then try to read HTT in the following axiom system (this is essentially the one of Feferman's article "Set-theoretic foundations of category theory", and has also been proposed in the answer of Rodrigo Freire below).

(i) The usual ZFC axioms

(ii) Two other symbols $\kappa_0$ and $\kappa_1$, with the axioms that they are cardinals, that the cofinality of $\kappa_0$ is uncountable, and that the cofinality of $\kappa_1$ is larger than $\kappa_0$.

(iii) An axiom schema, saying that for every formula $\phi$ of set theory, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ and $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.

Then the reflection principle can be used to show (see Rodrigo Freire's answer below for a sketch of the proof):

Theorem. This axiom system is conservative over ZFC. In other words, any theorem in this formal system that does not refer to $\kappa_0$ and $\kappa_1$ is also a theorem of ZFC.

This is precisely the conclusion I'd like to have.

Note that $V_{\kappa_0}$ and $V_{\kappa_1}$ are models of ZFC, but (critically!) this cannot be proved inside the formal system, as ZFC is not finitely axiomatizable, and only each individual axiom of ZFC is posited by (iii).

One nice thing about this axiom system is that it explicitly allows the occasional arguments of the form "we proved this theorem for small categories, but then we can also apply it to large categories".

A more precise question is then:

Do the arguments of HTT work in this formal system?

Mike Shulman in Section 11 of https://arxiv.org/abs/0810.1279 gives a very clear exposition of what the potential trouble here is. Namely, if you have a set $I\in V_{\kappa_0}$ and sets $S_i\in V_{\kappa_0}$ for $i\in I$, you are not allowed to conclude that the union of the $S_i$ is in $V_{\kappa_0}$. This conclusion is only guaranteed if the function $i\mapsto S_i$ is also defined in $V_{\kappa_0}$ (or if $I$ is countable, by the extra assumption of uncountable cofinality). In practice, this means that when one wants to assert that something is "small" (i.e. in $V_{\kappa_0}$), this judgment pertains not only to objects, but also to morphisms etc. It is not clear to me now how much of a problem this actually is, I would have to think more about it; I might actually imagine that it is quite easy to read HTT to meet this formal system. Shulman does say that, with this caveat, the adjoint functor theorem can be proved, and as Lurie says in his answers, the arguments in HTT are of similar set-theoretic complexity. However, I'd still be interested in a judgment whether the answer to the question is "Yes, as written" or rather "Probably yes, but you have to put some effort in" or in fact "Not really". (I sincerely hope that the experts will be able to agree on roughly where the answer falls on this spectrum.)

A final remark: One may find the "uncountability" assumption above a bit arbitrary; why not allow some slightly larger unions? One way to take care of this is to add a symbol $\kappa_{-1}$ with the same properties, and ask instead that the cofinality of $\kappa_0$ is larger than $\kappa_{-1}$. Similarly, one might want to replace the bound $\mathrm{cf} \kappa_1>\kappa_0$ by a slightly stronger bound like $\mathrm{cf} \kappa_1>2^{\kappa_0}$ say. Again, if it simplifies things, one could then just squeeze another $\kappa_{1/2}$ in between, so that $\mathrm{cf} \kappa_{1/2}>\kappa_0$ and $\mathrm{cf} \kappa_1>\kappa_{1/2}$. This way one does not have to worry whether any of the "standard" objects that appear in some proofs stay of countable size, or whether one can still take colimits in $V_{\kappa_1}$ when index sets are not exactly of size bounded by $\kappa_0$ but have been manipulated a little.

PS: I'm only now finding all the relevant previous MO questions and answers. Some very relevant ones are Joel Hamkins' answers here and here.

really needed(the observations and measurements we make in real life are always very very very finite), but because it simplifies a lot of things. Mathematicians tend to shun annoying logic where we need to carefully make sure that all our formulas are suitable for our purposes (this is one of the reasons Quine's NF never fully caught on). This here is a real nice example for large cardinals alleviating this issue as well. It saves time and effort on bookkeeping. $\endgroup$ – Asaf Karagila♦ Jan 28 at 14:0318more comments