Why doesn't the definition of a category require an explicit notion of morphisms equality?

Solution 1:

Morphism equality is indeed taken as primitive, but at an "even more primitive" level than composition.

Remember - ignoring set/class issues for the moment - composition consists of a partial function assigning to a pair of morphisms (on which it's defined) a third morphism, which we call their composition. So equality between morphisms is folded into the very nature of sets themselves (in this case, the sets of morphisms).

If you're familiar with model theory, equality is part of the logical language - on the same level as the quantifiers and Boolean connectives - while compositionof morphisms would be part of the signature (or language, or vocabulary, or ...), similarly to the symbol for the group operation in the context of groups.

Your second-to-last paragraph, though, is more special. The phenomenon you're describing there is actually something category theory explicitly doesn't want to pay attention to, at least most of the time, since one of the big points is that we can forget what the objects are and just look at how the morphisms behave. Certainly there's no object/morphism relation in general categories - for example, think about a group viewed as a one-object category.

Solution 2:

Category theory is ordinarily formulated within the framework of axiomatic set theory, just like the rest of mathematics. Axiomatic set theory includes equality as a primitive notion. So there is no need to separately specify equality as part of a category--you already know what equality means from your background foundation of mathematics. There is nothing special about category theory in this respect; this is just like how when defining a group, you don't have to specify what it means for two elements of the group to be equal, for instance.

Yes, the underlying notion of equality may include equalities that you don't want, such as a morphism being equal to an object. But this is not actually a problem at all--you will never talk about morphisms being equal to objects, so you don't care whether they are. Note in particular that an isomorphism between categories does not need to preserve such equalities.

(That said, there is some interest in alternate foundations of mathematics that are more strongly "typed", so that you can't talk about equalities of things that shouldn't "make sense". See for instance https://ncatlab.org/nlab/show/structural+set+theory. Again, though, this is in no way specific to category theory, nor is it at all logically necessary for the development of mathematics.)

Solution 3:

As the other answers state, for typical, set-theoretic foundations, a global notion of equality is always available. There is thus no need to explicitly provide a notion of equality, and it is always possible to ask whether two mathematical objects (i.e. sets) are equal. Functions, i.e. arrows of $\mathbf{Set}$, are sets and so are also objects of $\mathbf{Set}$. The function qua an object isn't "essentially exactly the same" as the function qua an arrow. They are exactly the same thing, no "essentially" about it.¹

However, this is not desirable for category theory. Ideally, you'd use a logical framework in which the principle of equivalence held. The principle of equivalence states that everything you state should be isomorphism invariant. Makkai developed FOLDS explicitly to provide such a logical framework. The slightly more usable Dependent FOL (DFOL) also accomplishes this goal as well. This is also typically accomplished by formalizations in dependent type theories such as the Calculus of (Inductive) Constructions. As I illustrate in this answer, formalizing the notion of category in DFOL would explicitly provide a (family of) notion(s) of equality for morphism. (And, notably, not provide a notion of equality for objects.)

Within traditional set-theoretic foundations, if you wanted to be more explicit about notions of equality, you could work in a setoid-enriched version of category theory. You would provide a (family of) setoid(s) of arrows² This would require composition to respect the setoid structure of its inputs. This would then impact the definition of things like functors.

¹ Technically, we would probably add the codomain (at least) to the notion of arrow for $\mathbf{Set}$ since hom-sets are usually defined to be disjoint in set-theoretic foundations. The resulting arrow is still a set, though, so that doesn't really change the story.

² Indeed, a (set-theoretic) model of the DFOL theory I sketch in the other answer would have arrows be a family of setoids.