Kerodon

Remark 11.10.1.3. Let $S$ be a simplicial set. Then the simplicial categories $\operatorname{Cart}(S)$ and $\operatorname{CCart}(S)$ are locally Kan.

Remark 11.10.1.4. Let $S$ be a simplicial set. Then the construction $X \mapsto X^{\operatorname{op}}$ determines an isomorphism of simplicial categories $\operatorname{CCart}(S) \simeq \operatorname{Cart}( S^{\operatorname{op}} )^{\operatorname{c}}$; here $\operatorname{Cart}(S^{\operatorname{op}})^{\operatorname{c}}$ denotes the conjugate of the simplicial category $\operatorname{Cart}(S^{\operatorname{op}})$ (see Example 2.4.2.12).

Remark 11.10.1.8. Let $q: X \rightarrow S$ be a cocartesian fibration of simplicial sets and let $q': X' \rightarrow S$ be a left fibration. Then $q'$ is also a cocartesian fibration, and every edge of $X'$ is $q'$-cocartesian (Proposition 5.1.4.14). In particular:

• Every morphism $f: X \rightarrow X'$ in $(\operatorname{Set_{\Delta }})_{/S}$ carries $q$-cocartesian edges of $X$ to $q'$-cocartesian edges of $X'$. That is, we have $\operatorname{Fun}_{/S}^{\operatorname{CCart}}(X,X') = \operatorname{Fun}_{/S}(X,X')$.

• The simplicial set $\operatorname{Fun}_{/S}(X,X')$ is a Kan complex (Corollary 4.4.2.5), and is therefore equal to its core $\operatorname{Fun}_{/S}(X,X')^{\simeq }$.

It follows that we can regard $\operatorname{LFib}(S)$ as a full subcategory of the simplicial category $\operatorname{CCart}(S)$. Similarly, we can regard $\operatorname{RFib}(S)$ as a full subcategory of the simplicial category $\operatorname{Cart}(S)$. We therefore obtain a diagram of fully faithful inclusions

Remark 11.10.1.9 (Functoriality). Let $f: S' \rightarrow S$ be a morphism of simplicial sets. Then $f$ determines a functor of simplicial categories $f^{\ast }: (\operatorname{Set_{\Delta }})_{/S} \rightarrow (\operatorname{Set_{\Delta }})_{/S'}$, given on objects by the formula $f^{\ast }(X) = S' \times _{S} X$. Since the collection of cartesian fibrations is stable under base change (Remark 5.1.4.6), $f^{\ast }$ restricts to a simplicial functor $\operatorname{Cart}(S) \rightarrow \operatorname{Cart}(S')$, which we will also denote by $f^{\ast }$. Similarly we obtain pullback functors

Remark 11.10.1.12. Let $q: X \rightarrow S$ and $q': X' \rightarrow S$ be cartesian fibrations of simplicial sets. Then a morphism $f: X \rightarrow X'$ is an equivalence of cartesian fibrations over $S$ if and only if the opposite morphism $f^{\operatorname{op}}: X^{\operatorname{op}} \rightarrow X'^{\operatorname{op}}$ is an equivalence of cocartesian fibrations over $S^{\operatorname{op}}$. In particular, the cartesian fibrations $q$ and $q'$ are equivalent if and only if the cocartesian fibrations $q^{\operatorname{op}}: X^{\operatorname{op}} \rightarrow S^{\operatorname{op}}$ and $q'^{\operatorname{op}}: X'^{\operatorname{op}} \rightarrow S^{\operatorname{op}}$ are equivalent.

Remark 11.10.1.14 (Pullback Stability). Let $q: X \rightarrow S$ and $q': X' \rightarrow S$ be cocartesian fibrations of simplicial sets, and let $f: X \rightarrow X'$ be an equivalence of cocartesian fibrations over $S$. For any morphism of simplicial sets $T \rightarrow S$, the induced map $f_{T}: T \times _{S} X \rightarrow T \times _{S} X'$ is an equivalence of cocartesian fibrations over $T$ (this follows immediately from Remark 11.10.1.9). In particular, for every vertex $s \in S$, the induced map of fibers $f_{s}: X_{s} \rightarrow X'_{s}$ is an equivalence of $\infty $-categories.

Remark 11.10.1.18. We will see later that Corollary 11.10.1.17 remains valid without the assumption that $\operatorname{\mathcal{E}}$, $\operatorname{\mathcal{E}}'$, and $\operatorname{\mathcal{C}}$ are $\infty $-categories; see Corollary .