Corollary 8.2.2.10. Let $\lambda = (\lambda _{-}, \lambda _{+}): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ and $\mu = (\mu _{-}, \mu _{+}): \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{D}}_{+}$ be couplings of $\infty $-categories. Fix a functor $F_{+}: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{D}}_{+}$. If $\lambda $ is corepresentable, then the forgetful functor
\[ \operatorname{Fun}_{ \pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} )} \{ F_{+} \} \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \]
is fully faithful, and its essential image is the full subcategory $\operatorname{Fun}^{0}_{ / \operatorname{\mathcal{D}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \subseteq \operatorname{Fun}_{ / \operatorname{\mathcal{D}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ spanned by those functors which carry $\lambda _{+}$-cocartesian morphisms of $\operatorname{\mathcal{C}}$ to $\mu _{+}$-cocartesian morphisms of $\operatorname{\mathcal{D}}$.
Proof.
Let $\operatorname{\mathcal{E}}_{-} \subseteq \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ be the full subcategory defined in Proposition 8.2.2.9. We then have a commutative diagram of $\infty $-categories
8.32
\begin{equation} \begin{gathered}\label{equation:collapse-left-universal2} \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} ) } \{ F_{+} \} \ar [r] \ar [d] & \operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [d] \\ \operatorname{Fun}^{0}_{ / \operatorname{\mathcal{D}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [r] \ar [d] & \operatorname{\mathcal{E}}_{-} \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{+} ) } \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} ) \ar [d] \\ \{ F_{+} \} \ar [r] & \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} ), } \end{gathered} \end{equation}
where both squares are pullback diagrams. Note that the vertical map on the lower right is a pullback of the functor $\operatorname{\mathcal{E}}_{-} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{+} )$ obtained by restricting the cocartesian fibration $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \xrightarrow {\mu _{+} \circ } \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}_{+})$ (see Proposition 8.2.1.7 and Theorem 5.2.1.1) to the replete subcategory $\operatorname{\mathcal{E}}_{-} \subseteq \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$, and is therefore an isofibration. Moreover, the right vertical composition $\operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} )$ is a cocartesian fibration (see Proposition 8.2.1.7 and Remark 8.2.2.3), and therefore an isofibration. It follows that the bottom square and outer rectangle of (8.32) are categorical pullback diagrams (Corollary 4.5.2.27), so that the upper square is also a categorical pullback diagram (Proposition 4.5.2.18). Our assumption that $\lambda $ is corepresentable guarantees that for each object $X_{-} \in \operatorname{\mathcal{C}}_{-}$, the fiber $\{ X_{-} \} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{C}}$ has an initial object, and is therefore weakly contractible. Applying Proposition 8.2.2.9, we deduce that the vertical map on the upper right is an equivalence of $\infty $-categories. Invoking Proposition 4.5.2.21, we conclude that the forgetful functor $\operatorname{Fun}_{ \pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} )} \{ F_{+} \} \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}_{+}}^{0}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ is also an equivalence of $\infty $-categories.
$\square$