Kerodon

Remark 8.6.4.14. 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, let $\lambda : \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ be a left fibration, and let $\mathscr {K}: \operatorname{\mathcal{E}}^{\vee } \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a covariant transport representation for $\lambda $. Then $\lambda $ exhibits $U^{\vee }$ as a cocartesian dual of $U$ (in the sense of Definition 8.6.4.1) if and only if $\mathscr {K}$ exhibits $U^{\vee }$ as a cocartesian dual of $U$ (in the sense of Variant 8.6.4.13). See Remarks 8.3.2.19 and 8.3.2.8.