Kerodon

Proof. Let $C$ be an object of $\operatorname{\mathcal{C}}'$, so that $\eta _{C}: C \rightarrow (G \circ F)(C)$ is an isomorphism. Since $\eta $ and $\epsilon $ are compatible up to homotopy, the identity morphism $\operatorname{id}_{ F(C) }$ is a composition of $F(\eta _ C): F(C) \rightarrow (F \circ G \circ F)(C)$ with $\epsilon _{F(C)}: (F \circ G \circ F)(C) \rightarrow F(C)$ in the $\infty $-category $\operatorname{\mathcal{D}}$. It follows that $\epsilon _{F(C)}$ is an isomorphism in $\operatorname{\mathcal{D}}$ (Remark 1.4.6.3), so that $F(C)$ belongs to the full subcategory $\operatorname{\mathcal{D}}' \subseteq \operatorname{\mathcal{D}}$. Setting $F' = F|_{\operatorname{\mathcal{C}}'}$, we obtain a functor $F': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}'$. A similar argument shows that we can regard $G' = G|_{\operatorname{\mathcal{D}}'}$ as a functor from $\operatorname{\mathcal{D}}'$ to $\operatorname{\mathcal{C}}'$. The unit morphism $\eta $ restricts to a natural transformation of functors $\eta ': \operatorname{id}_{\operatorname{\mathcal{C}}'} \rightarrow G' \circ F'$. By construction, $\eta '$ carries each object $C \in \operatorname{\mathcal{C}}'$ to an isomorphism, and is therefore an isomorphism in the functor $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{C}}' )$ (Theorem 4.4.4.4). Similarly, the counit $\epsilon $ restricts to a natural isomorphism $\epsilon ': F' \circ G' \rightarrow \operatorname{id}_{\operatorname{\mathcal{D}}'}$, so that $F'$ and $G'$ are homotopy inverse to one another. $\square$