Kerodon

Proof. Since $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}'$ is a pullback of $U$, it is a left fibration. It will therefore suffice to show that $U'$ satisfies condition $(4)$ of Theorem 7.2.6.1. Suppose we are given an object $X' \in \operatorname{\mathcal{C}}'$ and a morphism of simplicial sets $e: \operatorname{\partial \Delta }^{n} \rightarrow \operatorname{\mathcal{E}}'_{X'} = \{ X' \} \times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}'$. Set $X = V(X')$, so that we can identify $e$ with a morphism from $\operatorname{\partial \Delta }^{n}$ to the fiber $\operatorname{\mathcal{E}}_{X} = \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Since $\operatorname{\mathcal{E}}$ and $\operatorname{\mathcal{C}}$ are filtered, Theorem 7.2.6.1 guarantees that we can choose a morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ for which the composite map $\operatorname{\partial \Delta }^ n \xrightarrow {e} \operatorname{\mathcal{E}}_{X} \xrightarrow { f_{!} } \operatorname{\mathcal{E}}_{Y}$ is nullhomotopic, where $f_{!}$ is given by covariant transport along $f$. Since $V$ is a left fibration, we can write $f = V(f')$ for some morphism $f': X' \rightarrow Y'$ in the $\infty $-category $\operatorname{\mathcal{C}}'$. Under the canonical isomorphisms $\operatorname{\mathcal{E}}'_{X'} \simeq \operatorname{\mathcal{E}}_{X}$ and $\operatorname{\mathcal{E}}'_{Y'} \simeq \operatorname{\mathcal{E}}_{Y}$, the morphism $f_{!}: \operatorname{\mathcal{E}}_{X} \rightarrow \operatorname{\mathcal{E}}_{Y}$ corresponds to a functor $f'_{!}: \operatorname{\mathcal{E}}'_{X'} \rightarrow \operatorname{\mathcal{E}}'_{Y'}$ given by covariant transport along $f'$ (Remark 5.2.8.5 ), so that the composition $(f'_{!} \circ e): \operatorname{\partial \Delta }^{n} \rightarrow \operatorname{\mathcal{E}}'_{Y'}$ is also nullhomotopic. $\square$