Is it possible to formalize (higher) category theory as a one-sorted theory, just like we did with set theory? Set theory is typically formalized as a one-sorted theory without urelements.
Is it possible to do the same with category theory or higher category theory, formalizing the whole affair as a theory with only one type of object?
I know 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.


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?

 A: I think the trick that Zhen Lin is talking about in the comments is the following one. (If I am mistaking, please point it out.)
Take $\alpha$ a cardinal. An $\alpha$-sorted theory $T$ on the first-order language $\mathcal L$ with sorts $(X_k)_{k\leq\alpha}$ can be viewed as a one-sorted theory $T^+$ on the first-order language $\mathcal L^+ = \mathcal L \cup \{ P_k : k \leq \alpha \}$ where the $P_k$ are symbols of arity 1 relations and where the sentences of $T^+$ are obtained by substituting "$\forall x:X_k$" with "$\forall x \, P_k(x) \to$" and "$\exists x:X_k$" with "$\exists x:X_k\, P_k(x) \wedge$" in the sentences of $T$.
For example, the 2-sorted theory 
$$ \forall e:\mathrm{Elts}, \, \exists s:\mathrm{Sets}, \, e\in S  $$
on the language $\{\in\}$ can be understood as the $1$-sorted theory
$$ \forall e , \, E(e) \to (\exists s, \, S(s) \wedge e \in S)$$
on the language $\{\in, E, S\}$. In either case, you're talking about sets and elements and the theory states that every element must be contained by a set.

Taking Zhen Lin's comment into account, what's above only holds for $\mathcal L$ without function symbols and does not assert that relations act on the wanted sorts. So, for every function symbol $f : X_{i_1}\times\dots\times X_{i_n} \to X_k$ in $\mathcal L$, add a new relation symbol $R_f$ of arity $n+1$ in $\mathcal L^+$. Then add to $T^+$ the following axioms :
$$ \forall x_1,\dots,x_n,y,z, \, (R_f(x_1,\dots,x_n,y) \wedge R_f(x_1,\dots,x_n,z)) \to y=z, $$
$$ \forall x_1,\dots,x_n,y, \, R_f(x_1,\dots,x_n,y) \to (P_{i_1}(x_1) \wedge \dots \wedge P_{i_n}(x_n) \wedge P_k(y)).$$ 
(The first axiom assures that $R_f$ is a graph of a partial function).
Then, for every relation symbol $R$ of arity $n$ of $\mathcal L$ with input in the sort $X_{i_1} \times \dots \times X_{i_n}$, add to $T^+$ the axiom :
$$ \forall x_1,\dots,x_n, \, R(x_1,\dots,x_n,y) \to (P_{i_1}(x_1) \wedge \dots \wedge P_{i_n}(x_n)).$$
(I dont treat constants of $\mathcal L$ in here : constant symbols are just function symbols of arity $0$.)
Of course, it remains to substitute "$f(x_1,\dots,x_n) = y$" with "$R_f(x_1,\dots,x_n,y)$" in sentences of $T$.
