The following proposition is from Herrlich and Strecker's Category theory (2nd ed.):
29.1 PROPOSITION
Let $C \;\mathop{\rightrightarrows}\limits^f_g \;D$ be a pair of $\mathscr{A}$-morphisms [in some category $\mathscr{A}$]. Then the following are equivalent:
- $f = g$.
- For each $\mathscr{A}$-object $A$, $\hom(A, -)(f) = \hom(A, -)(g)$.
Proof: Clearly (1) implies (2). If (2) holds, then $ f = f\;{\scriptstyle\circ}\;1_C = \hom(C, f)(1_C) = \hom(C, g)(1_C) = g\;{\scriptstyle\circ}\;1_C = g.\;\;\;\;\square $
I think I understand both the theorem's statement and its proof, and yet the whole thing makes no sense to me. First, the $1 \Rightarrow 2$ implication is at once too banal to merit notice, and unnecessarily weak, since $f = g$ in fact implies $F(f) = F(g)$ for every functor $F$.
Second, the $2 \Rightarrow 1$ implication is more interesting, but I don't understand why its antecedent was made so strong.
Why isn't enough to require simply that $\hom(C, -)(f) = \hom(C, -)(g)$?