Kerodon

Remark 5.1.0.1. The entirety of the preceding discussion can be dualized. If $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a morphism of simplicial sets, we will say that an edge $f$ of $\operatorname{\mathcal{E}}$ is $U$-cocartesian if it is $U^{\operatorname{op}}$-cartesian when viewed as an edge of the opposite simplicial set $\operatorname{\mathcal{E}}^{\operatorname{op}}$. We say that $U$ is a cocartesian fibration if the opposite functor $U^{\operatorname{op}}: \operatorname{\mathcal{E}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is a cartesian fibration. For the sake of brevity, we will sometimes state our results only for cartesian fibrations (in which case there is always a counterpart for cocartesian fibrations, which can be obtained by passing to opposite simplicial sets).