I'm now reading the proof of Mitchell's embedding theorem proved in the book of Swan 'Algebraic K-Theory'.


Now I'm trying to understand the sentence



> 
> '*It is well known that for a small abelian category $A$, the functor category from $A$ to the category $Ab$ of abelian groups is well powered, right complete, and has injective envelopes.'*
> 
> 
> 


To understand the well-poweredness, I tried to understand that for a functor $F$, $\{ F(X) \}\_{X \in \mathrm{obj}(A)}$ is a set.


I guess the relevant axiom in the set theory is the 'Axiom of Replacement' and it seems that the axiom is understood to be natural because if a collection of elements of a class is indexed by a set, then the collection is also a set because the cardinality of the collection is bounded by the index set. With this explanation, $\{ F(X) \}\_{X \in \mathrm{obj}(A)}$ must be a set.


But in the textbooks of set theory, there is a mention of the definable property (more precisely definable in the formal first order language) in the axiom of replacement.


So my question is


In the category theory, do we implicitly assume that a functor is definable? or if not the argument using the cardinality is formal enough?


(By the way, If you can also briefly explain the sentence of the Swan's book, then that would be also a great help! as I'm not meant to be a specialist in this field.)



Using Axiom of Replacement to construct the set of sets that are indexed by a set
For category theory, rather than using ZFC as the background theory, one usually works with an axiomatic system that treats classes a little more simply, like NBG. In NBG, the axiom of replacement has no definability requirement for class functions.


If you want to stick with ZFC, then yes you are implicitly assuming that functors are class functions, and hence are definable from first-order formulas in the language (possibly with set parameters).


I personally like to work with ZFC + an axiom of universes. In this view, one may take every category to be contained in a universe. Thus, every functor is actually a set, and hence definable (using that set as a parameter).


