I am reading "Category Theory" (2nd ed.) of Awodey, and I'm stuck at page 96 (proposition 5.12) when pullbacks are presented as functors:

The pullback under question corresponds to this square:

$$\begin{matrix} C' \times_C A & \xrightarrow{h'} & A \\[1ex] \downarrow \rlap{\scriptstyle{\alpha'}} & & \downarrow\rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

Here is the statement of Awodey's book that I do not understand:

Pullback is a functor. That is, for fixed $C' \rightarrow_h C$ in a category $\mathbf{C}$ with pullbacks, there is a functor

$h^* : \mathbf{C}/C \rightarrow \mathbf{C}/C'$

defined by

$(A\rightarrow_\alpha C) \mapsto (C'\times_C A \rightarrow_{\alpha'} C')$

where $\alpha'$ is the pullback of $\alpha$ along h

The problem that I see is that, given initially:

$$\begin{matrix} & & A \\[1ex] & & \downarrow \rlap{\scriptstyle{\alpha}} \\[1ex] C' & \xrightarrow{h} & C \end{matrix}$$

there can be several pullbacks on it, for example, in addition to $(\alpha',h')$, there could be $(\alpha_2',h_2')$, and the unique condition is that there exists an isomorphism $i$ such that $\alpha_2' = \alpha\circ i$ and $h_2' = h'\circ i$. Worse, given a pullback $(\alpha',h')$, one can build as many as pullbacks as there exist isomorphisms, as given any isomorphism $j$ (with domain $C' \times_C A \rightarrow_{h'}$) the two arrows $(\alpha'\circ j,h' \circ j)$ form a new pullback.

So, how could we build a functor if the image arrow is only defined up to an arbitrary isomorphism?

chooseone pullback for each cospan, and show thatanyfamily of choices defines a functor. (That is why Awodey writes "afunctor"!) $\endgroup$ – Zhen Lin Dec 11 '12 at 14:08afunctor, but he also writesthepullback, so Almeo's point is well taken. The writing is indeed sloppy. Almeo: Zhen's solution does work, though: For each diagram, arbitrarily choose a pullback --- then you'll get a (non-uniquely-defined) functor. $\endgroup$ – Steven Landsburg Dec 11 '12 at 14:16apullback functor" then your comment would be relevant, as in this case we would be talking about one of many different pullback functors (all of which are naturlly isomorphic). I think it is not Awodey who is sloppy here. $\endgroup$ – Andrej Bauer Dec 11 '12 at 14:22