Subsection 5.3.1 (035D): The Strict Transport Representation

5.3.1 The Strict Transport Representation

Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. To each morphism $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, the homotopy transport representation $\operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }$ associates the homotopy class $[f_{!} ]$, where $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is given by covariant transport along $f$. Beware that the functor $f_{!}$ is only well-defined up to isomorphism. For example, the value of $f_{!}$ on an object $X \in \operatorname{\mathcal{E}}_{C}$ depends on an auxiliary choice: namely, the choice of a $U$-cocartesian morphism $\widetilde{f}: X \rightarrow Y$ satisfying $U( \widetilde{f} ) = f$ (once we have made this choice, we can take $f_{!}(X)$ to be the object $Y \in \operatorname{\mathcal{E}}_{D}$). Our goal in this section is to show that, by replacing each fiber $\operatorname{\mathcal{E}}_{C}$ by an equivalent $\infty $-category, the ambiguity in the definition of the transport functors can be eliminated. More precisely, we will associate to each object $C \in \operatorname{\mathcal{C}}$ a simplicial set $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ with the following properties:

There is a trivial Kan fibration of simplicial sets $\operatorname{ev}_{C}: \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{\mathcal{E}}_{C}$ (Proposition 5.3.1.7). In particular, $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is an $\infty $-category which is equivalent to $\operatorname{\mathcal{E}}_{C}$.
Every morphism $f: C \rightarrow D$ in the category $\operatorname{\mathcal{C}}$ determines a functor of $\infty $-categories $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f): \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(D)$, which does not depend on any auxiliary choices. Moreover, the assignment $f \mapsto \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f)$ is compatible with composition, and therefore determines a functor $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ which we will refer to as the strict transport representation of $U$ (Construction 5.3.1.5).
For every morphism $f: C \rightarrow D$ in $\operatorname{\mathcal{C}}$, the diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \ar [r]^-{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } \ar [d]^{ \operatorname{ev}_ C } & \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(D) \ar [d]^{ \operatorname{ev}_{D} } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{ f_{! } } & \operatorname{\mathcal{E}}_{D} } \]

commutes up to isomorphism. Consequently, the strict transport representation $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ can be regarded as a refinement of the homotopy transport representation $\operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }$ of Construction 5.2.5.2.

We begin by considering a closely related construction.

Construction 5.3.1.1. Let $\operatorname{Cat}$ denote the ordinary category whose objects are (small) categories and whose morphisms are functors. If $\operatorname{\mathcal{C}}$ is a category, then the construction $C \mapsto \operatorname{\mathcal{C}}_{C/}$ determines a functor $\operatorname{\mathcal{C}}\rightarrow (\operatorname{Cat}_{ /\operatorname{\mathcal{C}}})^{\operatorname{op}}$, carrying each morphism $f: C \rightarrow D$ in $\operatorname{\mathcal{C}}$ to the functor

\[ \operatorname{\mathcal{C}}_{D/} \rightarrow \operatorname{\mathcal{C}}_{C/} \quad \quad ( g: D \rightarrow E ) \mapsto ( (g \circ f): C \rightarrow E). \]

For any morphism of simplicial sets $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$, we let $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set_{\Delta }}$ denote the functor given on objects by the formula

\[ \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) = \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}}). \]

We will refer to $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ as the weak transport representation of $U$.

Remark 5.3.1.2. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be an inner fibration of $\infty $-categories. Then, for every object $C \in \operatorname{\mathcal{C}}$, the simplicial set

is an $\infty $-category (Corollary 4.1.4.8).

Remark 5.3.1.3. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a morphism of simplicial sets. For each object $C \in \operatorname{\mathcal{C}}$, we can regard the identity morphism $\operatorname{id}_{C}$ as an object of the coslice $\infty $-category $\operatorname{\mathcal{C}}_{C/}$. Evaluation on $\operatorname{id}_{C}$ determines a morphism of simplicial sets

\[ \operatorname{ev}_{C}: \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{\mathcal{E}}_{C}. \]

Note that $\operatorname{id}_{C}$ is an initial object of the category $\operatorname{\mathcal{C}}_{C/}$, so the inclusion map $\{ \operatorname{id}_ C \} \hookrightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} )$ is left anodyne (Corollary 4.6.7.24). If $U$ is a left fibration of $\infty $-categories, then $\operatorname{ev}_{C}$ is a trivial Kan fibration of simplicial sets. It follows that the simplicial set $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is a Kan complex, and that $\operatorname{ev}_{C}$ is a homotopy equivalence of Kan complexes.

Example 5.3.1.4. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a left covering map of simplicial sets. Then, for every object $C \in \operatorname{\mathcal{C}}$, the evaluation map $\operatorname{ev}_{C}: \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{\mathcal{E}}_{C}$ is an isomorphism of simplicial sets (Exercise 4.2.5.5). It follows that the simplicial set $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is discrete (see Remark 4.2.3.17). We can therefore identify $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ with a functor from $\operatorname{\mathcal{C}}$ to the category of sets, which is isomorphic to the homotopy transport representation $\operatorname{hTr}_{ \operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set}$ of Definition 5.2.0.4.

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \ar [rr]^-{ F } \ar [dr] & & \operatorname{\mathcal{E}}\ar [dl]^{U} \\ & \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) & } \]

is commutative. This functor carries $\operatorname{id}_{C}$ to an object $X = \operatorname{ev}_{C}(F) \in \operatorname{\mathcal{E}}_{C}$, and carries each morphism $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$ to an object $Y \in \operatorname{\mathcal{E}}_{D}$ equipped with a morphism $\widetilde{f}: X \rightarrow Y$ satisfying $U( \widetilde{f} ) = f$. To guarantee that this data can be recovered from $X$ (at least up to isomorphism), we need to impose an additional condition which guarantees that $\widetilde{f}$ is $U$-cocartesian.

Construction 5.3.1.5 (The Strict Transport Representation). Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. For every object $C \in \operatorname{\mathcal{C}}$, we let $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ denote the full subcategory of $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) = \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}})$ spanned by those commutative diagrams

where $F$ carries each morphism of $\operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} )$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$. The construction $C \mapsto \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ determines a functor $\operatorname{sTr}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$, which we will refer to as the strict transport representation of the cocartesian fibration $U$.

Remark 5.3.1.6. In the situation of Construction 5.3.1.5, suppose that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is a left fibration of $\infty $-categories. It follows that every morphism of $\operatorname{\mathcal{E}}$ is $U$-cocartesian (Proposition 5.1.4.14), so the strict transport representation $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ coincides with the weak transport representation $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$.

We now wish to show that Construction 5.3.1.5 is a refinement of the homotopy transport representation introduced in §5.2.5. This is a consequence of the following generalization of Remark 5.3.1.3:

Proposition 5.3.1.7. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. Then, for every object $C \in \operatorname{\mathcal{C}}$, the evaluation map of Remark 5.3.1.3 induces a trivial Kan fibration of $\infty $-categories $\operatorname{ev}_{C}: \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{\mathcal{E}}_{C}$.

Corollary 5.3.1.8. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. Then the diagram of functors

\[ \xymatrix@C =50pt@R=50pt{ & \operatorname{QCat}\ar [dr] & \\ \operatorname{\mathcal{C}}\ar [ur]^-{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } \ar [rr]_-{ \operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) } } & & \mathrm{h} \mathit{\operatorname{QCat}} } \]

commutes up to natural isomorphism, given by the construction

\[ (C \in \operatorname{\mathcal{C}}) \mapsto (\operatorname{ev}_{C}: \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( C) = \operatorname{\mathcal{E}}_{C} ). \]

Proof. It follows from Proposition 5.3.1.7 that for each object $C \in \operatorname{\mathcal{C}}$, the evaluation functor $\operatorname{ev}_{C}$ is a trivial Kan fibration, and therefore an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$. To complete the proof, it will suffice to show that the construction $C \mapsto \operatorname{ev}_{C}$ is a natural transformation: that is, for every morphism $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, the diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \ar [r]^{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } \ar [d]^{\operatorname{ev}_{C}} & \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(D) \ar [d]^{ \operatorname{ev}_{D} } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{ f_{!} } & \operatorname{\mathcal{E}}_{D} } \]

commutes up to natural isomorphism. Let $s: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ be a section of the trivial Kan fibration $\operatorname{ev}_{C}$. Then the homotopy class $[s]$ is an inverse of $[ \operatorname{ev}_{C} ]$ in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$. It will therefore suffice to show that the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \ar [r]^{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } & \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(D) \ar [d]^{ \operatorname{ev}_{D} } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{ f_{!} } \ar [u]_{ s } & \operatorname{\mathcal{E}}_{D} } \]

commutes up to isomorphism: that is, that the composite functor

\[ \operatorname{\mathcal{E}}_{C} \xrightarrow {s} \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \xrightarrow { \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( D) \xrightarrow { \operatorname{ev}_{D} } \operatorname{\mathcal{E}}_{D} \]

is given by covariant transport along $f$.

Unwinding the definitions, we can identify the composition

\[ \operatorname{\mathcal{E}}_{C} \xrightarrow {s} \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \subseteq \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) = \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}}) \]

with a functor $H: \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$. Let us regard $\operatorname{id}_{C}$ and $f$ as objects of the category $\operatorname{\mathcal{C}}_{C/}$, so that $f$ lifts to a morphism $\widetilde{f}: \operatorname{id}_{C} \rightarrow f$ corresponding to an edge $e: \Delta ^1 \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} )$. Let $H_{e}$ denote the composition

\[ \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \xrightarrow {e \times \operatorname{id}} \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \times \operatorname{\mathcal{E}}_{C} \xrightarrow {H} \operatorname{\mathcal{E}}. \]

Unwinding the definitions, we see that the commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{H_{e}} \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^1 \ar [r]^{f} & \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) } \]

witnesses the composite functor $\operatorname{ev}_{D} \circ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) \circ s$ as given by covariant transport along $f$, in the sense of Definition 5.2.2.4. $\square$

Corollary 5.3.1.9 (Functoriality). Suppose we are given a commutative diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [dr]^{U} \ar [rr]^{F} & & \operatorname{\mathcal{E}}' \ar [dl]_{U'} \\ & \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}), & } \]

where $U$ and $U'$ are cocartesian fibrations. The following conditions are equivalent:

$(1)$: The functor $F$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ to $U'$-cocartesian morphisms of $\operatorname{\mathcal{E}}'$.
$(2)$: The induced map of weak transport representations $\operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} \rightarrow \operatorname{wTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}$ carries $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ into $\operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}$.

Proof. The implication $(1) \Rightarrow (2)$ is immediate from the definitions. Conversely, suppose that condition $(2)$ is satisfied, and let $f: X \rightarrow Y$ be a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$; we wish to show that $F(f)$ is $U'$-cocartesian. Set $C = U(X)$. Using Proposition 5.3.1.7, we can choose an object $\widetilde{X} \in \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ satisfying $\operatorname{ev}_{C}(\widetilde{X}) = X$. Let us identify $\widetilde{X}$ with a functor of $\infty $-categories $G: \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \rightarrow \operatorname{\mathcal{E}}$. Write $\overline{f}$ for the image $U(f)$, which we regard as a morphism in the coslice category $\operatorname{\mathcal{C}}_{C/}$. Assumption $(2)$ guarantees that $F$ carries $\widetilde{X}$ to an object of $\operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}(C)$, so that $(F \circ G)(\overline{f} )$ is a $U'$-cocartesian morphism of $\operatorname{\mathcal{E}}'$. Since $f$ is isomorphic to $G( \overline{f} )$ (as an object of the $\infty $-category $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{E}})$), it follows that $F(f)$ is also $U'$-cocartesian. $\square$

The remainder of this section is devoted to the proof of Proposition 5.3.1.7. With an eye toward future applications, we will formulate a more general result, which can be applied to cocartesian fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ where $\operatorname{\mathcal{C}}$ is not given by (the nerve of) an ordinary category.

Notation 5.3.1.10 (Cocartesian Sections). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets. Then the simplicial set

\[ \operatorname{Fun}_{/ \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) = \{ U' \} \times _{ \operatorname{Fun}(\operatorname{\mathcal{E}}',\operatorname{\mathcal{C}}) } \operatorname{Fun}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \]

is an $\infty $-category (see Corollary 4.1.4.8). We let $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ denote the full subcategory of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ whose objects are morphisms $F: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ which satisfy the identity $U \circ F = U'$ and carry $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$ to $U$-cocartesian edges of $\operatorname{\mathcal{E}}$.

Variant 5.3.1.11 (Cartesian Sections). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cartesian fibrations of simplicial sets. We let $\operatorname{Fun}^{\operatorname{Cart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ denote the full subcategory of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ whose objects are morphisms $F: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ which satisfy the identity $U \circ F = U'$ and carry $U'$-cartesian edges of $\operatorname{\mathcal{E}}'$ to $U$-cartesian edges of $\operatorname{\mathcal{E}}$. Note that we have a canonical isomorphism of simplicial sets

\[ \operatorname{Fun}^{\operatorname{Cart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})^{\operatorname{op}} = \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }( \operatorname{\mathcal{E}}'^{\operatorname{op}}, \operatorname{\mathcal{E}}^{\operatorname{op}} ). \]

In the special case $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}$, we will refer to $\operatorname{Fun}^{\operatorname{Cart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ as the $\infty $-category of cartesian sections of $U$.

Remark 5.3.1.12. Suppose we are given a commutative diagram of simplicial sets

\[ \xymatrix { \operatorname{\mathcal{E}}' \ar [dr]_{U'} \ar [rr]^{ F } & & \operatorname{\mathcal{E}}\ar [dl]^{U} \\ & \operatorname{\mathcal{C}}, & } \]

where $U$ and $U'$ are cocartesian fibrations. Let $e: X \rightarrow Y$ be an edge of $\operatorname{\mathcal{C}}$. The following conditions are equivalent:

$(1)$: For every $U'$-cocartesian edge $\widetilde{e}: \widetilde{X} \rightarrow \widetilde{Y}$ of $\operatorname{\mathcal{E}}'$ satisfying $U'( \widetilde{e} ) = e$, the image $F( \widetilde{e} )$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$.
$(2)$: For every vertex $\widetilde{X}$ of $\operatorname{\mathcal{E}}'$ satisfying $U'( \widetilde{X} ) = X$, there exists a $U'$-cocartesian edge $\widetilde{e}: \widetilde{X} \rightarrow \widetilde{Y}$ of $\operatorname{\mathcal{E}}'$ such that $F( \widetilde{e} )$ is $U$-cocartesian and $U'( \widetilde{e} ) = e$.

The implication $(1) \Rightarrow (2)$ is immediate from the definitions, and the implication $(2) \Rightarrow (1)$ follows from Remark 5.1.3.8.

Let $W$ be the collection of edges of $\operatorname{\mathcal{C}}$ which satisfy these conditions. Then $W$ contains all degenerate edges of $\operatorname{\mathcal{C}}$ and is closed under composition: that is, for every $2$-simplex

\[ \xymatrix@C =50pt@R=50pt{ & Y \ar [dr]^{ e' } & \\ X \ar [ur]^{e} \ar [rr]^{e''} & & Z } \]

of $\operatorname{\mathcal{C}}$, if $e$ and $e'$ belong to $W$, then $e''$ also belongs to $W$ (see Proposition 5.1.4.12).

Remark 5.3.1.13. We will be primarily interested in the special case of Notation 5.3.1.10 where $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ is a left fibration of simplicial sets. In this case, an object $F \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ belongs to the full subcategory $\operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ if and only if it carries every edge of $\operatorname{\mathcal{E}}'$ to a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ (Proposition 5.1.4.14).

Example 5.3.1.14. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. Then the strict transport representation $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ of Construction 5.3.1.5 is given on objects by the formula

\[ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) = \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }^{\operatorname{CCart}}( \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}}). \]

Remark 5.3.1.15. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets. Then the full subcategory $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \subseteq \operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ is replete (Example 4.4.1.12). That is, if $F$ and $G$ are isomorphic objects of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$, then $F$ carries $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$ to $U$-cocartesian edges of $\operatorname{\mathcal{E}}$ if and only if $G$ has the same property. In fact, we can be more precise: for every particular edge $e$ of $\operatorname{\mathcal{E}}'$, the image $F(e)$ is $U$-cocartesian if and only if $G(e)$ is $U$-cocartesian. To prove this, we can assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^1$, in which case it follows from Corollary 5.1.2.5.

Remark 5.3.1.16 (Detecting Isomorphisms). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of $\infty $-categories, and let $\alpha : F \rightarrow G$ be a morphism in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$. The following conditions are equivalent:

$(1)$: The morphism $\alpha $ is an isomorphism in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$.
$(2)$: The image of $\alpha $ is an isomorphism in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$.
$(3)$: The image of $\alpha $ is an isomorphism in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$.
$(4)$: For each object $X \in \operatorname{\mathcal{C}}$, the induced map $\alpha _{X}: F(X) \rightarrow G(X)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{X}$.
$(5)$: For each object $X \in \operatorname{\mathcal{C}}$, the induced map $\alpha _{X}: F(X) \rightarrow G(X)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}$.

The implications $(1) \Leftrightarrow (2)$ is immediate, the equivalences $(2) \Leftrightarrow (3)$ and $(4) \Leftrightarrow (5)$ follow from Corollary 4.4.3.19, and the equivalence $(3) \Leftrightarrow (5)$ follows from Theorem 4.4.4.4.

Remark 5.3.1.17 (Functoriality). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets. Suppose that we are given a morphism of simplicial sets $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$, and set $\operatorname{\mathcal{E}}_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ and $\operatorname{\mathcal{E}}'_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$. Then pullback along $F$ determines a morphism of simplicial sets

\[ F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ), \]

which we will refer to as the restriction map.

Remark 5.3.1.18. In the situation of Remark 5.3.1.17, suppose that $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ is a monomorphism of simplicial sets. Then the restriction map $F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 )$ is an isofibration. To see this, we first observe that $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ can be regarded as a replete subcategory of the fiber product

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ) \times _{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ) } \operatorname{Fun}_{ /\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \]

(Remark 5.3.1.15). It will therefore suffice to show that the restriction map

\[ \operatorname{Fun}_{ /\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ) \simeq \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}) \]

is an isofibration, which follows from Proposition 4.5.5.14.

Remark 5.3.1.19. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets, and let $K$ be an arbitrary simplicial set. Then:

The projection map $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ is also a cocartesian fibration.
The canonical isomorphism

\[ \operatorname{Fun}(K, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) ) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) ) \]

restricts to an isomorphism of full subcategories

\[ \operatorname{Fun}(K, \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) ) \simeq \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) ). \]

Both assertions follow immediately from Theorem 5.2.1.1.

Remark 5.3.1.20. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Let $\operatorname{\mathcal{E}}^{\circ } \subseteq \operatorname{\mathcal{E}}$ be the simplicial subset whose $n$-simplices are maps $\Delta ^{n} \rightarrow \operatorname{\mathcal{E}}$ which carry each edge of $\Delta ^ n$ to a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$, so that $U$ restricts to a left fibration $U^{\circ }: \operatorname{\mathcal{E}}^{\circ } \rightarrow \operatorname{\mathcal{C}}$ (see Corollary 5.1.4.15). Then $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}^{\circ } )$ can be identified with the core of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$.

Proposition 5.3.1.21. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, let $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ be a left anodyne morphism of simplicial sets, and set $\operatorname{\mathcal{E}}_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Then the restriction map

\[ F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}_0 ) \]

of Remark 5.3.1.17 is a trivial Kan fibration.

Proof. Since $F$ is a monomorphism of simplicial sets, the functor $F^{\ast }$ is an isofibration of $\infty $-categories (Remark 5.3.1.18). It will therefore suffice to show that $F^{\ast }$ is an equivalence of $\infty $-categories (see Proposition 4.5.5.20). By virtue of Proposition 4.5.1.22, this is equivalent to the assertion that for simplicial set $X$, the induced map

\[ \operatorname{Fun}(X, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}))^{\simeq } \rightarrow \operatorname{Fun}(X, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}_0 ))^{\simeq } \]

is a homotopy equivalence of Kan complexes (in fact, it suffices to verify this for $X = \Delta ^1$; see Theorem 4.5.7.1). Replacing $\operatorname{\mathcal{E}}$ by the fiber product $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X,\operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ and using Remark 5.3.1.19, we are reduced to proving that $F^{\ast }$ restricts to a homotopy equivalence $F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})^{\simeq } \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}_0)^{\simeq }$. Let $U^{\circ }: \operatorname{\mathcal{E}}^{\circ } \rightarrow \operatorname{\mathcal{E}}$ denote the underlying left fibration of $U$. Using Remark 5.3.1.20, we can identify $\theta $ with the map

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}^{\circ } ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}^{\circ } ) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{E}}^{\circ } ), \]

given by precomposition with $F$. Since $F$ is left anodyne, this map is a trivial Kan fibration (Proposition 4.2.5.4). $\square$

Corollary 5.3.1.22. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories, let $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be a left fibration of $\infty $-categories, and let $X$ be an initial object of $\operatorname{\mathcal{E}}'$. Then evaluation at $X$ induces a trivial Kan fibration of $\infty $-categories

\[ \operatorname{ev}_{X}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}. \]

Proof. By virtue of Remark 5.3.1.13, we can replace $U$ by the projection map $\operatorname{\mathcal{E}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$ and thereby reduce to the case where $U'$ is the identity map. In this case, the desired result follows from Proposition 5.3.1.21, since the inclusion map $\{ X\} \hookrightarrow \operatorname{\mathcal{E}}'$ is left anodyne (Corollary 4.6.7.24). $\square$

Proof of Proposition 5.3.1.7. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. By virtue of Example 5.3.1.14, it will suffice to show that the evaluation functor

\[ \operatorname{ev}_{C}: \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})}^{\operatorname{CCart}}( \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{E}}_{C} \]

is a trivial Kan fibration. This is a special case of Corollary 5.3.1.22, since the identity morphism $\operatorname{id}_{C}$ is initial when viewed as an object of the coslice category $\operatorname{\mathcal{C}}_{C/}$. $\square$

We conclude by recording another special case of Corollary 5.3.1.22 which will be useful later:

Corollary 5.3.1.23. Let $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$ be a cocartesian fibration of simplicial sets. Then evaluation at ${\bf 0}$ induces a trivial Kan fibration of simplicial sets

\[ \operatorname{Fun}_{/ \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \{ {\bf 0} \} \times _{ \operatorname{\mathcal{C}}^{\triangleleft } } \overline{\operatorname{\mathcal{E}}}. \]

Proof. Combine Corollary 5.3.1.22 with Example 4.3.7.11. $\square$