Kerodon

Proof. We first show that $(2)$ implies $(1)$. Suppose that there exists a morphism of couplings

which exhibits $\lambda $ as represented by $G$ (in the sense of Definition 8.2.4.1). For each object $C_{+} \in \operatorname{\mathcal{C}}_{+}$, the functor $\widetilde{G}$ carries $\operatorname{id}_{C}$ to a universal object of $C \in \operatorname{\mathcal{C}}$ satisfying $\lambda _{+}(C) = C_{+}$. It follows that the coupling $\lambda $ is representable. Theorem 8.2.3.4, guarantees that there exists a functor $G': \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{-}$ such that $\lambda $ is representable by $G'$. Choose morphism of couplings

which exhibits $\lambda $ as represented by $G'$ (in the sense of Definition 8.2.3.5). Composing (8.42) with (8.41), we obtain a morphism of twisted arrow couplings

where the functor $\widetilde{G}' \circ \widetilde{G}$ carries isomorphisms of $\operatorname{\mathcal{C}}_{+}$ to isomorphisms of $\operatorname{\mathcal{C}}_{-}$. Invoking Corollary 8.2.2.13, we deduce that the functors $G$ and $G'$ are isomorphic, so that $\lambda $ is also representable by $G$ (Remark 8.2.3.2).

We now show that $(1)$ implies $(2)$. Assume that $\lambda $ is representable by $G$. Setting $G' = G$, we can choose a diagram (8.42) which exhibits $\lambda $ as represented by $G$. Applying Proposition 8.2.3.9, we deduce that composition with $\widetilde{G}'$ induces a homotopy equivalence of Kan complexes

In particular, there exists an object $(G, \widetilde{G}, \operatorname{id}) \in \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+} ), \operatorname{\mathcal{C}})$ such that $(\operatorname{id}, \widetilde{G}', G) \circ (G, \widetilde{G}, \operatorname{id})$ is isomorphic to $(G, \operatorname{Tw}(G), G)$ in the $\infty $-category $\operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}), \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} ) )$. In particular, the functor $\widetilde{G}' \circ \widetilde{G}: \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \rightarrow \operatorname{Tw}(\operatorname{\mathcal{C}}_{-})$ is isomorphic to the functor $\operatorname{Tw}(G)$, and therefore carries isomorphisms of $\operatorname{\mathcal{C}}_{+}$ to isomorphisms of $\operatorname{\mathcal{C}}_{-}$. It follows that the functor $\widetilde{G}: \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}) \rightarrow \operatorname{\mathcal{C}}$ carries isomorphisms in $\operatorname{\mathcal{C}}_{+}$ to universal objects of $\operatorname{\mathcal{C}}$, so that the diagram (8.41) exhibits $\lambda $ as represented by $G$. $\square$

Proof. Choose morphisms of couplings

which exhibit $\lambda $ and $\mu $ as represented by $G$ and $H$, respectively. We first prove that $(2)$ implies $(1)$. Suppose there exists a diagram (8.43), where $\widetilde{F}$ carries universal objects of $\operatorname{\mathcal{C}}$ to universal objects of $\operatorname{\mathcal{D}}$. Composing with the morphisms (8.44), we obtain a morphism of twisted arrow couplings

where the functor $\widetilde{H} \circ \widetilde{F} \circ \widetilde{G}$ carries isomorphisms in $\operatorname{\mathcal{C}}_{+}$ to isomorphisms in $\operatorname{\mathcal{D}}_{-}$. Applying Corollary 8.2.2.13, we deduce that the functors $F_{-} \circ G$ and $H \circ F_{+}$ are isomorphic.

We now show that $(1)$ implies $(2)$. Since $\lambda $ is representable and the twisted arrow pairing $\operatorname{Tw}(\operatorname{\mathcal{D}}_{-}) \rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{-}$ is corepresentable, Theorem 8.2.2.11 guarantees that there exists a morphism of pairings

where $\widetilde{T}$ carries universal objects of $\operatorname{\mathcal{C}}$ to isomorphisms in the $\infty $-category $\operatorname{\mathcal{D}}_{-}$. Composing with the pairing on the left half of (8.44), we obtain a morphism of twisted arrow pairings

Applying Corollary 8.2.2.13, we conclude that $T_{+}$ is isomorphic to the functor $F_{-} \circ G$. If condition $(1)$ is satisfied, then $T_{+}$ is also isomorphic to the functor $H \circ F_{+}$. Replacing (8.45) by an isomorphic objects of $\infty $-category $\{ F_{-} \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{C}}_{-}, \operatorname{\mathcal{D}}_{-})^{\operatorname{op}}} \times \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{Tw}(\operatorname{\mathcal{D}}_{-} ) )$, we may assume without loss of generality that $T_{+}$ is equal to $H \circ F_{+}$. Invoking the universal property of Proposition 8.2.3.9, we can further assume that (8.45) factors as a composition

Since $\widetilde{T} = \widetilde{H} \circ \widetilde{F}$ carries universal objects of $\operatorname{\mathcal{D}}$ to isomorphisms in $\operatorname{\mathcal{D}}_{-}$, the functor $\widetilde{F}$ carries universal objects of $\operatorname{\mathcal{C}}$ to universal objects of $\operatorname{\mathcal{D}}$. $\square$

Proof of Theorem 8.2.4.6. Let $\lambda : \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+}$ be a coupling which is corepresented by a functor $F: \operatorname{\mathcal{C}}_{-} \rightarrow \operatorname{\mathcal{C}}_{+}$, and let $\mu : \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{+}$ be a coupling which is represented by a functor $G: \operatorname{\mathcal{D}}_{+} \rightarrow \operatorname{\mathcal{D}}_{-}$. It follows from Theorem 8.2.2.11 that the coupling

of Remark 8.2.2.3 is representable, and that an object $(T_{-}, T, T_+) \in \operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}},\operatorname{\mathcal{D}})$ is universal if and only if the functor $T$ carries couniversal objects of $\operatorname{\mathcal{C}}$ to universal objects of $\operatorname{\mathcal{D}}$. We will complete the proof by showing that the coupling $\Phi $ is representable by the functor

Choose a morphism of couplings

which exhibits $\lambda $ as corepresented by $F$, and a morphism of couplings

which exhibits $\mu $ as represented by $G$.

Let $E: \operatorname{Tw}( \operatorname{Fun}( \operatorname{\mathcal{C}}_{+}, \operatorname{\mathcal{D}}_{+} ) ) \rightarrow \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}), \operatorname{Tw}(\operatorname{\mathcal{D}}_{+} ) )$ be the comparison map of Example 8.2.4.8. Precomposition with (8.47) and postcomposition with (8.48) determines a functor $E': \operatorname{Fun}_{\pm }( \operatorname{Tw}(\operatorname{\mathcal{C}}_{+}), \operatorname{Tw}(\operatorname{\mathcal{D}}_{+} ) ) \rightarrow \operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ for which the diagram

is commutative. We will complete the proof by showing that this diagram exhibits the coupling $\Phi $ as represented by $H$.

Fix a functor $T_{+}: \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{D}}_{+}$; we wish to show that the composite functor

carries $\operatorname{id}_{ T_{+} }$ to a universal object of $\operatorname{Fun}_{\pm }(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. Unwinding the definitions, we see that the image of $\operatorname{id}_{ T_{+} }$ is given by the triple $(G \circ T_{+} \circ F, \widetilde{G} \circ \operatorname{Tw}( T_{+} ) \circ \widetilde{F}, T_{+} ) \in \operatorname{Fun}_{\pm }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. Using the criterion of Theorem 8.2.2.11, we are reduced to showing that the composite functor

carries every couniversal object $X \in \operatorname{\mathcal{C}}$ to a universal object of $\operatorname{\mathcal{D}}$. Proposition 8.2.3.7 guarantees that $\widetilde{F}(X) \in \operatorname{Tw}( \operatorname{\mathcal{C}}_{+} )$ corresponds to an isomorphism in $\operatorname{\mathcal{C}}_{+}$, so its image under $\operatorname{Tw}( T_{+} )$ corresponds to an isomorphism in $\operatorname{\mathcal{D}}_{+}$; the desired result now follows from our hypothesis that the functor $\widetilde{G}$ carries isomorphisms in $\operatorname{\mathcal{D}}_{+}$ to universal objects of $\operatorname{\mathcal{D}}$. $\square$

Proof. By virtue of Proposition 8.2.1.7, the functors $\lambda _{+}$ and $\mu _{+}$ are cocartesian fibrations, and the functor $\widetilde{G}$ carries $\mu _{+}$-cocartesian morphisms of $\operatorname{Tw}(\operatorname{\mathcal{C}}_{+} )$ to $\lambda _{+}$-cocartesian morphisms of $\operatorname{\mathcal{C}}$. By virtue of Corollary 7.2.3.15, the functor $\widetilde{G}$ is left cofinal if and only if, for every object $C \in \operatorname{\mathcal{C}}_{+}$, the induced map $\widetilde{G}_{C}: \operatorname{Tw}( \operatorname{\mathcal{C}}_{+} ) \times _{ \operatorname{\mathcal{C}}_{+} } \{ C \} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{\mathcal{C}}_{+} } \{ C\} $ is left cofinal. It will therefore suffice to show that the following conditions are equivalent, for each object $C \in \operatorname{\mathcal{C}}_{+}$.

$(1_ C)$

The image $\widetilde{G}( \operatorname{id}_ C )$ is a universal object of $\operatorname{\mathcal{C}}$: that is, it is initial when viewed as an object of the $\infty $-category $\operatorname{\mathcal{C}}\times _{ \operatorname{\mathcal{C}}_{+} } \{ C\} $.

$(2_ C)$

The functor $\widetilde{G}_{C}$ is left cofinal.

The equivalence $(1_ C) \Leftrightarrow (2_ C)$ is a special case of Corollary 7.2.1.9, since $\operatorname{id}_{C}$ is initial when viewed as an object of the $\infty $-category $\operatorname{Tw}( \operatorname{\mathcal{C}}_{+} ) \times _{ \operatorname{\mathcal{C}}_{+} } \{ C \} $ (see Proposition 8.1.2.1). $\square$