>>13377171This category has a final object. But "this category" is just a pair of unary conditions, one that picks out the objects and one that picks out the morphisms.
So how does "final object" refer to a pair of unary conditions? A pair of unary conditions isn't a set! Definitions pick out sets from among all sets! Definitions can't pick out non-sets!
That's why you have to use a schema - ordinary definitions only let you use formal variables (sets); schema definitions let you add constant, relation, and function symbols. The data for an explicit schema definition therefore includes the signature information about the new symbols.
So to make this formal, we are going to have to parameterize the definitions with each signature of new symbols. In this case, we have two new unary relation symbols, Obj(x) and Mor(x) to pick out objects and morphisms.
Now we are ready to give the explicit definition: If Obj(x) and Mor(x) satisfy the axioms for being a category, then t is a (Obj,Mor)-final object if there is a unique morphism phi : x -> t for all x such that Obj(x).
If "final object" were an ordinary definition, then we would say
>The triple (Obj,Mor,t) is a final object is (Obj,Mor) is a category, t <- Obj, and ...And that's perfectly valid, but it only includes small categories, not large ones.
The issue is that the signature must expand by two additional relation symbols in order to handle large categories; ordinary explicit definitions aren't equipped to handle that.
