Kerodon

Little typo: Here in the statement it seems that $\widehat{\mathscr{F}}$ should be $\widetilde{\mathscr{F}}$.

By the way, it seems better to isolate the argument appearing in the proof as such an independent proposition: if $F:\mathcal{D}\to\mathcal{E}$ is a map of cocartesian fibrations over some simplicial set $\mathcal{C}$ and $\mathcal{C}_0\to\mathcal{C}$ is an inner anodyne simplicial map, then $F$ preserves cocartesian edges over $\mathcal{C}$ if and only if $F_0=F\times_{\mathcal{C}}\mathcal{C}_0$ preserves cocartesian edges over $\mathcal{C}_0$. As corollaries, 1.$F$ is an equivalence of cocartesian fibrations over $\mathcal{C}$ if and only if $F_0$ is an equivalence of cocartesian fibrations over $\mathcal{C}_0$. Here we apply this on the induced map $\mathcal{E}\to\int_{\mathcal{C}}\mathscr{F}$. 2. The restriction map $\mathrm{Fun}^{\mathrm{CCart}}_{/\mathcal{C}}(\mathcal{D},\mathcal{E})\to\mathrm{Fun}^{\mathrm{CCart}}_{/\mathcal{C}_0}(\mathcal{D}_0,\mathcal{E}_0)$ is a pullback of $\mathrm{Fun}_{/\mathcal{C}}(\mathcal{D},\mathcal{E})\to\mathrm{Fun}_{/\mathcal{C}_0}(\mathcal{D}_0,\mathcal{E}_0)$ hence is a trivial Kan fibration. This is a bit similar to Proposition 035S.

Yep. Thanks!