$\mathscr{U}$-categories and $\mathsf{Hom}$-functors Let $\mathscr{U}$ be a universe. Call a set $X$ $\mathscr{U}$-small if there is a set $Y \in \mathscr{U}$ so that $X \cong Y$. Call a category $\mathsf{C}$ a $\mathscr{U}$-category if for any $X,Y \in \mathsf{C}$, $\mathsf{Hom_C}(X,Y)$ is $\mathscr{U}$-small.
Assume $\mathsf{ZFC}$ as our foundational system (not Bourbaki set theory). 
Let $\mathsf{C}$ be a $\mathscr{U}$-category and let $\mathscr{U}\text{-}\mathsf{Set}$ be the category of all sets which belong to $\mathscr{U}$.
How do we construct a $\mathsf{Hom}$-functor $\mathsf{Hom_C}(X,-)\colon\mathsf{C}\to\mathscr{U}\text{-}\mathsf{Set}$? Note for every $Y \in \mathsf{C}$, $\mathsf{Hom_C}(X,Y)$ doesn't belong to $\mathscr{U}\text{-}\mathsf{Set}$, but rather is isomorphic to a set in there. Grothendieck in SGA uses Bourbaki set theory and $\tau$ choice operator (also axiom $\mathscr{U}$B), while in $\mathsf{ZFC}$ we don't have that. 
Is it even possible to work with these definition in $\mathsf{ZFC}$?
 A: This depends on what definition of category you have taken: do you assume the objects form a set?
(I’ll avoid the terminology “small category”, since while this is sometimes used to mean “objects form a set”, it’s also used to mean “objects form a $U$-set”, for some universe $U$ whose sets have been earlier designated as “small”.)
If you’ve taken the definition where objects of a category are always assumed to form a set, then there’s no problem: just use the axiom of choice.  For each $X, Y$ in $\operatorname{ob} C$, you know there exist some set in $U$ and isomorphism $C(X,Y) \cong U$; so by the axiom of choice, there’s a function which chooses, for each $X$, $Y$, some such set and isomorphism.  Given this, the construction of the hom-functor is straightforward.
If you’re not assuming that the objects of a category form a set — i.e. you define a category to have a class of objects — then life gets rather subtle, because categories in this sense aren’t something you can really talk about inside ZFC.  You can represent classes by predicates, and so talk about individual categories (or parametrised families of categories) schematically — so any theorem about arbitrary categories is really a theorem schema.  Or you can extend your language to something like NBG set theory, where you really can talk about classes (and hence categories) directly.
In either of those setups of “large categories”, I don’t see how you can define the hom-functor for an arbitrary $U$-category without invoking something approaching the axiom of global choice, which essentially gives you choice functions on classes instead of sets.  Given global choice, we can construct hom-functors essentially by re-running the argument used for the small case above.
Using the language of NBG, one can ask whether the existence of hom-functors for all such categories is (a) independent of NBG (which is conservative over ZFC), or (b) equivalent over NBG to the axiom of global choice.  It’s equivalent to the statement “there is a global choice function for non-empty $U$-small sets”, if I’m not mistaken. My guess would be that this statement is independent of NBG, but strictly weaker than full global choice. I can’t substantiate either part of this, off the top of my head, but I think for someone less rusty than me on the relevant techniques, it should be fairly standard.
A: If we wish to do this while keeping all the properties that the construction in SGA 4.I.1.3 has, then I think it is not possible:
Given objects $X$ and $Y$ such that ${\rm Hom}(X,Y)\notin\mathscr{U}$, we have to choose canonically a set in $\mathscr{U}$ with the same cardinality as ${\rm Hom}(X,Y)$; the only candidate that comes to my mind is the cardinality of ${\rm Hom}(X,Y)$. But now we also have to canonically choose a bijection between ${\rm Hom}(X,Y)$ and its cardinality, which is impossible.
A: I think in this approach, you also need Grothendieck's axiom for universe besides ZFC, namely you have to admit for any set $A$, there is a universe $\mathcal{V}$ with $A \in \mathcal{V}$.
Once Grothendieck's axiom on universe is valid, one can only consider small categories in the sense that both the class of the objects and class of morphisms are sets---all the usual categorical constructions, such that forming functor categories as in this question, just produces small categories in an even bigger universe.
With that being said, we can assume that there exists a big universe $\mathcal{V} $, such that the set of objects of $C$ and all him-sets of $C$ are all elements of $\mathcal{V} $. Then for any $X\in \mathcal{V} $, we can form the set $\tau_X$ of injective maps from $X$ into $\mathcal{U} $. Then you can form the product set $\prod_{X \in \mathcal{V} } \tau_X$. An element in this product set, which exists by the axiom of choice for sets, serves as your $\tau$ operator. And you can continue your constructions with the help of this element. When more and more categories are involved for whatever purpose later, you can always take even bigger universe $\mathcal{V} $ to have a global choice of bijections. This allows you to abandon the full power of the $\tau$ operator and use the axiom of choice for a big enough universe instead. 
