The Stacks project

Proof. Basically what one has to show here is that given $F : \mathcal{X} \to \mathcal{S}$ and $G : \mathcal{Y} \to \mathcal{S}$ morphisms of fibred categories over $\mathcal{C}$, then the category $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$ described in Lemma 4.32.3 is fibred. Let us show that $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$ has plenty of strongly cartesian morphisms. Namely, suppose we have $(U, x, y, \phi )$ an object of $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$. And suppose $f : V \to U$ is a morphism in $\mathcal{C}$. Choose strongly cartesian morphisms $a : f^*x \to x$ in $\mathcal{X}$ lying over $f$ and $b : f^*y \to y$ in $\mathcal{Y}$ lying over $f$. By assumption $F(a)$ and $G(b)$ are strongly cartesian. Since $\phi : F(x) \to G(y)$ is an isomorphism, by the uniqueness of strongly cartesian morphisms we find a unique isomorphism $f^*\phi : F(f^*x) \to G(f^*y)$ such that $G(b) \circ f^*\phi = \phi \circ F(a)$. In other words $(G(a), G(b)) : (V, f^*x, f^*y, f^*\phi ) \to (U, x, y, \phi )$ is a morphism in $\mathcal{X} \times _\mathcal {S} \mathcal{Y}$. We omit the verification that this is a strongly cartesian morphism (and that these are in fact the only strongly cartesian morphisms). $\square$