Qfyilyi

I am learning basics of the category theory (CT).

I do understand that CT is a modern powerful framework to describe various branches of mathematics in a unified way.

I do admit that category's definition tells a lot about the whole thing and focuses on the most important properties, shadowing unnecessary details. However, the more I go forward, the more it feels like it should explicitly require a notion of morphisms equality (like it does with morphism composition). It feels so because equality or inequality of morphisms arises everywhere, since the very beginning: any commutative diagram eventually reduces to an equality of two different paths and many other things involve equality as well. Even composition is defined grouding upon an (implicit) equality!

I'll try to give an example of my concern. Consider $mathbb{SET}$. Its objects are sets and morphisms are functions. Now, let's recall that functions are sets as well - to be more precise, a function $f : A mapsto B$ is a subset of a $A times B$ obeying certain properties, which I omit. Thus, one could argue that $f$ is both a morphism between objects $A, B in Obj(mathbb{SET})$ and an object defined as a set of pairs ${ (a_1 in A, b_1 in B), ..., (a_n in A, b_n in B) }$ and those are equal because both are essentially exactly the same thing.

I hope my concern is clear and I need some kind of "conceptual insight" from knowledgeable people to move forward. Please give me the right perspective.

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.

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.)

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.