I'm getting a bit lost over at Peter Scholze's interesting question about removing the dependence on universes from theorems in category theory. In particular, I'm being forced to admit that I don't really know when replacement is being invoked, never mind when it is invoked "in an essential way". So I'd like to work through a reasonably concrete example of the phenomenon. I understand that replacement should "really" be thought of as the axiom which allows for transfinite recursion. My sense is that category theory tends not to use recursion in a heavy-duty way (although, more so than other branches of mathematics, it does have plenty of definitions which at least prima facie have nontrivial Levy complexity. For instance, I think the formula $\phi(x,y,z,p,q)$ saying that the set $z$ and functions $p: z \to x$ and $q: z \to y$ are a categorical product of the sets $x,y$ is syntactically $\Pi_1$, and the statement that binary products exist in the category of sets is syntactically $\Pi_3$ (ignoring bounded quantifiers of course)).
The following theorem is, I think, one of the notable exceptions to the category-theoretic-non-use-of-recursion:
Theorem [Quillen] "The small object argument": Let $\mathcal C$ be a locally presentable category, and let $I \subseteq Mor \mathcal C$ be a small set of morphisms. Let $\mathcal L \subseteq Mor \mathcal C$ be the class of retracts of transfinite composites of cobase-changes of coproducts of morphisms in $I$, and let $\mathcal R \subseteq Mor \mathcal C$ comprise those morphisms weakly right orthogonal to the morphsims of $I$. Then $(\mathcal L, \mathcal R)$ is a weak factorization system on $\mathcal C$.
For the proof, see the nlab. Basically, factorizations are constructed by transfinite recursion. The recursion seems "essential" to me because new data is introduced at each stage of the construction.
Formalization:
I think this theorem and its proof are straightforwardly formalizable in MK, where the category-theoretic "small/large" distinction is interpreted as MK's "set/class" distinction. I don't feel qualified to comment on whether the proof works in NBG, but the statement at least makes sense straightforwardly.
When it comes to formalizing in ZFC, we have choices to make regarding the small/large distinction:
One option is to introduce a "universe" $V_\kappa$ (which, if we're actually trying to work in ZFC, will be a weaker sort of universe than usual). We'll interpret "small" to mean "in $V_\kappa$". We won't consider "truly large objects" -- everything we talk about will be a set -- in particular, every category we talk about will be set-sized, even if not "small" per se. We'll interpret "locally presentable category" to mean "$\kappa$-cocomplete, locally $\kappa$-small category with a strong $\kappa$-small, $\lambda$-presentable generator for some regular $\lambda < \kappa$" (I don't know if it makes a difference to say that $V_\kappa$ thinks $\lambda$ is a regular cardinal).
Another option is to not introduce any universe, and just interpret "small" to mean "set-sized". In this case, any "large" object we talk about must be definable from small parameters. So we define a category to comprise a parameter-definable class of objects, a parameter-definable class of morphisms, etc. This might seem restrictive, but it will work fine in the locally presentable case, since we can define a locally presentable category $\mathcal C$ to be defined, relative to parameters $(\lambda, \mathcal C_\lambda)$ (where $\lambda$ is a regular cardinal and $\mathcal C_\lambda$ is a small $\lambda$-cocomplete category), as the category of $\lambda$-Ind objects in $\mathcal C_\lambda$.
Now, for the theorem at hand, approach (2) seems cleaner because the necessary "tranlsation" is straightforward, and once it is done, the original proof should work without modification. I think the main drawbacks of (2) come elsewhere. For instance it will probably be a delicate matter to formulate theorems about the category of locally presentable categories. In general, there will be various theorems about categories which have clean, conceptual formulations and proofs when the categories involved are small, but which require annoying technical modifications when the categories involved are large. It's for such reasons that approaches more like (1) tend to be favored for large-scale category-theoretic projects.
So let's assume we're following approach (1). The question then becomes:
Question 1: Exactly what kind of universe do we need to formulate and prove the above theorem following approach (1)?
Question 2: How many such universes are guaranteed to exist by ZFC?
Presumably, the answer to Question 2 will be that there are a lot of such universes -- enough so that we can do things like, given a category, pass to a universe large enough to make that category small and invoke the theorem for that universe.
Question 3: How far into the weeds must we go to answer Questions 1 and 2?
Do we have to analyze the proof of the Theorem in a deep way? Is there an easy rubric of criteria which allow us to glance at the proof and, for 99% of theorems like this, easily say that it "passes" without delving into things too much? Or is there even some formal metatheorem we can appeal to such that even a computer could check that things are fine?