Roughly: This question concerns the process and the constructive nature of formalizing and proving category theoretic statements within $\textsf{ZFC}$.
$\textsf{ZFC}$ can only talk about sets, while proper classes live in the metatheory as explicit first order formulae. Statements about classes are always to be interpreted as schemes in the metatheory of $\textsf{ZFC}$ beginning with some (meta-theoretic) quantification "For any formula $\phi(x)$, …".
In particular, this applies to non-small categories. A statement about some family of categories has to be interpreted as a scheme in the metatheory beginning with "For any three formulas $\text{Obj}(x)$, $\text{Mor}(x,y,z)$, $\text{Comp}(x,y,z,f,g,h)$ defining the objects, morphisms and compositions of a category [maybe some extra properties], …". The meta-theoretic quantification gets richer in case several categories and/or functors between categories and/or transformations between functors are given.
The above concerns the translation of the assumptions of a category-theoretic statement into the meta-theory of $\textsf{ZFC}$. As for the conclusion, it might be that it just concerns some properties of the categories under consideration, like 'In any abelian category epimorphisms are stable under pullback'; in this case, the conclusion is just a single formula of $\textsf{ZFC}$, so the whole statement translates into a meta-theoretic scheme of the form "For any formulas $\phi,\psi,…$, $\textsf{ZFC}\vdash \text{(Some explicit formula involving }\phi,\psi,…\text{)}$".
This is different if the conclusion concerns the existence of certain categories, functors, natural transformations… Again, as one cannot quantify over proper classes within $\textsf{ZFC}$, the formalization of such a statement as a scheme in the metatheory of $\textsf{ZFC}$ requires that the objects whose existence is claimed can be explicitly defined, within the finitistic meta-theory, as certain first-order formulae.
Observation: Proofs of statements about the existence of categories and functors have to be explicit/constructive when they ought to be formalizable within $\textsf{ZFC}$
My question now simply is:
Question A: Are most existence results of standard category theory indeed constructive?
I have doubts that this is the case, which would mean that $\textsf{ZFC}$ is really insufficient for formalizing category theory, even in principle. For example, consider the statement:
Example: Any fully faithful and essentially surjective functor is an equivalence
How to formalize this in $\textsf{ZFC}$? Is there any way to derive from any family of formulas defining two categories ${\mathscr C},{\mathscr D}$ and a fully faithful and essentially surjective functor ${\textbf F}:{\mathscr C}\to{\mathscr D}$ between them three formulas defining an inverse functor ${\textbf G}: {\mathscr D}\to {\mathscr C}$ and equivalences ${\textbf F}{\textbf G}\cong\text{id}_{\mathscr D}$ and ${\textbf G}{\textbf F}\cong\text{id}_{\mathscr C}$?
As in the development of (small) category theory within $\textsf{ZF}$, one might try to resolve this by using anafunctors instead of functors. That is, statements about functors should be formalized as schemes in the meta-theory concerning formulas defining anafunctors; this essentially means that we ignore this single issue of explicitly inverting fully faithful and dense functors by formally adding their inverses.
Question B: Does Question A have a positive answer in case functors are always formalized as anafunctors?
For example, one might now consider more complicated statements like the adjoint functor theorem and ask whether they can be formalized within $\mathsf{ZFC}$ when anafunctors are used instead of functors. In other words: are their proofs constructive up to inverting fully faithful and dense functors?
Clarification: (1st edit) By "constructive" I do only refer to the proofs of existence statements about categories and functors: I wonder whether (maybe up to the formal inversion of fully faithful and dense functors through the use of anafunctors) from proofs of such statements one can extract explicit first-order formulae defining the desired categories and (ana)functors.
Then, and only then, the statement could indeed by formalized as a scheme in the meta-theory of $\textsf{ZFC}$.
I do not necessarily want to replace $\textsf{ZFC}$ by $\textsf{ZF}$ or even some intuitionistic set theories. My primary goal is to understand whether $\textsf{ZFC}$ can in principle serve as a home for basic category theory through the use of schemes in the meta-theory.
For example, although unlikely, it is not clear to me whether there could be an algorithm turning formulae describing a fully faithful and dense functor into another formula describing a quasi-inverse.
Best Answer
Your first observation has been fleshed out by Bénabou in his paper cited below.
My experience with category theory indicates that the answer to Question A is Yes after removing useless applications of the global axiom of choice, which is used especially in the theorem that fully faithful essentially surjective functors are equivalences. Why useless? Most equivalences of categories in practice appear as adjoint equivalences where the pseudo-inverse functor, as well as unit and counit, are already given.
It is often critized that ZFC doesn't enable us to talk about the category of all functors $\mathsf{Set} \to \mathsf{Set}$. Before moving into more sophisticated foundations (Grothendieck universes, homotopy type theory, etc.), we should first ask ourselves if it is really necessary to talk about this wild category. I would argue that ZFC is not able to formalize all of category theory, but it is able to formalize 99% of category relevant for practice.
The following papers deal with ZFC-foundations of category theory: