# Pullback of a single map

We work in a category where pullbacks exist. Given a map $$f:Y\to Z$$, there is a pull-back diagram $$\begin{array}& Y \times_Z Y & \stackrel{g_1}{\longrightarrow} & Y \\ \downarrow{g_2} & & \downarrow{f} \\ Y & \stackrel{f}{\longrightarrow} & Z \end{array}$$ (I am sorry for the awful formatting, is there a better solution?)

Of course, because of symmetry, we should have $$g_1=g_2$$. But category theory is a formal language, so I would like to have a formal proof of this, without hand-waving. I have not managed to find one so far, although I think that it should not be difficult... The farthest I've got is that there must be a unique map $$\phi: Y \times_Z Y \to Y \times_Z Y$$ such that $$g_1 \phi = g_2 \phi = g_1$$, because of the universal property of the pullback. Similarly, there is a unique $$\psi$$ such that $$g_1\psi=g_2\psi=g_2$$. But how do I continue from here?

It needn't be true in general that $$g_1 = g_2$$. In case you want to read more about such things, the morphisms $$g_1$$ and $$g_2$$ are called a kernel pair for $$f$$.
In the category of sets, for example, we can take $$Y \times_Z Y = \{ (a, b) \in Y \times Y \mid f(a) = f(b) \}$$ And then the functions $$g_1 : Y \times_Z Y \to Y$$ and $$g_2 : Y \times_Z Y \to Y$$ are given by projection onto the first and second coordinates, respectively. Then typically $$g_1 \ne g_2$$.
There are some cases where we might have $$g_1 = g_2$$. For example, if $$f$$ is a monomorphism, then since $$f \circ g_1 = f \circ g_2$$ it follows that $$g_1 = g_2$$. In fact, $$f$$ is a monomorphism if and only if $$(\mathrm{id}_Y, \mathrm{id}_Y)$$ is a kernel pair for $$f$$.