Kerodon

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

Remark 5.3.1.15. 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 full subcategory $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \subseteq \operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ is replete (Example 4.4.1.12). That is, if $F$ and $G$ are isomorphic objects of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$, then $F$ carries $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$ to $U$-cocartesian edges of $\operatorname{\mathcal{E}}$ if and only if $G$ has the same property. In fact, we can be more precise: for every particular edge $e$ of $\operatorname{\mathcal{E}}'$, the image $F(e)$ is $U$-cocartesian if and only if $G(e)$ is $U$-cocartesian. To prove this, we can assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^1$, in which case it follows from Corollary 5.1.2.5.