Why pullback only defined up-to-isomorphism but nevertheless presented as functor? 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?
 A: Let us first consider a slightly simpler situation. The cartesian product of sets $A$ and $B$ is a set $C$ with two maps $p_1 : C \to A$ and $p_2 : C \to B$ such that ... (familiar condition inserted here). All cartesian products of $A$ and $B$ are canonically isomorphic, and among them there is a particular one, denoted $A \times B$, which is specifically defined as $A \times B = \lbrace\lbrace\lbrace x,y \rbrace, \lbrace y\rbrace\rbrace \mid x \in A \land y \in B\rbrace$.
This is a familiar situation. Often a construction is determined up to canonical isomorphism, but we have a specific one that we can use as an operation, like $(A,B) \mapsto A \times B$ above.
Awodey does the same thing in his book. "Being a pullback" is a property, but we can turn it into structure, i.e., an operation which takes a pair of arrows $f : A \to C$ and $g : B \to C$ and gives a pullback square. You may wonder whether there always is such an operation. If you believe in the axiom of choice then the answer is positive, because we may always choose particular pullbacks among the canonically isomorphic ones. In concrete examples you will usually find chosen pullbacks easily, so this is not problematic.
There is a small catch. While for $h : A \to B$ it is the case that $h^{*}$ is a functor from $\mathcal{C}/B$ to $\mathcal{C}/A$, the assignment $h \mapsto h^\ast$ tends to be a "functor up to isomorphism" only. This is so because composition of chosen pullbacks need not be a chosen pullback (but is canonically isomprhic to it).
A: Actually, it looks to me that there's a conflation of two different issues. According to the boxed statement in the OP, we just have to exhibit a functor $h^\ast: \mathbf{C}/C \to \mathbf{C}/C'$ for a fixed morphism $h: C' \to C$. We are not being asked to prove that we can choose a strict functor (as opposed to a pseudofunctor) 
$$\mathbf{C}^{op} \to Cat$$ 
which takes each object $C$ to the slice $\mathbf{C}/C$, and morphisms $h$ to pullback functors, which appears to be the issue Andrej is discussing. 
The issue being discussed in the boxed statement is easy, and can be boiled down to this: if $\mathbf{C}$ has pullbacks, then for each $h: C' \to C$ the pushforward functor $\sum_h: \mathbf{C}/C' \to \mathbf{C}/C$ (taking each object $f: X \to C'$ in the domain to the object $h \circ f: X \to C$ in the codomain, and defined in the obvious way on morphisms) has a right adjoint (which is of course a functor) $h^\ast$. Here we need only choose a pullback object $h^\ast g$ in $\mathbf{C}/C'$ for each object $g: Y \to C$ in $\mathbf{C}/C$, and then define $h^\ast$ on morphisms in the way dictated by the universal property. In other words, any choice of pullback $h^\ast g$, one for each object $g$ in $\mathbf{C}/C$, defines a universal arrow 
$$\Phi_g: \sum_h (h^\ast g) \to g$$ 
so that having made these choices and given a morphism $f: g \to g'$ in $\mathbf{C}/C$ (i.e., a commutative triangle), we may then define $h^\ast f: h^\ast g \to h^\ast g'$ to be the unique arrow such that 
$$\Phi_{g'} \circ \sum_h (h^\ast f) = f \circ \Phi_g$$ 
and functoriality of $h^\ast$ is assured by the usual universal arguments. 
Edit: For example, let us show $h^\ast$ preserves compositions. Suppose given morphisms $f: g \to g'$ and $f': g' \to g''$ in $\mathbf{C}/C$. Then $h^\ast (f' \circ f)$ is the unique arrow $h^\ast g \to h^\ast g''$ such that 
$$\Phi_{g''} \circ \sum_h h^\ast(f' \circ f) = f' \circ f \circ \Phi_g.$$ 
On the other hand, 
$$
\Phi_{g''} \circ \sum_h (h^\ast f' \circ h^\ast f) = \Phi_{g''} \circ (\sum_h h^\ast f') \circ (\sum_h h^\ast f)
 = f' \circ \Phi_{g'} \circ (\sum_h h^\ast f) 
 = f' \circ f \circ \Phi_g
$$
and so, by uniqueness, $h^\ast (f' \circ f) = (h^\ast f') \circ (h^\ast f)$. 
A: Why has no one mentioned anafunctors? They were invented by Makkai for the express purpose of expressing universal constructions as functor-like things (I was going to say 'objects') without having to make choices. 
The definition is as follows: Let $C$ and $D$ be categories. An anafunctor from $C$ to $D$ is a span $C\leftarrow U \to D$ where $U \to C$ is fully faithful and surjective on objects.
That's it.
Of course, it is a bit more tricky to show that there are the arrows of a (weak) 2-category of categories, and that category theory works perfectly well using this notion of categories; for the present purposes, the references at the above link should satisfy the most curious.
In the case of the pullback 'functor' $h^*$ we have an anafunctor
$\mathbf{C}/C \leftarrow P \to \mathbf{C}/C'$ where $P$ is the category with objects pullback squares with bottom arrow $h$ and morphisms the canonical thing which makes $P \to \mathbf{C}/C$ fully faithful: commutative triangles involving the other leg of the cospan involving $h$ - in other words, arrows in $\mathbf{C}/C$. This induces a canonical arrow in $\mathbf{C}/C'$ by the universal property of pullbacks, and then the functor $P\to \mathbf{C}/C'$ just forgets the original pullback square, and keeps the arrow with codomain $C'$. This is a functor by using the universal property of pullbacks a couple of times.
If one has a way of choosing a particular pullback square for each object of $\mathbf{C}/C$, say by some sort of canonical construction as in the category of (ZF-)sets (Kuratowski pairs and subsets), or by judicious amounts of the axiom of choice, then one can find a section on objects of $P \to \mathbf{C}/C$, and this gives you a canonical section of the functor $P \to \mathbf{C}/C$, which then gives a pullback functor $h^*\colon \mathbf{C}/C \to \mathbf{C}/C'$.
A similar sort of anafunctor exists for any universal construction, which is defined up to isomorphism by some universal property.
