In Rethinking set theory Tom Leinster writes:
We could adapt the axiomatization in Section 2 by adding ‘element’ to the list of primitive concepts.
Assume we do so, that is, we add a relation symbol $\in$ to our formal system. Recall that in ETCS, there are the types "set" and "function between a set A and a set B". Between which types is $\in$ a relation?
My thoughts: The thing written to the right of $\in$ should be of type "set". But the thing written to the left of $\in$ can be of an arbitrary type: For functions $f: A\longrightarrow B$ we want to write $f\in B^A$, but we also want to write things like $\emptyset\in \{\emptyset\}$. So we cannot decide which type should be written to the left of $\in$. That is why I also ask the following question: In many-sorted first-order theories (that is first-order theories that are typed, that is, have types), is one allowed to have a relation between objects of any type? Or, when we have a relation $R(x, y)$, do we have to specify which type $x$ should have and which type $y$ should have?
Note that membership is really just the evaluation function $e: X \times 2^X \to 2$ in ETCS.
It is the case that in many-sorted first-order logic, the relation symbols are expected to have a sort specified for each argument. However, I don't believe ETCS is intended to have a sort for every set, because that would make the language uncountable. McLarty's formal presentation of ETCS has just two sorts, one for objects and one for morphisms. The presentation by Trimble and others is single-sorted (morphisms only).