Corollary 11.5.0.12 (01VJ)

Corollary 11.5.0.12. Let $q: X \rightarrow S$ be a locally cartesian fibration of simplicial sets, let $K$ be a simplicial set, and let $q': S \times _{ \operatorname{Fun}(B,S) } \operatorname{Fun}(B,X) \rightarrow S$ be the projection map onto the first factor. Then:

$(1)$: The morphism $q'$ is a locally cartesian fibration of simplicial sets.
$(2)$: Let $e$ be an edge of the simplicial set $S \times _{ \operatorname{Fun}(B,S)} \operatorname{Fun}(B,X)$. Then $e$ is locally $q'$-cartesian if and only if, for every vertex $b \in B$, the image of $e$ under the evaluation functor $S \times _{ \operatorname{Fun}(B,S) } \operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}( \{ b\} , X) \simeq X$ is locally $q$-cartesian.

Proof. By virtue of Remark 5.1.5.6, we may assume without loss of generality that $S = \Delta ^1$. In this case, $q$ is a cartesian fibration. The desired result now follows by combining Theorem 5.2.1.1 with Remark 5.1.4.6. $\square$