Corollary 5.1.6.2. Suppose we are given a commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{F} \ar [d]^-{U} & \operatorname{\mathcal{C}}' \ar [d]^-{U'} \\ \operatorname{\mathcal{D}}\ar [r]^-{ \overline{F} } & \operatorname{\mathcal{D}}'. } \]
Assume that $U$ and $U'$ are isofibrations of $\infty $-categories and that $F$ and $\overline{F}$ are equivalences of $\infty $-categories. Then:
Proof.
We will prove the first assertion; the second follows by a similar argument. It follows from Theorem 5.1.6.1 that if $U$ is a cartesian fibration, then $U'$ is also a cartesian fibration. To prove the converse, choose functors $G': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$ and $\overline{G}: \operatorname{\mathcal{D}}' \rightarrow \operatorname{\mathcal{D}}$ which are homotopy inverse to the equivalences $F$ and $\overline{F}$, respectively. We then have isomorphisms
\[ U \circ G' \circ F \simeq U \simeq \overline{G} \circ \overline{F} \circ U = \overline{G} \circ U' \circ F \]
in the functor $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. Since $F$ is an equivalence of $\infty $-categories, it follows that there exists an isomorphism $\overline{\alpha }: U \circ G' \rightarrow \overline{G} \circ U'$ in the functor $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}', \operatorname{\mathcal{D}})$. Using our assumption that $U$ is an isofibration, we can lift $\overline{\alpha }$ to an isomorphism of functors $\alpha : G' \rightarrow G$ (Proposition 4.4.5.8). Applying Theorem 5.1.6.1 to the commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}' \ar [r]^-{G} \ar [d]^-{U'} & \operatorname{\mathcal{C}}\ar [d]^-{U} \\ \operatorname{\mathcal{D}}' \ar [r]^-{\overline{G}} & \operatorname{\mathcal{D}}, } \]
we conclude that if $U'$ is a cartesian fibration, then $U$ is also a cartesian fibration.
$\square$