Proof.
Using Proposition 8.2.4.3, we can choose a commutative diagram
8.52
\begin{equation} \begin{gathered}\label{equation:coupling-fully-faithful} \xymatrix@R =50pt@C=50pt{ \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \ar [r]^-{ \widetilde{G}'} \ar [d] & \operatorname{\mathcal{C}}\ar [r]^-{ \widetilde{G} } \ar [d]^{\lambda } & \operatorname{Tw}( \operatorname{\mathcal{C}}_{-} ) \ar [d] \\ \operatorname{\mathcal{C}}_{+}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ G^{\operatorname{op}} \times \operatorname{id}} & \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} \ar [r]^-{ \operatorname{id}\times G } & \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{-}, } \end{gathered} \end{equation}
where the left square exhibits $\lambda $ as represented by $G$ in the sense of Definition 8.2.4.1, and the right square exhibits $\lambda $ as represented by $G$ in the sense of Definition 8.2.3.5. Invoking (the dual of) Lemma 8.2.3.6, we see that $(1)$ is equivalent to the following:
- $(1')$
The left square of (8.52) is a categorical pullback diagram.
For each object $C \in \operatorname{\mathcal{C}}_{+}$, Proposition 8.2.3.7 guarantees that the composite functor $\widetilde{G} \circ \widetilde{G}'$ carries $\operatorname{id}_{C}$ to an isomorphism of $\operatorname{\mathcal{C}}_{-}$ (regarded as an object of $\operatorname{Tw}(\operatorname{\mathcal{C}}_{-} )$). It follows from Theorem 8.2.2.11 that $(G, \widetilde{G}' \circ \widetilde{G}, G)$ and $(G, \operatorname{Tw}(G), G)$ are isomorphic when viewed as objects of $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}))$ (since both are initial objects of the $\infty $-category $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-})) \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{C}}_{-})} \{ G\} $). In particular, for every pair of objects $X,Y \in \operatorname{\mathcal{C}}_{+}$, the diagram of Kan complexes
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}_{+}}(X,Y) \ar [d]^{G} \ar [r] & \{ X\} \times _{ \operatorname{\mathcal{C}}_{+}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \times _{\operatorname{\mathcal{C}}_{+}} \{ Y\} \ar [d]^{ \widetilde{G}' \circ \widetilde{G} } \ar [d] \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}_{-}}( G(X), G(Y) ) \ar [r] & \{ G(X) \} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) \times _{\operatorname{\mathcal{C}}_{-}} \{ G(Y) \} } \]
commutes up to homotopy, where the horizontal maps are the homotopy equivalences of Notation 8.1.2.14. Using Corollary 5.1.7.16, we see that $(2)$ is equivalent to the following:
- $(2')$
The outer rectangle of (8.52) is a categorical pullback diagram.
The equivalence of $(1')$ and $(2')$ is a special case of Proposition 4.5.2.18, since the right square of (8.52) is a categorical pullback square by assumption.
$\square$