Kerodon

Proof. We first prove $(1)$. Assume that $U$ and $V$ are inner fibration and that $F$ is an equivalence of inner fibrations over $\operatorname{\mathcal{E}}$. We wish to show that $F$ is a categorical equivalence of simplicial sets. Fix an $\infty $-category $\operatorname{\mathcal{K}}$, and let $\theta _{F}: \pi _0( \operatorname{Fun}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{K}})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{K}})^{\simeq } )$ be the map given by precomposition with $F$. We wish to show that $\theta _{F}$ is a bijection. Let $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a homotopy inverse of $F$ relative to $\operatorname{\mathcal{E}}$, so that precomposition with $G$ determines a map $\theta _{G}: \pi _0( \operatorname{Fun}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{K}})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{K}})^{\simeq } )$. We claim that $\theta _{G}$ is an inverse of $\theta _{F}$. We will show that $\theta _{G}$ is a left inverse of $\theta _{F}$; a similar argument will show that $\theta _{G}$ is a right inverse of $\theta _{F}$. Fix a morphism $H: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{K}}$; we wish to show that $H$ is isomorphic to $H \circ G \circ F$ as an object of the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{K}})$. This is clear, since postcomposition with $H$ determines a functor of $\infty $-categories $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{K}})$.

We now prove $(2)$. Let $Q$ be a contractible Kan complex containing a pair of distinct vertices $x$ and $y$, and form a pushout diagram of simplicial sets

Since the vertical maps are monomorphisms, this diagram is also a categorical pushout square (Proposition 4.5.4.11). In particular, if $F$ is a categorical equivalence, then the map $Q \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{M}}$ is also a categorical equivalence (Proposition 4.5.4.10). Since $Q$ is contractible, the inclusion $\{ y\} \times \operatorname{\mathcal{C}}\hookrightarrow Q \times \operatorname{\mathcal{C}}$ is a categorical equivalence (Remark 4.5.3.7), so the inclusion $\{ y\} \times \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{M}}$ is also a categorical equivalence. If $U$ is an isofibration, then the lifting problem

admits a solution, which we can identify with a pair of morphisms $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ and $u: Q \rightarrow \operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$ satisfying $u(x) = G \circ F$ and $u(y) = \operatorname{id}_{\operatorname{\mathcal{C}}}$. It follows that $G \circ F$ is isomorphic to $\operatorname{id}_{\operatorname{\mathcal{C}}}$ as an object of the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}},\operatorname{\mathcal{C}})$.

Repeating the above argument with $F$ replaced by $G$, we conclude that there exists a morphism $H: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ in $(\operatorname{Set_{\Delta }})_{/S}$ such that $H \circ G$ is isomorphic to $\operatorname{id}_{\operatorname{\mathcal{D}}}$ as an object of the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{D}},\operatorname{\mathcal{D}})$. Then $F$ and $H$ are both isomorphic to $H \circ G \circ F$ as objects of the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$, and are therefore isomorphic to each other. We may therefore assume without loss of generality that $H = F$, so that $G$ is a homotopy inverse of $F$ relative to $\operatorname{\mathcal{E}}$. In particular, $F$ is an equivalence of inner fibrations over $\operatorname{\mathcal{E}}$. $\square$