Lift a morphism onto the category theoretical product For three sets $X, Y, Z$, we can lift a morphism $f:Y\to Z$ onto the cartesian product with $X$, such that we get a morphism $\bar f:X\times Y\to X\times Z$ (obviously $\bar f(x,y)=(x,f(y))$).
How does that work in category theory? If $X, Y, Z$ are three objects in a category (which has products), how do I get a morphism $\bar f:X\times Y\to X\times Z$? Here, $\times$ denotes the product, i.e. the limit of the discrete diagram.
 A: You want to use the universal property of products, so you need arrows from $X \times Y$ to $X$ and $Z$, which will then give you an arrow from $X \times Y$ to $X \times Z$.  The first is the projection onto $X$ and the second is the projection onto $Y$ followed by the given arrow.
A: If a category $\mathcal{A}$ has products, then there is a functor:
$$\times : \mathcal{A} \times \mathcal{A} \to \mathcal{A}$$
which maps a pair of objects $(A,A')$ to $A\times A'$ and where $(f: A \to B, f' : A' \to B')$ is mapped to a morphism $f\times f' : A\times A' \to B\times B'$, which you get by the universal property of $B\times B'$ applied to the morphisms $f \circ \operatorname{pr}_1$ and $f' \circ \operatorname{pr}_2$ ($\operatorname{pr}_1$ and $\operatorname{pr}_2$ are the projections from $A\times A'$ to $A$ and $A'$ respectively).
Now take $\bar{f} = \operatorname{id}_X\times f$.
A: If the product of $B$ and $C$ exists, then there is a natural bijection
$$ \hom(A, B) \times \hom(A, C) \cong \hom(A, B \times C) $$
We can write the function in the forward direction as $(,)$: that is, it is the function that takes two morphisms $g : A \to B$ and $h : A \to C$ and produces the corresponding morphism $(g,h) : A \to B \times C$.
On $X \times Y$, we can let $x$ denote the projection map $X \times Z \to X$, $y$ denote the projection map $X \times Y \to Y$, and $f(y)$ denote the composite $f \circ y$.
Then, $(x, f(y)) : X \times Y \to X \times Z$ is precisely the morphism you want.
Even more suggestively, $(x,y)$ is the identity map $X \times Y \to X \times Y$, and thus
$$ \bar{f}(x,y) = (x, f(y)) $$
is a perfectly good category theoretic definition of $\bar{f}$.
This style of calculation can be formalized by developing the internal language of a category.
