Equality of objects in category theory

The identity functor is an identity arrow in the (large) category of (locally small) categories, so it is idempotent like any identity arrow. To be clear, a function, $f$, being idempotent means $f\circ f = f$. Also, $1_{\mathcal C}(X)=X$ is likely a definition. In an axiomatic approach, this might be accomplished by asserting that formula as an axiom, but in a set-theoretic approach, this would usually be interpreted as the set $\{(X,X)\mid X\in\mathsf{Ob}(\mathcal C)\}$ which is then referred to with the shorthand $1_\mathcal C$. The principle of equivalence talks about properties (or sometimes operations), what property, i.e. predicate, are you referring to with $1_\mathcal C(X)=X$? Are you taking $X$ as free? Well then this predicate is just always true by definition and thus trivially satisfies the principle of equivalence.

Taking a broader perspective, it is possible to define the notion of category in a framework where equality of objects is simply not a question that can be asked, there is no formula that corresponds to it. For example, this can be done using FOLDS or Belo's Dependently Sorted Logic or dependent type theory. This preprint by Erik Palmgren gives a relatively brief description of both FOLDS and (a variant of) Belo's system which he calls DFOL. If you are familiar with dependent type theory, these other systems are roughly the "first-order fragment" of a simple dependent type theory. For what I'm going to do, DFOL is a bit more handy as FOLDS lacks function symbols.

One signature for the DFOL theory of categories could be: $$\begin{array}% \mathsf{O}\ \mathsf{type}&& () \\ \mathsf{Hom}(A,B)\ \mathsf{type}&& (A,B:\mathsf O) \\ 1_A : \mathsf{Hom}(A,A)&& (A:\mathsf O) \\ f\circ g :\mathsf{Hom}(A,C)&& (A,B,C:\mathsf O,f:\mathsf{Hom}(B,C),g:\mathsf{Hom}(A,B)) \\ f = g\quad \mathsf{formula} && (A,B:\mathsf O, f,g:\mathsf{Hom}(A,B)) \end{array}$$ to which would be added axioms making $=_{AB}$ a congruence and the usual category axioms in terms of $=_{AB}$. Models of this wouldn't be categories exactly, but categories enriched in setoids. This is just to say that we have an equivalence relation on each hom-set, the interpretation of $=_{AB}$, and the operations are only defined up to equivalence. We can, of course, quotient by those equivalence relations in most set theories to get a standard category. It's actually awkward to add "equality" to $\mathsf{O}$ since presumably we'd then want something like $\mathsf{Hom}(A,B)=\mathsf{Hom}(A',B)$ when $A=A'$, but types aren't objects of the logic, i.e. there is no sort of types. There's a solution to this, but it is not obvious.

Homomorphisms of models of the above theory will be (setoid-enriched) functors. It can be proven that the principle of equivalence holds with respect to formulas written using the above signature. If we wanted to have a DFOL theory whose models were functors, we could start with two copies of the above signature, which I'll use subscript $1$ and $2$ to differentiate, and extend that with: $$\begin{array}% \mathsf F(A):\mathsf O_2 && (A:\mathsf O_1)\\ \mathsf F_{AB}(f) : \mathsf{Hom}_2(\mathsf F(A),\mathsf F(B)) && (A,B:\mathsf O_1, f:\mathsf{Hom}_1(A,B)) \end{array}$$ to which the functor laws are added as well as $\mathsf F_{AB}(f)=\mathsf F_{AB}(f')$ when $f=f'$. To be a bit more precise, this is the theory of a pair of categories and a functor between them. The models are a pair of (setoid-enriched) categories and a (setoid-enriched) functor between them. Continuing, we could extend this theory with: $$\begin{array}% \mathsf G(A):\mathsf O_1 && (A:\mathsf O_2)\\ \mathsf G_{AB}(f) : \mathsf{Hom}_1(\mathsf G(A),\mathsf G(B)) && (A,B:\mathsf O_2, f:\mathsf{Hom}_2(A,B)) \end{array}$$ and analogous laws to have a theory with a pair of functors going in both directions. Now, not only can we not state that $\mathsf G(\mathsf F(A))= A$ simply because we don't have an equality relation on objects, but we can't even state $\mathsf G_{\mathsf F(A)\mathsf F(B)}(\mathsf F_{AB}(f))=f$ as this isn't a well-formed formula: the left hand side is a term of sort $\mathsf{Hom}_1(\mathsf G(\mathsf F(A)),\mathsf G(\mathsf F(B)))$, while the right hand side is a term of sort $\mathsf{Hom}_1(A,B)$. We can easily add as data or assert the existence of isomorphisms between $\mathsf G(\mathsf F(A))$ and $A$ and similarly for $\mathsf F(\mathsf G(B))$ and $B$.