Lemma 4.33.13. Let $p : \mathcal{S} \to \mathcal{C}$ be a fibred category. Let $x \to y$ and $z \to y$ be morphisms of $\mathcal{S}$ with $x \to y$ strongly cartesian. If $p(x) \times _{p(y)} p(z)$ exists, then $x \times _ y z$ exists, $p(x \times _ y z) = p(x) \times _{p(y)} p(z)$, and $x \times _ y z \to z$ is strongly cartesian.
Proof. Pick a strongly cartesian morphism $\text{pr}_2^*z \to z$ lying over $\text{pr}_2 : p(x) \times _{p(y)} p(z) \to p(z)$. Then $\text{pr}_2^*z = x \times _ y z$ by Lemma 4.33.4. $\square$
Comments (0)