**Proof.**
Proof of (1). Let $\varphi : y \to x$ and $\psi : z \to y$ be strongly cartesian. Let $t$ be an arbitrary object of $\mathcal{S}$. Then we have

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

hence $z \to x$ is strongly cartesian.

Proof of (2). Let $y \to x$ be an isomorphism. Then $p(y) \to p(x)$ is an isomorphism too. Hence $\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(y)) \to \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(x))$ is a bijection. Hence $\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(z, x) \times _{\mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(x))} \mathop{\mathrm{Mor}}\nolimits _\mathcal {C}(p(z), p(y))$ is bijective to $\mathop{\mathrm{Mor}}\nolimits _\mathcal {S}(z, x)$. Hence the displayed map of Definition 4.33.1 is a bijection as $y \to x$ is an isomorphism, and we conclude that $y \to x$ is strongly cartesian.

Proof of (3). Assume $\varphi : y \to x$ is strongly cartesian with $p(\varphi ) : p(y) \to p(x)$ an isomorphism. Applying the definition with $z = x$ shows that $(\text{id}_ x, p(\varphi )^{-1})$ comes from a unique morphism $\chi : x \to y$. We omit the verification that $\chi $ is the inverse of $\varphi $.
$\square$

## Comments (0)