$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 8.6.4.7. Let $U: \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ and $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \Delta ^1$ be cocartesian fibrations of $\infty $-categories, and let $F: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}_1$ and $F^{\vee }: \operatorname{\mathcal{E}}^{\vee }_0 \rightarrow \operatorname{\mathcal{E}}^{\vee }_{1}$ be functors given by covariant transport along the nondegenerate edge of $\Delta ^1$. Let $\lambda = (\lambda _{-}, \lambda _{+}): \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}^{\vee } \times _{ \Delta ^1 } \operatorname{\mathcal{E}}$ be a left fibration, and suppose that the associated couplings
\[ \lambda _0: \widetilde{\operatorname{\mathcal{E}}}_0 \rightarrow \operatorname{\mathcal{E}}_{0}^{\vee } \times \operatorname{\mathcal{E}}_{0} \quad \quad \lambda _{1}: \widetilde{\operatorname{\mathcal{E}}}_{1} \rightarrow \operatorname{\mathcal{E}}_{1}^{\vee } \times \operatorname{\mathcal{E}}_{1} \]
are representable by functors $G_0: \operatorname{\mathcal{E}}_0 \rightarrow (\operatorname{\mathcal{E}}_0^{\vee })^{\operatorname{op}}$ and $G_1: \operatorname{\mathcal{E}}_1 \rightarrow (\operatorname{\mathcal{E}}_1^{\vee })^{\operatorname{op}}$, respectively. If $\lambda $ satisfies condition $(b)$ of Definition 8.6.4.1, then the diagram of $\infty $-categories
8.80
\begin{equation} \begin{gathered}\label{equation:balanced-coupling-family-over-edge1} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_{0} \ar [r]^-{F} \ar [d]^{ G_0 } & \operatorname{\mathcal{E}}_{1} \ar [d]^{ G_1 } \\ (\operatorname{\mathcal{E}}^{\vee }_{0})^{\operatorname{op}} \ar [r]^-{ (F^{\vee } )^{\operatorname{op}} } & ( \operatorname{\mathcal{E}}^{\vee }_{1})^{\operatorname{op}} } \end{gathered} \end{equation}
commutes up to isomorphism.
Proof.
Let $\widetilde{U}$ denote the composite map
\[ \widetilde{\operatorname{\mathcal{E}}} \xrightarrow {\lambda } \operatorname{\mathcal{E}}^{\vee } \times _{ \Delta ^1 } \operatorname{\mathcal{E}}\rightarrow \Delta ^1. \]
Using Proposition 5.1.4.14, we see that $\lambda $ is a cocartesian fibration, and that an edge $e$ of $\widetilde{\operatorname{\mathcal{E}}}$ is $\widetilde{U}$-cocartesian if and only if $\lambda _{+}(e)$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ and $\lambda _{-}(e)$ is a $U^{\vee }$-cocartesian edge of $\operatorname{\mathcal{E}}^{\vee }$. Let $\widetilde{F}: \widetilde{\operatorname{\mathcal{E}}}_0 \rightarrow \widetilde{\operatorname{\mathcal{E}}}_1$ be given by covariant transport along the nondegenerate edge of $\Delta ^1$. Using Remark 5.2.8.5, we see that the diagram of $\infty $-categories
8.81
\begin{equation} \begin{gathered}\label{equation:balanced-coupling-family-over-edge2} \xymatrix@R =50pt@C=50pt{ \widetilde{\operatorname{\mathcal{E}}}_0 \ar [r]^-{ \widetilde{F} } \ar [d]^{ \lambda _0 } & \widetilde{\operatorname{\mathcal{E}}}_1 \ar [d]^{ \lambda _1} \\ \operatorname{\mathcal{E}}_0^{\vee } \times \operatorname{\mathcal{E}}_0 \ar [r]^-{ F^{\vee } \times F} & \operatorname{\mathcal{E}}_1^{\vee } \times \operatorname{\mathcal{E}}_1 } \end{gathered} \end{equation}
commutes up to isomorphism. Since $\lambda _1$ is an isofibration, we can replace $\widetilde{F}$ by an isomorphic functor to arrange that the diagram (8.81) is strictly commutative (see Corollary 4.4.5.6). Condition $(b)$ of Definition 8.6.4.1 guarantees that the functor $\widetilde{F}$ carries universal objects of $\widetilde{\operatorname{\mathcal{E}}}_0$ (for the coupling $\lambda _0$) to universal objects of $\widetilde{\operatorname{\mathcal{E}}}_1$ (for the coupling $\lambda _1$). The commutativity of the diagram (8.80) now follows from Corollary 8.2.4.4.
$\square$