Kerodon

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

Proposition 5.1.4.8. Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a cartesian fibration of $\infty$-categories. Then $q$ is an isofibration.

Proof. Suppose we are given an object $Y \in \operatorname{\mathcal{C}}$ and an isomorphism $\overline{e}: \overline{X} \rightarrow q(Y)$ in the $\infty$-category $\operatorname{\mathcal{D}}$. We wish to show that there exists an isomorphism $e: X \rightarrow Y$ in the $\infty$-category $\operatorname{\mathcal{C}}$ satisfying $q(e) = \overline{e}$. Our assumption that $q$ is a cartesian fibration guarantees that we can write $\overline{e} = q(e)$, where $e: X \rightarrow Y$ is a $q$-cartesian morphism of $\operatorname{\mathcal{C}}$. Since $\overline{e} = q(e)$ is an isomorphism, Proposition 5.1.1.8 guarantees that $e$ is an isomorphism. $\square$