Remark 7.4.1.8. In the situation of Proposition 7.4.1.6, suppose that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a left fibration. Then the extension $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$ is also a left fibration. To prove this, it will suffice to show that the fiber $\overline{\operatorname{\mathcal{E}}}_{ {\bf 0} }$ is a Kan complex (Proposition 5.1.4.14). This follows from the fact that the covariant diffraction functor
\[ \mathrm{Df}: \overline{\operatorname{\mathcal{E}}}_{ {\bf 0} } \rightarrow \operatorname{Fun}_{/ \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) = \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \]
is an equivalence of $\infty $-categories, since the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is a Kan complex by (Corollary 4.4.2.5).