The Stacks project

Proof. Suppose that $\varphi : x' \to x$ is strongly cartesian with respect to $p$. We claim that $\varphi$ is strongly cartesian with respect to $p'$ also. Set $g = p'(\varphi )$, so that $g : V'/U \to V/U$ for some morphisms $f : V \to U$ and $f' : V' \to U$. Let $z \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{S})$. Set $p'(z) = (W \to U)$. To show that $\varphi$ is strongly cartesian for $p'$ we have to show

given by $\psi ' \longmapsto (\varphi \circ \psi ', p'(\psi '))$ is bijective. Suppose given an element $(\psi , h)$ of the right hand side, then in particular $g \circ h = p(\psi )$, and by the condition that $\varphi$ is strongly cartesian we get a unique morphism $\psi ' : z \to x'$ with $\psi = \varphi \circ \psi '$ and $p(\psi ') = h$. OK, and now $p'(\psi ') : W/U \to V/U$ is a morphism whose corresponding map $W \to V$ is $h$, hence equal to $h$ as a morphism in $\mathcal{C}/U$. Thus $\psi '$ is a unique morphism $z \to x'$ which maps to the given pair $(\psi , h)$. This proves the claim.

Finally, suppose given $g : V'/U \to V/U$ and $x$ with $p'(x) = V/U$. Since $p : \mathcal{S} \to \mathcal{C}$ is a fibred category we see there exists a strongly cartesian morphism $\varphi : x' \to x$ with $p(\varphi ) = g$. By the same argument as above it follows that $p'(\varphi ) = g : V'/U \to V/U$. And as seen above the morphism $\varphi$ is strongly cartesian. Thus the conditions of Definition 4.33.5 are satisfied and we win. $\square$