One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large categories are not even objects of the universe of discourse (though individual large categories can be considered by formulas defining their objects), and even working around that, we can't perform constructions like that of functor categories between them.
The most common way to deal with them is to wave your hands and say "universes!" which magically makes all your worries go away. (This is of course a joke, but it is generally understood that any such worrisome issues can be easily dealt with by passing to a higher universe.) I imagine in the context of proof assistants this is fairly convenient, as they generally are based on type theory which commonly have a hierarchy of universes as a built-in feature.
However many "purists" would not be content with this resolution as Grothendieck universes have strictly higher consistency strength than ZFC. There has been a fair bit of discussion in the past about whether the use of universes is ever of any real necessity, with the consensus strongly leaning towards "no" (see for instance this MO post or this one, also this one specifically about Wiles' work). Very few of these arguments however do any kind of "formal analysis" which would unambiguously remove the necessity of universes from such arguments.
I hereby ask: have there been any proposals to provide some formal tools which could transform a proof using universes into a proof in ZFC? This of course cannot be done in complete generality because ZFC+universes is not conservative over ZFC, but I could imagine some tool of this sort for uses of universes in the style of category theory.
