# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Remark 5.1.5.8. In the situation of Proposition 5.1.5.7, we can replace $(2)$ with the following a priori weaker assumption:

$(2')$

For every object $Z \in \operatorname{\mathcal{C}}$ and every morphism $\overline{u}: \overline{Y} \rightarrow q(Z)$ in $\operatorname{\mathcal{D}}$, there exists a $q$-cartesian $u: Y \rightarrow Z$ of $\operatorname{\mathcal{C}}$ satisfying $q(u) = \overline{u}$ and for which $F(u)$ is locally $q'$-cartesian.

Assume that $(2)$ is satisfied and let $v: X \rightarrow Z$ be any $q$-cartesian morphism in $\operatorname{\mathcal{C}}$; we wish to show that $F(v)$ is locally $q'$-cartesian. To prove this, we can assume without loss of generality that $\operatorname{\mathcal{D}}= \Delta ^1 = \operatorname{\mathcal{D}}'$ and that $\overline{F}$ is the identity map. Using $(2')$, we can choose another $q$-cartesian morphism $u: Y \rightarrow Z$ satisfying $q(u) = q(v)$ for which $F(u)$ is $q'$-cartesian. Applying Remark 5.1.3.8, we see that $v$ can be obtained as a composition of $u$ with an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}$. Then $F(v)$ can be obtained as the composition of $F(u)$ with an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}'$, and is therefore $q$-cartesian by virtue of Corollary 5.1.2.4 (and Proposition 5.1.1.8).