One way to define a category set-theoretically might be to give four $\in$-formulas (not sets!)
$$\begin{array}{rl} \mathsf{O}(X)&\text{(“$X$ is an object”)}\\ \mathsf{M}(X,Y,z)&\text{(“$z$ is a morphism from $X$ to $Y$”)}\\ \mathsf{C}(x,y,z)&\text{(“$z$ is a composition of $x$ and $y$”)}\\ \mathsf{I}(X,y)&\text{(“$y$ is an identity of $X$”)} \end{array}$$
for which some formulas (“axioms”) are provable from the axioms of set theory. The ingredients of a thus definable category $\mathcal{C}$ will be given (not necessarily as sets) by
$$\begin{array}{rcl} \operatorname{Obj}(\mathcal{C})&:\equiv&\lbrace X\ :\ \mathsf{O}(X) \rbrace\\ \operatorname{Mor}(\mathcal{C})&:\equiv&\lbrace (X,Y,z)\ :\ \mathsf{M}(X,Y,z)\rbrace\\ \operatorname{Hom}_\mathcal{C}(X,Y)&:\equiv&\lbrace f\ :\ (\exists z)\ f = (X,Y,z) \wedge \mathsf{M}(X,Y,z)\rbrace \end{array}$$
The “axioms” include some sort of typing axioms:
$$\begin{array}{rcll} \mathsf{M}(X,Y,z)&\rightarrow&\mathsf{M}_1(X,Y)&\\ \mathsf{C}(x,y,z)&\rightarrow&\mathsf{C}_1(x,y,z)&\\ \mathsf{I}(X,y)&\rightarrow&\mathsf{I}_1(X,y)& \end{array}$$
with the typing conditions
$$\begin{array}{rcl} \mathsf{M}_1(X,Y)&:\equiv&\mathsf{O}(X)\ \wedge\ \mathsf{O}(Y)\\ &&\text{(“morphisms are from objects to objects”)}\\ \mathsf{C}_1(x,y,z)&:\equiv&(\exists X,Y,Z)\ \ \mathsf{M}(X,Y,x)\ \wedge\ \mathsf{M}(Y,Z,y)\ \wedge\ \mathsf{M}(X,Z,z)\\ &&\text{(“only morphisms between appropriate objects can be composed”)}\\ \mathsf{I}_1(X,y)&:\equiv&\mathsf{M}(X,X,y)\\ &&\text{(“identities are morphisms from an object $X$ to itself”)}\\ \end{array}$$
Looking at some examples and thinking of other definable categories I know, I get the impression that the typing conditions are often either explicitly built-in in the formulas $\mathsf{M}, \mathsf{C}, \mathsf{I}$ (e.g. $\mathsf{C} :\equiv \mathsf{C}_1 \wedge \mathsf{C}'$) or the typing axioms hold otherwise tautologically (e.g. $\mathsf{M} \equiv \mathsf{M}_1 \wedge \mathsf{M}'$), i.e. hold independently of the axioms of set theory.
I am looking for an example of a category $\mathcal{C}$ definable by formulas $\mathsf{O}, \mathsf{M}, \mathsf{C}, \mathsf{I}$ as above, fulfilling the “axioms”, for which the typing axioms are not fulfilled tautologically, i.e. require the axioms of set theory.
