We assume ZFC+U.
A *category* is an ordered pair $(\operatorname{Ob} \mathcal{C},\operatorname{Mor} \mathcal{C},\operatorname{dom},\operatorname{codom},e,∘)$ of sets (not classes) and maps satifying some conditions.


Let $\mathbb{U}$ be a Grothendieck universe.
An element of $\mathbb{U}$ is called a *$\mathbb{U}$-set*.
A set is called *$\mathbb{U}$-small* if it is isomorphic to a $\mathbb{U}$-set.
In the following, we suppose that $\mathbb{N} \in \mathbb{U}$.


In SGA4, a category $\mathcal{C}$ is called *$\mathbb{U}$-small*
if $(\operatorname{Ob} \mathcal{C},\operatorname{Mor} \mathcal{C},\operatorname{dom},\operatorname{codom},e,∘)$ is $\mathbb{U}$-small
as a set (if my understanding is correct).
However, I don't see this definition working well.
For any set $a$ and $b$,
an ordered pair $(a,b)$ is always $\mathbb{U}$-small
since $(a,b)=\{\{a\},\{a,b\} \}$ is a set consisting of exactly two elements,
which is isomophic to $2:=\{\emptyset,\{\emptyset\}\} \in \mathbb{U}$.
Thus, $\mathbb{U}$-smallness imposes nothing on categories.
In particular, it is not equivalent to $\operatorname{Ob} \mathcal{C}$ and $\operatorname{Mor} \mathcal{C}$ are $\mathbb{U}$-small.


I think I am mistaken somewhere, where is it?



On the definition of small categories in SGA4
You’re correct: read literally, those definitions are mismatched, for the reasons you give. The solution is to fix the definition of “$U$-small category” to say that “$\newcommand{\C}{\mathcal{C}}\newcommand{\mor}{\mathrm{mor}}\mor(\C)$ is $\newcommand{\ob}{\mathrm{ob}}U$-small” — this is what the authors of SGA4 clearly intended (as clarified in the footnote on p2 of [this modern edition](http://www.normalesup.org/%7Eforgogozo/SGA4/tomes/SGA4.pdf), pointed out [by @abx in comments](https://mathoverflow.net/questions/439306/on-the-definition-of-small-categories-in-sga4#comment1133094_439306)), but expressed in a way that doesn’t depend on the precise encoding of the definition of categories or of ordered pairs.


There are two general points here:


* Outside of explicit investigations of set-theoretically foundational issues (and usually even within such contexts), *nothing* should ever depend on the specific set-theoretic implementation of ordered pairs. Anything that seems to depend on it can very safely be assumed to be a misunderstanding, an abuse of notation, or a mismatch of definitions.
* More generally, mathematics is usually written in “implementation-independent” ways as far as possible. Of course, there are often lapses from this in practice, and that sometimes leads to mismatches, as here. When such mismatches happen, the right fix is to rewrite the later definitions in more implementation-independent ways, *not* to tweak the implementation of the earlier definitions so that the implementation-dependent later definitions work. In ordinary human-practiced mathematics, this usually isn’t a problem, because it’s clear what people meant. But in computer-formalised mathematics (and programming more generally), this is a serious concern: if you go back and change the implementation of the earlier definition to make one later definition work, then that may break *anything else* that was written in an implementation-specific way. Implementation-dependent definitions are inherently fragile — so fix *them*, don’t take them as god-given and twist other things around to try to work with them.


