Lemma 4.33.4. Let $\mathcal{C}$ be a category. Let $p : \mathcal{S} \to \mathcal{C}$ be a category over $\mathcal{C}$. Let $x \to y$ and $z \to y$ be morphisms of $\mathcal{S}$. Assume

1. $x \to y$ is strongly cartesian,

2. $p(x) \times _{p(y)} p(z)$ exists, and

3. there exists a strongly cartesian morphism $a : w \to z$ in $\mathcal{S}$ with $p(w) = p(x) \times _{p(y)} p(z)$ and $p(a) = \text{pr}_2 : p(x) \times _{p(y)} p(z) \to p(z)$.

Then the fibre product $x \times _ y z$ exists and is isomorphic to $w$.

Proof. Since $x \to y$ is strongly cartesian there exists a unique morphism $b : w \to x$ such that $p(b) = \text{pr}_1$. To see that $w$ is the fibre product we compute

\begin{align*} & \mathop{Mor}\nolimits _\mathcal {S}(t, w) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(w)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z))} (\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x)) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(z))) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {S}(t, y)} \mathop{Mor}\nolimits _\mathcal {S}(t, y) \times _{\mathop{Mor}\nolimits _\mathcal {C}(p(t), p(y))} \mathop{Mor}\nolimits _\mathcal {C}(p(t), p(x)) \\ & = \mathop{Mor}\nolimits _\mathcal {S}(t, z) \times _{\mathop{Mor}\nolimits _\mathcal {S}(t, y)} \mathop{Mor}\nolimits _\mathcal {S}(t, x) \end{align*}

as desired. The first equality holds because $a : w \to z$ is strongly cartesian and the last equality holds because $x \to y$ is strongly cartesian. $\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).