Kerodon

Proof. Let $\operatorname{\mathcal{D}}$ be an $\infty $-category, so that precomposition with $F$ induces a functor $F^{\ast }: \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$. We wish to show that the functor $F^{\ast }$ is fully faithful, and that its essential image is the full subcategory $\operatorname{Fun}( \operatorname{\mathcal{E}}[W^{-1}], \operatorname{\mathcal{D}}) \subseteq \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$. Let $\operatorname{\mathcal{B}}= \operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ and $\operatorname{\mathcal{B}}' = \operatorname{Fun}(\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ be the relative exponentials of Construction 4.5.9.1, and let $\pi : \operatorname{\mathcal{B}}\rightarrow \operatorname{\mathcal{C}}$ and $\pi ': \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{C}}$ denote the projection maps. Combining assumption $(1)$ with Corollary 5.3.6.8, we see that $\pi $ and $\pi '$ are cartesian fibrations.

For each vertex $C \in \operatorname{\mathcal{C}}$, let us identify the fibers $\operatorname{\mathcal{B}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}$ and $\operatorname{\mathcal{B}}'_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}'$ with the $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{D}})$ and $\operatorname{Fun}( \operatorname{\mathcal{E}}'_{C}, \operatorname{\mathcal{D}})$, respectively. Precomposition with $F$ induces a morphism of simplicial sets $G: \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{B}}$ satisfying $\pi \circ G = \pi '$, given on each fiber by the functor

Combining assumption $(2)$ with Corollary 5.3.6.8, we see that $G$ carries $\pi '$-cartesian edges of $\operatorname{\mathcal{B}}'$ to $\pi $-cartesian edges of $\operatorname{\mathcal{B}}$. In particular, for every edge $e: X \rightarrow Y$ of $\operatorname{\mathcal{C}}$, the diagram of $\infty $-categories

commutes up to isomorphism, where the horizontal functors are given by contravariant transport along $e$ (see Remark 5.2.8.5).

Let us identify the vertices of $\operatorname{\mathcal{B}}$ with pairs $(C, \rho )$, where $C$ is a vertex of $\operatorname{\mathcal{C}}$ and $\rho : \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{D}}$ is a functor of $\infty $-categories. Let $\operatorname{\mathcal{B}}^{0} \subseteq \operatorname{\mathcal{B}}$ denote the full simplicial subset spanned by those vertices $(C,\rho )$ for which the functor $\rho $ carries each edge of $W_{C}$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}$. It follows from assumption $(3)$ that for every vertex $C$, the functor $G_{C}: \operatorname{\mathcal{B}}'_{C} \rightarrow \operatorname{\mathcal{B}}_{C}$ is fully faithful, and its essential image can be identified with the full subcategory $\operatorname{\mathcal{B}}^{0}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}^{0} \subseteq \operatorname{\mathcal{B}}_{C}$. Combining this observation with the homotopy commutativity of the diagram (6.13), we see that for every edge $e: X \rightarrow Y$ in $\operatorname{\mathcal{E}}$, the contravariant transport functor $e^{\ast }: \operatorname{\mathcal{B}}_{Y} \rightarrow \operatorname{\mathcal{B}}_{X}$ carries $\operatorname{\mathcal{B}}^{0}_{Y}$ into $\operatorname{\mathcal{B}}^{0}_{X}$. It follows that $\pi $ restricts to a cartesian fibration of simplicial sets $\pi ^{0}: \operatorname{\mathcal{B}}^{0} \rightarrow \operatorname{\mathcal{C}}$, and that an edge of $\operatorname{\mathcal{B}}^{0}$ is $\pi ^{0}$-cartesian if and only if it is $\pi $-cartesian when viewed as an edge of $\operatorname{\mathcal{B}}$ (Proposition 5.1.4.17). In particular, the morphism $G: \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{B}}^{0} \subseteq \operatorname{\mathcal{B}}$ carries $\pi '$-cartesian edges of $\operatorname{\mathcal{B}}'$ to $\pi ^{0}$-cartesian edges of $\operatorname{\mathcal{B}}^{0}$, and therefore induces an equivalence $\operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{B}}^{0}$ of cartesian fibrations over $\operatorname{\mathcal{C}}$ (Proposition 5.1.7.15). We complete the proof by observing that $F^{\ast }: \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{E}}[W^{-1}], \operatorname{\mathcal{D}})$ can be identified with the functor

given by precomposition with $G$, and is therefore an equivalence of $\infty $-categories. $\square$