Proposition 6.3.5.6. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a morphism of simplicial sets which exhibits $\operatorname{\mathcal{D}}$ as a localization of $\operatorname{\mathcal{C}}$ with respect to a collection of edges $W$. Let $K$ be any simplicial set, and let $W_{K}$ denote the collection of edges $e = (e', e'')$ of the product $K \times \operatorname{\mathcal{C}}$ for which $e'$ is a degenerate edge of $K$ and $e''$ belongs to $W$. Then the induced map $F_{K}: K \times \operatorname{\mathcal{C}}\rightarrow K \times \operatorname{\mathcal{D}}$ exhibits $K \times \operatorname{\mathcal{D}}$ as the localization of $K \times \operatorname{\mathcal{C}}$ with respect to $W_{K}$.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Let $\operatorname{\mathcal{E}}$ be an $\infty $-category, and let
\[ \theta : \operatorname{Fun}( K \times \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}(K \times \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \]
be the functor given by precomposition with $F_ K$. We wish to show that $F_{K}$ is fully faithful, and that its essential image is the full subcategory $\operatorname{Fun}( (K \times \operatorname{\mathcal{C}})[W_{K}^{-1}], \operatorname{\mathcal{E}})$ of Notation 6.3.1.1. Unwinding the definitions, we can identify $\theta $ with the functor
\[ \theta ': \operatorname{Fun}( \operatorname{\mathcal{D}}, \operatorname{Fun}(K,\operatorname{\mathcal{E}}) ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{Fun}(K, \operatorname{\mathcal{E}})) \]
given by precomposition with $F$. Under this identification $\operatorname{Fun}( (K \times \operatorname{\mathcal{C}})[W_{K}^{-1}], \operatorname{\mathcal{E}})$ corresponds to the full subcategory $\operatorname{Fun}( \operatorname{\mathcal{C}}[W^{-1}], \operatorname{Fun}(K,\operatorname{\mathcal{E}}) ) \subseteq \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{Fun}(K,\operatorname{\mathcal{E}}) )$ (see Theorem 4.4.4.4), so that the desired result follows from our assumption on the functor $F$. $\square$