# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Definition 8.6.3.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets, and let $\lambda = (\lambda _{-}, \lambda _{+}): \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ be a left fibration of simplicial sets. We will say that $\lambda$ exhibits $U^{\vee }$ as a cocartesian dual of $U$ if the following conditions are satisfied:

$(a)$

For every vertex $C \in \operatorname{\mathcal{C}}$, the left fibration

$\lambda _{C}: \widetilde{\operatorname{\mathcal{E}}}_{C} \rightarrow \operatorname{\mathcal{E}}^{\vee }_{C} \times \operatorname{\mathcal{E}}_{C}$

is a balanced coupling of $\infty$-categories.

$(b)$

Let $\widetilde{U}: \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}$ denote the projection map $U^{\vee } \circ \lambda _{-} = U \circ \lambda _{+}$, $f: \widetilde{X} \rightarrow \widetilde{X}'$ be a $\widetilde{U}$-cocartesian edge of $\widetilde{\operatorname{\mathcal{E}}}$, and let $e: C \rightarrow C'$ be its image $\widetilde{U}(f)$ in the simplicial set $\operatorname{\mathcal{C}}$. If the object $\widetilde{X} \in \widetilde{\operatorname{\mathcal{E}}}_{C}$ is universal for the coupling $\lambda _{C}$, then the object $\widetilde{X}' \in \widetilde{\operatorname{\mathcal{E}}}_{C'}$ is universal for the coupling $\lambda _{C'}$.

We say that $U^{\vee }$ is a cocartesian dual of $U$ if there exists a left fibration $\lambda : \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ which exhibits $U^{\vee }$ as a cocartesian dual of $U$.