Equivalent categories are elementarily equivalent: Formalization?

Equivalent categories should be elementarily equivalent in the sense of mathematical logic. How to make this precise? Here is an attempt:

Let $F : \mathcal{C} \to \mathcal{D}$ be an equivalence of categories. Let $\phi$ be a formula in the language of categories with $n$ free object variables and $m$ free morphism variables, with the following property: No objects are said to be equal or non-equal, and morphisms can only be said to be equal or non-equal if they have the same source and target. Then for objects $X_1,\dotsc,X_n$ and morphisms $f_1,\dotsc,f_m$ in $\mathcal{C}$, we have $$\phi^{\mathcal{C}}(X_1,\dotsc,X_n,f_1,\dotsc,f_m) \Leftrightarrow \phi^{\mathcal{D}}(F(X_1),\dotsc,F(X_n),F(f_1),\dotsc,F(f_m)).$$

The crucial assumption, in italics, shows what is really the difference between equivalences of categories and isomorphisms of categories: We cannot talk about equality of objects. And we cannot talk about equality of morphisms, unless they are parallel.

I guess the statement is more or less known and clear enough, but still not formalized enough (in terms of mathematical logic) in order to prove it properly. I guess that our language, from which $\phi$ is built, consists of two sorts, called "objects" and "morphisms" (although categories may be axiomatized with only one sort "morphisms", I doubt that this is convenient here), and that we have function symbols $s,t$ from morphisms to objects, called "source" and "target", a function symbol $\circ$ from pairs of morphisms to morphisms, called "composition", and finally a function symbol from objects to morphisms. We don't want an equality relation between objects. But we want an equality relation between parallel morphisms. I don't know how to make this precise. Somehow, in each formula, each appearance of $f=g$ should be replaced by $(f=g) \wedge s(f)=s(g) \wedge t(f)=t(g)$. But I have never heard of such replacements in mathematical logic. Is it possible to find a theory in a suitable language such that the formula $\phi$ in the statement about equivalences of categories can be any well-formed formula? Based on my own experience with category theory, there are almost no statements of the form "there is a morphism $f$ such that ...", but rather "there is a morphism $f : A \to B$". If this could be formalized, then the equality relation should be defined only between two morphisms $f : A \to B$ and $g : A \to B$. Perhaps this will be kind of a two-sorted language with "parameters"?

The question has been studied by various authors:

• Freyd, 1976, Properties invariant within equivalence types of categories [MR0412249].
• Blanc, 1978, Équivalence naturelle et formules logiques en théorie des catégories [MR0539867].
• Makkai, 1995, First order logic with dependent sorts, with applications to category theory.

I'm afraid I am not familiar with the details of any of these, but I can say that FOLDS is probably the best bet. Frankly, I don't think any of these results will be especially useful – the restriction to first order logic is a severe restriction in practice. I quote Lambek's review of Freyd's paper:

How useful are the results of this paper? The ring theorist concerned with Morita equivalence of certain properties of rings must study the invariance under equivalence of certain properties of module categories. For example, he might consider such sentences as "every module is projective'' and "there exists a Noetherian generator''. It would seem that the first could in principle be handled by translating it into logical notation and checking Freyd's conditions, while the second must await an extension of Freyd's methods to non-elementary sentences. How long will ring theorists continue to wave their hands?

The statement as you've written it down is still not true. It seems to me that you can still write down statements like "there are at least $n$ different morphisms" and these sorts of statements are not invariant under equivalence of categories (where I understand "different" to mean that either the source differs, the target difers, or the source and target are the same but the morphisms are not equal in the parallel sense).