Kerodon

Corollary 7.3.8.12. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories which is Kan extended from a full subcategory $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$, and set $F_0 = F|_{ \operatorname{\mathcal{C}}^{0} }$. Then the restriction functor $\theta : \operatorname{\mathcal{C}}_{F/} \rightarrow \operatorname{\mathcal{C}}_{F_0 / }$ is a trivial Kan fibration.