# Can we always make a strictly functorial choice of pullbacks/re-indexing?

$\newcommand{\C}{\mathbf{C}} \newcommand{\D}{\mathbf{D}}$ Let $\C$ be a category with pullbacks. Taking any choice of pullbacks gives us re-indexing functors $f^* \colon \C /Y \to \C/X$, and these will be functorial in $f$ up to natural isomorphism, in that $g^* \cdot f^* \cong (f \cdot g)^*$. However, these will usually not be strictly functorial in $f$; that is, $g^* \cdot f^*$ and $(f \cdot g)^*$ will not be literally equal. Strict functoriality also requires that $1_X^* = 1_{\C/X}$; while this typically does hold on the nose, it’s still not automatic.

My main question: Is there always some choice of pullbacks that make re-indexing strictly functorial? I believe the answer should be “no”, but I don’t know any counterexample. Even in the case of $\mathbf{Set}$, it’s not obvious whether there’s a choice that works.

An equivalent phrasing of the question is: can the codomain fibration $\mathrm{cod} \colon \C^\rightarrow \to \C$ be equipped with a splitting? It can always be replaced by an equivalent split fibration over $\C$; but splitting the codomain fibration itself seems hard.

-
Just a rough idea (haven't check if it works): Define an element of $X \times_S Y$ to be a finite diagram of sets which "refines" $X \rightarrow S \leftarrow Y$ together with compatible elements in all the sets. – Martin Brandenburg Oct 11 '13 at 23:09
You could rephrase this as asking whether any 2-functor C -> Cat is isomorphic to a strict 2-functor (that is, the components of the transformation are isos, not equivalences). This is already assuming enough Choice to get from a fibration to said 2-functor, and you may not want this. – David Roberts Oct 12 '13 at 0:04
I'd say this is an undesirable property. Replacing isomorphisms with equalities is unnatural. – Fernando Muro Oct 12 '13 at 0:16
@FernandoMuro Until you're doing type theory :-) – David Roberts Oct 12 '13 at 0:40
@MartinBrandenburg: I don’t follow exactly what you’re suggesting, but the trouble I’ve had with constructions along those lines is that they don’t give $1^* = 1$, and if you modify them by making a special case for identities, then you lose $g^*f^*=(fg)^*$ in the case where $fg = 1$. – Peter LeFanu Lumsdaine Oct 12 '13 at 17:15