Kerodon

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

Remark 4.5.9.12. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be an inner fibration of $\infty $-categories. If $U$ is exponentiable, then it is is an isofibration. To prove this, fix an object $Y \in \operatorname{\mathcal{C}}$ having image $\overline{Y} = U(Y)$ and an isomorphism $\overline{e}: \overline{X} \rightarrow \overline{Y}$ in the $\infty $-category $\operatorname{\mathcal{B}}$; we wish to show that $\overline{e}$ can be lifted to an isomorphism $e: X \rightarrow Y$ in the $\infty $-category $\operatorname{\mathcal{C}}$. Using Corollary 4.4.3.14, we can reduce to the case where $\operatorname{\mathcal{B}}$ is a contractible Kan complex, so that the inclusion map $\{ \overline{X} \} \hookrightarrow \operatorname{\mathcal{B}}$ is an equivalence of $\infty $-categories. Our assumption that $U$ is exponentiable then guarantees that the inclusion map $\{ \overline{X} \} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}$ is also an equivalence of $\infty $-categories. In particular, there exists an object $X \in \operatorname{\mathcal{C}}$ which is isomorphic to $Y$ such that $U(X) = \overline{X}$. Choose an isomorphism $e': X \rightarrow Y$ in $\operatorname{\mathcal{E}}$, and set $\overline{e}' = U(e')$. Our assumption that $\operatorname{\mathcal{B}}$ is a contractible Kan complex then guarantees that we can choose a $2$-simplex $\overline{\sigma }$ of $\operatorname{\mathcal{B}}$ with boundary indicated in the diagram

\[ \xymatrix { & \overline{X} \ar [dr]^{ \overline{e}' } & \\ \overline{X} \ar [ur]^{ \operatorname{id}} \ar [rr]^{ \overline{e} } & & \overline{Y}. } \]

Since $U$ is an inner fibration, we can lift $\sigma $ to a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ with boundary indicated in the diagram

\[ \xymatrix { & X \ar [dr]^{e'} & \\ X \ar [ur]^{ \operatorname{id}} \ar@ {-->}[rr] & & Y. } \]

It follows that $e = d^{2}_{1}(\sigma )$ is an isomorphism from $X$ to $Y$ in the $\infty $-category $\operatorname{\mathcal{C}}$ satisfying $U(e) = \overline{e}$.