Proposition 4.4.1.7. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration between $\infty $-categories. Then $F$ is an isofibration of $\infty $-categories (in the sense of Definition 4.4.1.4) if and only if the induced functor of homotopy categories $f: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{\mathcal{D}}}$ is an isofibration of ordinary categories (in the sense of Definition 4.4.1.1).
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Assume first that $F$ is an isofibration and let $C \in \operatorname{\mathcal{C}}$ be an object, and let $[u]: D \rightarrow F(C)$ be an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{D}}}$, given by the homotopy class of some morphism $u: D \rightarrow F(C)$ in the $\infty $-category $\operatorname{\mathcal{D}}$. Then $u$ is an isomorphism, so our assumption that $F$ is an isofibration guarantees that we can lift $u$ to an isomorphism $\overline{u}: \overline{D} \rightarrow C$ in the $\infty $-category $\operatorname{\mathcal{C}}$. The homotopy class $[ \overline{u} ]$ is then an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ satisfying $f( [ \overline{u}] ) = [u]$. Allowing $C$ and $[u]$ to vary, we conclude that $f$ is an isofibration of ordinary categories.
Now suppose that $f$ is an isofibration, let $C \in \operatorname{\mathcal{C}}$ be an object, and let $u: D \rightarrow F(C)$ be an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}$. Then the homotopy class $[u]: D \rightarrow F(C)$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{D}}}$. Invoking our assumption that $f$ is an isofibration, we conclude that there exists an isomorphism $[v]: \overline{D} \rightarrow C$ in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ satisfying $f( [v] ) = [u]$. Then $[v]$ can be realized as the homotopy class of some morphism $v: \overline{D} \rightarrow C$ in the $\infty $-category $\operatorname{\mathcal{C}}$, which is automatically an isomorphism. The equation $f([v]) = [u]$ guarantees that there exists a homotopy from $F(v)$ to $u$ in the $\infty $-category $\operatorname{\mathcal{D}}$, given by a $2$-simplex $\sigma :$
\[ \xymatrix@R =50pt@C=50pt{ & F(C) \ar [dr]^{ \operatorname{id}_{ F(C) }} & \\ D \ar [ur]^{ F(v) } \ar [rr]^{ u } & & F(C). } \]
Since $F$ is an inner fibration, it is weakly right orthogonal to the inclusion $\Lambda ^{2}_{1} \hookrightarrow \Delta ^2$. We can therefore lift $\sigma $ to a $2$-simplex $\overline{\sigma }:$
\[ \xymatrix@R =50pt@C=50pt{ & C \ar [dr]^{ \operatorname{id}_{C }} & \\ \overline{D} \ar [ur]^{ v } \ar [rr]^{ \overline{u} } & & C. } \]
in the $\infty $-category $\operatorname{\mathcal{C}}$. Since $v$ and $\operatorname{id}_{C}$ are isomorphisms, it follows that $\overline{u}$ is an isomorphism (Remark 1.4.6.3). Allowing $C$ and $u$ to vary, we conclude that $F$ is an isofibration of $\infty $-categories. $\square$