Let $\mathcal{A}$ be a category whose collection of object forms a proper class. Then, to be able to formulate the concept of a terminal object in $\mathcal{A}$, do we have to leave ZFC? In other words, can we formulate the concept of a terminal object in $\mathcal{A}$ inside ZFC. If yes, how could we do it?
For example, in the category $\mathcal{Sets}$ of all sets. A singleton is a terminal object in $\mathcal{Sets}$, which could be checked by hand. But if we want to actually define what a terminal object is, then we have to quantify over all Sets, which is not a set. So, the definition is ill-formed inside ZFC?
A similar issue arises when we talk about things like injective objects, projective objects etc. of an arbitrary abelian category. How do we resolve this?
(I must be very confused about this basic issue; any help to resolve this will be greatly appreciated)
EDIT 1: What happens if in $\mathcal{A}$, $\hom(A,B)$ may also be proper classes where $A$ and $B$ are arbitrary objects of $\mathcal{A}$?
$(\forall u)(O(u)\to(\exists!f)H(f,u,t))$
, where $O(x)$ and $H(f,x,y)$ are formulas defining the classes of objects and morphisms of $\mathcal A$, respectively. $\endgroup$$\exists!x\,A(x)$
is a short hand for$\exists x\,\forall y\,(A(y)\leftrightarrow x=y)$
(or something equivalent), it does not involve the cardinality of any sets (or classes). $\endgroup$