Kerodon

Remark 11.5.0.114. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of categories. Then $U$ is an isofibration (Definition 4.4.1.1). If $Y$ is an object of $\operatorname{\mathcal{C}}$ and $\overline{f}: \overline{X} \rightarrow U(Y)$ is an isomorphism in the category $\operatorname{\mathcal{C}}$, then our assumption that $U$ is a cartesian fibration guarantees that we can choose a $U$-cartesian morphism $f: X \rightarrow Y$ of $\operatorname{\mathcal{E}}$ satisfying $U(f) = \overline{f}$, and the morphism $f$ is automatically an isomorphism (Example 11.5.0.108).