I'm trying to understand, precisely, what a "quotient category" is. I've looked at several different definitions and they all seem to vary so I'm having a hard time nailing this concept down. A more-or-less typical definition is given by Rotman in Introduction to Algebraic Topology. Central to actually understanding the quotient category is understanding what congruence means in this context which Rotman defines as follows:
A congruence on a category $C$ is an equivalence relation $\sim$ on the set of all morphisms of $C$ such that $f \in \mathsf{Hom}(A,B)$ and $f \sim g$ then $g \in \mathsf{Hom}(A,B)$ and for $f_1 \sim f_2$ and $g_1 \sim g_2$ if the composite $g_1 \circ f_1$ exists then $ g_1 \circ f_1 \sim g_2 \circ f_2 $
The first thing I want to do with this is show that it is indeed an equivalence relation but, honestly, I'm not sure exactly what the equivalence classes are. It seems to me that in order for two functions to be related they must, first of all, have the same domain and the same codomain. The other observation is that, loosely speaking, the relation must respect composition in the obvious way. Other than these conclusions, I don't really see the point of the definition. Yes, the relation partitions the morphisms in $C$ but hom-sets in $C$ are already pairwise-disjoint by the definition of category.
I'm sure there's a subtlety of the definition I'm overlooking but would appreciate a clear explanation of exactly what's going on here, specifically, why introduce a relation to partition the morphisms of $C$ when this partition already exists by definition?