Proposition 9.3.1.19. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $F: K \rightarrow \operatorname{\mathcal{E}}$ be morphisms of simplicial sets, where $U$ is a right fibration. Let $n$ and $k$ be integers such that $K$ is $(k-1)$-connective and each fiber of $U$ is $n$-truncated. Then the induced map $U_{ /F}: \operatorname{\mathcal{E}}_{/F} \rightarrow \operatorname{\mathcal{C}}_{ /(U \circ F)}$ is a right fibration, and each fiber of $U_{/F}$ is $(n-k)$-truncated.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. The first assertion follows from Variant 4.3.6.11. To prove the second, we can use Remark 5.6.7.4 to reduce to the case where $\operatorname{\mathcal{E}}$ and $\operatorname{\mathcal{C}}$ are $\infty $-categories. By virtue of Theorem 4.6.4.17, it will suffice to show that each fiber of the right fibration
\[ V: \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{E}}) } \{ F \} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ U \circ F \} \]
is $(n-k)$-truncated. Fix an object $C \in \operatorname{\mathcal{C}}$, and set $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, so that $V$ restricts to a right fibration
\[ V_{C}: \operatorname{\mathcal{E}}_{C} \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{E}}) } \{ F\} \rightarrow \{ C\} \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ U \circ F \} . \]
The target of $V_{C}$ is the Kan complex $\operatorname{Hom}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( \underline{C}, U \circ F )$, where $\underline{C}$ denotes the constant functor $K \rightarrow \operatorname{\mathcal{C}}$ taking the value $C$. It follows that $V_{C}$ is a Kan fibration between Kan complexes (Corollary 4.4.3.8). We will complete the proof by showing that the Kan fibration $V_{C}$ is $(n-k)$-truncated.
Note that the morphism $V_{C}$ factors as a composition
\[ \operatorname{\mathcal{E}}_{C} \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{E}}) } \{ F\} \xrightarrow {\iota } \operatorname{Fun}(K, \operatorname{\mathcal{E}}_{C} ) \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F\} \xrightarrow {G} \{ C\} \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ U \circ F \} , \]
where $G$ is a pullback of the map
\[ \operatorname{Fun}( \Delta ^1 \times K, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \Delta ^1 \times K, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}( \{ 1\} \times K, \operatorname{\mathcal{C}}) } \operatorname{Fun}( \{ 1\} \times K, \operatorname{\mathcal{E}}) \]
and therefore a trivial Kan fibration (see Proposition 4.2.6.1). It will therefore suffice to show that the inclusion map $\iota $ is $(n-m+2)$-connective. By construction, $\iota $ fits into a pullback diagram
\[ \xymatrix { \operatorname{\mathcal{E}}_{C} \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{E}}) } \{ F\} \ar [r]^{\iota } \ar [d] & \operatorname{Fun}(K, \operatorname{\mathcal{E}}_{C} ) \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F\} \ar [d] \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{\iota _0} & \operatorname{Fun}(K, \operatorname{\mathcal{E}}_ C ). } \]
The vertical maps in this diagram are right fibrations between Kan complexes, and therefore Kan fibrations (Corollary 4.4.3.8). It follows that the diagram is a homotopy pullback square (Example 3.4.1.3). We are therefore reduced to proving that $\iota _0$ is $(n-k)$-truncated (Corollary 3.5.9.11), which is a special case of Corollary 3.5.9.26. $\square$