The Stacks project

Proof. Note that the construction makes sense since by Lemma 4.33.2 the identity morphism of any object of $\mathcal{S}$ is strongly cartesian, and the composition of strongly cartesian morphisms is strongly cartesian. The first lifting property of Definition 4.35.1 follows from the condition that in a fibred category given any morphism $f : V \to U$ and $x$ lying over $U$ there exists a strongly cartesian morphism $\varphi : y \to x$ lying over $f$. Let us check the second lifting property of Definition 4.35.1 for the category $p' : \mathcal{S}' \to \mathcal{C}$ over $\mathcal{C}$. To do this we argue as in the discussion following Definition 4.35.1. Thus in Diagram 4.35.1.1 the morphisms $\phi$, $\psi$ and $\gamma$ are strongly cartesian morphisms of $\mathcal{S}$. Hence $\gamma$ and $\phi \circ \psi$ are strongly cartesian morphisms of $\mathcal{S}$ lying over the same arrow of $\mathcal{C}$ and having the same target in $\mathcal{S}$. By the discussion following Definition 4.33.1 this means these two arrows are isomorphic as desired (here we use also that any isomorphism in $\mathcal{S}$ is strongly cartesian, by Lemma 4.33.2 again). $\square$