
Lemma 4.32.7. Assume $p : \mathcal{S} \to \mathcal{C}$ is a fibred category. Assume given a choice of pullbacks for $p : \mathcal{S} \to \mathcal{C}$.

1. For any pair of composable morphisms $f : V \to U$, $g : W \to V$ there is a unique isomorphism

$\alpha _{g, f} : (f \circ g)^\ast \longrightarrow g^\ast \circ f^\ast$

as functors $\mathcal{S}_ U \to \mathcal{S}_ W$ such that for every $y\in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S}_ U)$ the following diagram commutes

$\xymatrix{ g^\ast f^\ast y \ar[r] & f^\ast y \ar[d] \\ (f \circ g)^\ast y \ar[r] \ar[u]^{(\alpha _{g, f})_ y} & y }$
2. If $f = \text{id}_ U$, then there is a canonical isomorphism $\alpha _ U : \text{id} \to (\text{id}_ U)^*$ as functors $\mathcal{S}_ U \to \mathcal{S}_ U$.

3. The quadruple $(U \mapsto \mathcal{S}_ U, f \mapsto f^*, \alpha _{g, f}, \alpha _ U)$ defines a pseudo functor from $\mathcal{C}^{opp}$ to the $(2, 1)$-category of categories, see Definition 4.28.5.

Proof. In fact, it is clear that the commutative diagram of part (1) uniquely determines the morphism $(\alpha _{g, f})_ y$ in the fibre category $\mathcal{S}_ W$. It is an isomorphism since both the morphism $(f \circ g)^*y \to y$ and the composition $g^*f^*y \to f^*y \to y$ are strongly cartesian morphisms lifting $f \circ g$ (see discussion following Definition 4.32.1 and Lemma 4.32.2). In the same way, since $\text{id}_ x : x \to x$ is clearly strongly cartesian over $\text{id}_ U$ (with $U = p(x)$) we see that there exists an isomorphism $(\alpha _ U)_ x : x \to (\text{id}_ U)^*x$. (Of course we could have assumed beforehand that $f^*x = x$ whenever $f$ is an identity morphism, but it is better for the sake of generality not to assume this.) We omit the verification that $\alpha _{g, f}$ and $\alpha _ U$ so obtained are transformations of functors. We also omit the verification of (3). $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).