Kerodon

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

Remark 5.1.6.4 (Functoriality). Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ and $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be inner fibrations of simplicial sets, and let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an equivalence of inner fibrations over $\operatorname{\mathcal{E}}$. For every morphism of simplicial sets $\operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$, the induced map $F': \operatorname{\mathcal{E}}' \times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}' \times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$ is an equivalence of inner fibrations over $\operatorname{\mathcal{E}}'$. In particular, for every object $E \in \operatorname{\mathcal{E}}$, the induced map $F_{E}: \{ E\} \times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{C}}\rightarrow \{ E\} \times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$ is an equivalence of $\infty $-categories.