Proposition 5.3.1.21. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, let $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ be a left anodyne morphism of simplicial sets, and set $\operatorname{\mathcal{E}}_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Then the restriction map
\[ F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}_0 ) \]
of Remark 5.3.1.17 is a trivial Kan fibration.
Proof.
Since $F$ is a monomorphism of simplicial sets, the functor $F^{\ast }$ is an isofibration of $\infty $-categories (Remark 5.3.1.18). It will therefore suffice to show that $F^{\ast }$ is an equivalence of $\infty $-categories (see Proposition 4.5.5.20). By virtue of Proposition 4.5.1.22, this is equivalent to the assertion that for simplicial set $X$, the induced map
\[ \operatorname{Fun}(X, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}))^{\simeq } \rightarrow \operatorname{Fun}(X, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}_0 ))^{\simeq } \]
is a homotopy equivalence of Kan complexes (in fact, it suffices to verify this for $X = \Delta ^1$; see Theorem 4.5.7.1). Replacing $\operatorname{\mathcal{E}}$ by the fiber product $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X,\operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ and using Remark 5.3.1.19, we are reduced to proving that $F^{\ast }$ restricts to a homotopy equivalence $F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})^{\simeq } \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}_0)^{\simeq }$. Let $U^{\circ }: \operatorname{\mathcal{E}}^{\circ } \rightarrow \operatorname{\mathcal{E}}$ denote the underlying left fibration of $U$. Using Remark 5.3.1.20, we can identify $\theta $ with the map
\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}^{\circ } ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}^{\circ } ) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}^{\circ } ), \]
given by precomposition with $F$. Since $F$ is left anodyne, this map is a trivial Kan fibration (Proposition 4.2.5.4).
$\square$