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?



Why pullback only defined up-to-isomorphism but nevertheless presented as functor?
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).


