$X \neq Y \Rightarrow id_X \neq id_Y$?

Question

Given two distinct objects $X$ and $Y$ in a category $C$, does it follow from the axioms that the identities $id_X$ and $id_Y$ are necessarily distinct?

The axioms here means those stated in Categories and Sheaves by Masaki Kashiwara and Pierre Schapira.

Answer 1

Kashiwara and Schapira use something like Tarski-Grothendieck set theory as a foundation. The definition of category given is then:

A category $\mathcal C$ consist of:

(i) a set $\mathrm{Ob}(\mathcal C)$,

(ii) for any $X,Y\in\mathrm{Ob}(\mathcal C)$, a set $\mathrm{Hom}_{\mathcal C}(X,Y)$,

(iii) for any $X,Y,Z\in\mathrm{Ob}(\mathcal C)$, a map $$\mathrm{Hom}_\mathcal C(X,Y)\times\mathrm{Hom}_\mathcal C(Y,Z)\to\mathrm{Hom}_\mathcal C(X,Z)$$ called the composition and denoted by $(f,g)\mapsto g\circ f$

followed by associativity and identity laws for $\circ$.

This does not imply that hom-sets are disjoint. We can easily create categories with overlapping (or even identical) hom-sets for different objects. For example, consider a discrete category with more than one object and simply define the hom-sets to be identical singleton sets.

You can compare this formulation with the one I give here using DFOL as a foundation. However, the difference in foundations matters. Kashiwara and Schapira have almost certainly made a mistake in this definition and should be requiring that the hom-sets are disjoint, or, alternatively, require an explicit source and target function (which would then force the hom-sets to be distinct). Leinster uses the same definition as Kashiwara and Schapira but in a more ambiguous foundations and explicitly includes Remark 1.1.2 (e):

If you believe it makes sense to form the intersection of an arbitrary pair of abstract sets, you should add to the definition of category the condition that $\mathscr A(A,B)\cap\mathscr A(A',B')=\varnothing$ unless $A=A'$ and $B=B'$.

If you don't "believe it makes sense to form the intersection of an arbitrary pair of abstract sets", you essentially get the definition I gave which I referenced above where asking whether $X=Y$ for objects $X$ and $Y$ doesn't make sense, i.e. is not a well-formed formula in the relevant language, so the question of disjointness of hom-sets can't even be formulated.

Notation 1.2.2 in Kashiwara and Schapira define the notion of the source and target of a morphism, but these are ill-defined if we don't require hom-sets to be disjoint.

As suggested by the DFOL formulation, most of the time the issue just won't come up. To ask a question that depends on hom-sets being disjoint is to ask an evil question. The point of approaches like FOLDS and DFOL is to make it impossible to ask such evil questions. Sometimes we want to think about (small) categories as models of essentially algebraic theories (though it isn't always described this way), and in that context it usually makes the most sense to have explicit source and target operations in the theory which will then force the hom-sets to be disjoint. Indeed, in that context, hom-sets are a derived concept and there is a set of all morphisms partitioned by pairs of objects into hom-sets via the source and target maps.