This is a modification of a question I asked earlier.
In that question, I hadn't placed any limits on the number of binary relations allowed, so my question had an affirmative answer, but a trivial and uninteresting one. This modification effectively changes the question by making it much less trivial, so this is not a duplicate post.
ZFC set theory is typically formalized as a one-sorted theory without urelements, and with a signature containing one primitive binary relation and no primitive functions.
Is it possible to do the same with category theory or higher category theory, formalizing a universe of categories as a first-order theory with only one type of object, one binary relation, and no functions?
To clarify: what I want is to formulate a first-order theory of an entire "universe" of categories, much like ZFC is a "universe" of sets - not a first-order theory in which the models are individual categories in general. This could be done in several ways: the universe could be a category itself, effectively formalizing Cat in an "Elementary Theory of the Category of Categories." Or, you could perhaps think of it as a theory of the 2-category of 1-categories, or something like that. (The discussion with user18921 in the comments made it clearer to me that there was some confusion on this point.)
If the above is impossible, then as a small concession, I'll allow a single binary function $\circ$ to denote composition, though it would be nice to see if it's possible even without that. I would expect that it is, much in the same way that $\cup$ and $\cap$ don't need to be defined explicitly as function symbols in the signature of ZFC. (You could also probably formalize $circ$ instead as a binary relation, just denoting that the composition of two functions exists.)
As before, I understand that this runs counter to what some feel is the philosophical spirit of category theory, but I'm still curious if it's possible anyway, just as an interesting logical puzzle.
My comments from before are repeated, as they still apply, and are now more pertinent that the trivial solution to the original question no longer applies:
It seems tricky to me at first glance. A "category" has a "set" of "objects" and another set of "morphisms." That's already four sorts of thing - category, set, object, morphism.
However, it's possible to identify an "object" with the identity morphism on that object. So, you could perhaps use this idea to bring you down to only three sorts of thing - category, set, and morphism.
Alternatively, you could say that "object" and "morphism" are both types of the more fundamental n-morphism, and arrive at a three-sorted theory of categories, sets, and n-morphisms.
You could also try to formalize a "set" as a discrete category, and bring you down to only two sorts of thing - category and (n-)morphism.
If you go with n-morphisms, maybe you could try to identify every n-morphism with the (n+1)-identity morphism on it, and see if that simplifies things somehow.
The above are some ideas that I had; I'm not even sure if they'd work. But assuming they do, that still leaves you with only two things - categories and morphisms - and I'm not sure if it's possible to go one step further and get it down to one thing. Thoughts?
The answer to the logical puzzle is "yes". For any finite signature $\Sigma$, there is a sentence $\chi$ in the language of a single binary relation such that models of $\Sigma$ are bi-interpretable with models of $\chi$ (Hodges, Model Theory, Theorem 5.5.1).