Kerodon

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

Notation 5.3.1.10 (Cocartesian Sections). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets. Then the simplicial set

\[ \operatorname{Fun}_{/ \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) = \{ U' \} \times _{ \operatorname{Fun}(\operatorname{\mathcal{E}}',\operatorname{\mathcal{C}}) } \operatorname{Fun}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \]

is an $\infty $-category (see Corollary 4.1.4.8). We let $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ denote the full subcategory of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ whose objects are morphisms $F: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ which satisfy the identity $U \circ F = U'$ and carry $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$ to $U$-cocartesian edges of $\operatorname{\mathcal{E}}$.