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)$?
Xholds if and only ifYholds "for all possiblez", and that this holds if and only ifYholds "for a particular choice ofz." My paraphrase was not meant to be formal or precise, merely indicative ("...if and only if for all Ablah" and then showing this in turn is equvalent to "... if and only if for this specific choice of Ablah"). – Arturo Magidin Feb 1 '12 at 20:45