Theorem 5.2.1.1. Let $q: X \rightarrow S$ be a morphism of simplicial sets, let $B$ be a simplicial set, and let $q': \operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}(B,S)$ be the morphism given by postcomposition with $q$. Then:
- $(1)$
If $q$ is a cartesian fibration of simplicial sets, then $q'$ is also a cartesian fibration of simplicial sets.
- $(2)$
Assume that $q$ is a cartesian fibration, and let $e$ be an edge of the simplicial set $\operatorname{Fun}(B,X)$. Then $e$ is $q'$-cartesian if and only if, for every vertex $b \in B$, the evaluation map $\operatorname{ev}_{b}: \operatorname{Fun}(B, X) \rightarrow \operatorname{Fun}( \{ b\} , X) \simeq X$ carries $e$ to a $q$-cartesian edge of $X$.
- $(1')$
If $q$ is a cocartesian fibration of simplicial sets, then $q'$ is also a cocartesian fibration of simplicial sets.
- $(2')$
Assume that $q$ is a cocartesian fibration, and let $e$ be an edge of the simplicial set $\operatorname{Fun}(B,X)$. Then $e$ is $q'$-cocartesian if and only if, for every vertex $b \in B$, the evaluation map $\operatorname{ev}_{b}: \operatorname{Fun}(B, X) \rightarrow \operatorname{Fun}( \{ b\} , X) \simeq X$ carries $e$ to a $q$-cocartesian edge of $X$.
Proof of Theorem 5.2.1.1.
Assume that $q: X \rightarrow S$ is a cartesian fibration of simplicial sets (the case where $q$ is a cocartesian fibration can be handled by a similar argument). Let $B$ be any simplicial set and let $q': \operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}(B,S)$ be the map given by postcomposition with $q$. Then $q'$ is an inner fibration (Corollary 4.1.4.3). Let us say that an edge $e$ of the simplicial set $\operatorname{Fun}(B,X)$ is special if, for every vertex $b \in B$, the evaluation map $\operatorname{ev}_{b}: \operatorname{Fun}(B, X) \rightarrow \operatorname{Fun}( \{ b\} , X) \simeq X$ carries $e$ to a $q$-cartesian edge of $X$. By virtue of Lemma 5.2.1.5, every special edge of $\operatorname{Fun}(B,X)$ is $q'$-cartesian. Moreover, Proposition 5.2.1.3 guarantees that for every vertex $z \in \operatorname{Fun}(B,X)$ and every edge $\overline{e}: \overline{y} \rightarrow q'(z)$ of $\operatorname{Fun}(B,S)$, there exists a special edge $e: y \rightarrow z$ of $\operatorname{Fun}(B,X)$ satisfying $q'(e) = \overline{e}$. It follows that $q'$ is a cartesian fibration.
To complete the proof, it will suffice to show that every $q'$-cartesian edge $e: x \rightarrow z$ of the simplicial set $\operatorname{Fun}(B,X)$ is special. By virtue of the preceding argument, there exists a special edge $e': y \rightarrow z$ of $\operatorname{Fun}(B,X)$ satisfying $q'(e') = q'(e)$, which is also $q'$-cartesian. Applying Remark 5.1.3.8, we can choose a $2$-simplex $\sigma $ of $\operatorname{Fun}(B,X)$ as indicated in the diagram
\[ \xymatrix@R =50pt@C=50pt{ & y \ar [dr]^{ e' } & \\ x \ar [ur]^{e''} \ar [rr]^-{e} & & z, } \]
where $e''$ is an isomorphism in the $\infty $-category $\{ q'(x) \} \times _{ \operatorname{Fun}(B,S) } \operatorname{Fun}(B,X)$. For each vertex $b \in B$, the evaluation functor $\operatorname{ev}_{b}$ carries $\sigma $ to a $2$-simplex
\[ \xymatrix@R =50pt@C=50pt{ & \operatorname{ev}_ b(y) \ar [dr]^{ \operatorname{ev}_ b(e') } & \\ \operatorname{ev}_ b(x) \ar [ur]^{\operatorname{ev}_ b(x'')} \ar [rr]^-{\operatorname{ev}_ b(e)} & & \operatorname{ev}_ b(z) } \]
in the simplicial set $X$. Since $e'$ is special, the edge $\operatorname{ev}_ b(e')$ is $q$-cartesian. The edge $\operatorname{ev}_ b(e'')$ is an isomorphism in a fiber of $q$, and is therfefore also $q$-cartesian (Proposition 5.1.4.12). Applying Proposition 5.1.4.13, we deduce that $\operatorname{ev}_ b(e)$ is $q$-cartesian. Allowing the vertex $b$ to vary, we conclude that $e$ is a special edge of $\operatorname{Fun}(B,X)$, as desired.
$\square$