7.4.2 Digression: Functoriality of Covariant Transport
Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. For every diagram $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$, let $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ denote the $\infty $-category of elements of $\mathscr {F}$ (Definition 5.6.2.1), so that the projection map $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Example 5.6.2.9). By virtue of Corollary 5.6.0.6, the construction $\mathscr {F} \mapsto \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ induces a bijection
\[ \xymatrix { \{ \textnormal{Diagrams $\operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$} \} / \textnormal{Isomorphism} \ar [d]^{\theta } \\ \{ \textnormal{Essentially small left fibrations $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$} \} / \textnormal{Equivalence} }. \]
Our goal in this section is to prove a stronger result, which upgrades $\theta $ to an equivalence of homotopy categories (Theorem 7.4.2.4).
Notation 7.4.2.1. Let $\operatorname{\mathcal{C}}$ be a simplicial set. We let $\operatorname{LFib}( \operatorname{\mathcal{C}})$ denote the full subcategory of $(\operatorname{Set_{\Delta }})_{ / \operatorname{\mathcal{C}}}$ spanned by the (essentially small) left fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. We will regard $\operatorname{LFib}( \operatorname{\mathcal{C}})$ as a simplicially enriched category, with morphism spaces given by
\[ \operatorname{Hom}_{ \operatorname{LFib}(\operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' )_{\bullet } = \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ). \]
It follows from Corollary 4.4.2.5 that the simplicial category $\operatorname{LFib}(\operatorname{\mathcal{C}})$ is locally Kan.
Definition 7.4.2.2. Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}\ar [rr]^{\Gamma } \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]^{U'} \\ & \operatorname{\mathcal{C}}, & } \]
where $U$ and $U'$ are left fibrations having covariant transport representations $\mathscr {F} = \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ and $\mathscr {F}' = \operatorname{Tr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}$, respectively. We say that a natural transformation $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ is compatible with $\Gamma $ if the diagram
\[ \xymatrix { & \underline{\Delta ^0}_{\operatorname{\mathcal{E}}} \ar [dl]^{ \alpha } \ar [dr]_{ \alpha '|_{ \operatorname{\mathcal{E}}}} & \\ \mathscr {F}|_{ \operatorname{\mathcal{E}}} \ar [rr]^{ \gamma |_{ \operatorname{\mathcal{E}}} } & & \mathscr {F}'|_{ \operatorname{\mathcal{E}}} } \]
commutes up to homotopy (in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}})$). Here $\alpha : \underline{\Delta ^0}_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ and $\alpha ': \underline{\Delta ^0}_{\operatorname{\mathcal{E}}' } \rightarrow \mathscr {F}'|_{\operatorname{\mathcal{E}}'}$ denote natural transformations which exhibit $\mathscr {F}$ and $\mathscr {F}'$ as covariant transport representations of $U$ and $U'$, in the sense of Definition 7.4.1.8.
Warning 7.4.2.3. The compatibility condition of Definition 7.4.2.2 depends not only on the morphisms $\gamma $ and $\Gamma $, but also on the choice of natural transformations
\[ \alpha : \underline{\Delta ^0}_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}} \quad \quad \alpha ': \underline{\Delta ^0}_{\operatorname{\mathcal{E}}' } \rightarrow \mathscr {F}'|_{\operatorname{\mathcal{E}}'} \]
exhibiting $\mathscr {F}$ and $\mathscr {F}'$ as covariant transport representations for $U$ and $U'$, respectively. We will sometimes omit mention of these choices, particularly in situations where there are natural candidates for $\alpha $ and $\alpha '$. For example:
Suppose that $\operatorname{\mathcal{E}}= \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ and $\operatorname{\mathcal{E}}' = \int _{\operatorname{\mathcal{C}}} \mathscr {F}'$ are the $\infty $-categories of elements of $\mathscr {F}$ and $\mathscr {F}'$, respectively. Then we can take $\alpha $ and $\alpha '$ to be the natural transformations of Example 7.4.1.10.
Suppose that $\mathscr {F}$ and $\mathscr {F}'$ are obtained from strictly commutative diagrams of Kan complexes $\mathscr {F}_0, \mathscr {F}'_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{Kan}$, and that $\operatorname{\mathcal{E}}= \operatorname{N}_{\bullet }^{\mathscr {F_0} }(\operatorname{\mathcal{C}}_0)$ and $\operatorname{\mathcal{E}}' = \operatorname{N}_{\bullet }^{\mathscr {F}'_0}(\operatorname{\mathcal{C}}_0)$ are the weighted nerves introduced in Definition 5.3.3.1. Then we can take $\alpha $ and $\alpha '$ to be the natural transformations given in Example 7.4.1.11.
Suppose $\operatorname{\mathcal{C}}= \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_0 )$ and that the diagrams $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ are the homotopy coherent nerve of the strict transport representations $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}_0}, \operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}_0}: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{Kan}$. In this case, we can take $\alpha $ and $\alpha '$ to be the natural transformations described in Example 7.4.1.12 (which are well-defined up to homotopy).
Theorem 7.4.2.4. Let $\operatorname{\mathcal{C}}$ be a simplicial set. Then the construction
\[ ( \mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}) \mapsto ( U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}) \]
determines an equivalence of homotopy categories
\[ \mathrm{h} \mathit{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) } \rightarrow \mathrm{h} \mathit{ \operatorname{LFib}( \operatorname{\mathcal{C}}) }, \]
which carries (the homotopy class of) a natural transformation $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ to (the homotopy class) of a map $\Gamma \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \int _{\operatorname{\mathcal{C}}} \mathscr {F}, \int _{\operatorname{\mathcal{C}}} \mathscr {F}' )$ which is compatible with $\gamma $.
Our proof of Theorem 7.4.2.4 begins with the following observation:
Proposition 7.4.2.6. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ be a natural transformation between functors $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ which are given as covariant transport representations for left fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$, respectively. Then there exists a morphism $\Gamma \in \operatorname{Hom}_{ \operatorname{LFib}(\operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' )$ which is compatible with $\gamma $. Moreover, the homotopy class $[\Gamma ]$ is uniquely determined.
Proof.
Fix natural transformations $\alpha : \underline{\Delta ^0}_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ and $\alpha ': \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}'|_{\operatorname{\mathcal{E}}'}$ which exhibit $\mathscr {F}$ and $\mathscr {F}'$ are covariant transport representations for $U$ and $U'$, respectively. Then $\alpha '$ induces a map of Kan complexes
7.50
\begin{eqnarray} \label{equation:induced-map-of-covariant-transport} \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) & \xrightarrow {\rho } & \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}}) }( \underline{\Delta ^0}_{\operatorname{\mathcal{E}}}, \mathscr {F}'|_{\operatorname{\mathcal{E}}} ), \end{eqnarray}
which carries a morphism $\Gamma \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' )$ to the pullback of $\alpha '$ along $\Gamma $. To prove Proposition 7.4.2.6, it suffices to show that $\rho $ is bijective on connected components. In fact, the morphism $\rho $ is a homotopy equivalence: this follows by applying Proposition 7.4.1.14 to the left fibration $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$.
$\square$
Example 7.4.2.7. Let $\operatorname{\mathcal{C}}$ be a simplicial set and let $\operatorname{Path}[\operatorname{\mathcal{C}}]_{\bullet }$ denote the simplicial path category of $\operatorname{\mathcal{C}}$ (Notation 2.4.4.2). In this case, we can identify diagrams $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ with simplicially enriched functors $\mathscr {F}, \mathscr {F}': \operatorname{Path}[\operatorname{\mathcal{C}}]_{\bullet } \rightarrow \operatorname{Kan}$. Suppose that $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ arises from a natural transformation of simplicial functors $\gamma _0: \mathscr {F}_0 \rightarrow \mathscr {F}'_0$. Applying Construction 
to $\gamma _0$, we obtain a map $\Gamma : \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \int _{\operatorname{\mathcal{C}}} \mathscr {F}'$ which is compatible with $\gamma $.
Example 7.4.2.8. Let $\operatorname{\mathcal{C}}= \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}_0)$ be the nerve of a category $\operatorname{\mathcal{C}}_0$. Suppose that $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ are obtained as the nerves of strictly commutative diagrams $\mathscr {F}_0, \mathscr {F}'_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{Kan}$, and let $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ be obtained from a natural transformation $\gamma _0: \mathscr {F}_0 \rightarrow \mathscr {F}'_0$. Applying the weighted nerve construction to $\gamma _0$, we obtain a functor $\Gamma : \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}_0) \rightarrow \operatorname{N}_{\bullet }^{ \mathscr {F}'_0 }(\operatorname{\mathcal{C}}_0)$ which is compatible with $\gamma $.
Example 7.4.2.9. Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be the covariant transport representation of a left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, and let $\gamma : \mathscr {F} \rightarrow \mathscr {F}$ be the identity transformation. Then the identity map $\Gamma : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}$ is compatible with $\gamma $.
The main content of Theorem 7.4.2.4 is contained in the following:
Proposition 7.4.2.11. Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}\ar [rr]^{\Gamma } \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]^{U'} \\ & \operatorname{\mathcal{C}}, & } \]
where $U$ and $U'$ are left fibrations having covariant transport representations $\mathscr {F} = \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ and $\mathscr {F}' = \operatorname{Tr}_{\operatorname{\mathcal{E}}' / \operatorname{\mathcal{C}}}$, respectively. Then there exists a natural transformation $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ such that $\Gamma $ is compatible with $\gamma $. Moreover, $\gamma $ is unique up to homotopy.
Example 7.4.2.12. In the situation of Proposition 7.4.2.11, suppose that $\operatorname{\mathcal{C}}= \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}_0)$ be the nerve of a category $\operatorname{\mathcal{C}}_0$, and that $\mathscr {F}$ and $\mathscr {F}'$ are given as the (homotopy coherent) nerves of the strict transport representations $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}_0}, \operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}_0}: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{Kan}$. In this case, we can take $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ to be the (homotopy coherent) nerve of the natural transformation $\gamma _0: \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}_0} \rightarrow \operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}_0}$ given by composition with $\Gamma $. See Examples 7.4.2.8 and 7.4.1.12.
Proof of Theorem 7.4.2.4.
Let $\operatorname{\mathcal{C}}$ be a simplicial set. It follows from Proposition 7.4.2.6 (together with Example 7.4.2.9 and Remark 7.4.2.10) that there is a unique functor
\[ \Theta : \mathrm{h} \mathit{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) } \rightarrow \mathrm{h} \mathit{ \operatorname{LFib}(\operatorname{\mathcal{C}}) } \]
which is given on objects by the construction $\mathscr {F} \mapsto \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ and on morphisms by the construction $[ \gamma ] \mapsto [\Gamma ]$, where $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ denotes a natural transformation and $\Gamma \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \int _{\operatorname{\mathcal{C}}} \mathscr {F}, \int _{\operatorname{\mathcal{C}}} \mathscr {F}' )$ is chosen to be compatible with $\gamma $. It follows from Corollary 5.6.0.6 that the functor $\Theta $ is bijective on isomorphism classes: in particular, it is essentially surjective. To complete the proof, it suffices to show that $\Theta $ is fully faithful, which is a reformulation of Proposition 7.4.2.11.
$\square$
Our proof of Proposition 7.4.2.11 will make use of the following reformulation of Definition 7.4.1.8:
Proposition 7.4.2.13 (Covariant Transport as a Kan Extension). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small left fibration of $\infty $-categories, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be a functor, and let $\alpha : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ be a natural transformation. Then $\alpha $ exhibits $\mathscr {F}$ as covariant transport representation for $U$ (in the sense of Definition 7.4.1.8) if and only if it exhibits $\mathscr {F}$ as a left Kan extension of $\underline{ \Delta ^0}_{\operatorname{\mathcal{E}}}$ along $U$ (in the sense of Variant 7.3.1.5).
Proof.
Using Proposition 7.3.4.1, we can reduce to the special case where the $\infty $-category $\operatorname{\mathcal{C}}= \{ C\} $ consists of a single vertex. In this case, the desired result is a reformulation of Example 7.1.2.10.
$\square$
Variant 7.4.2.14. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of $\infty $-categories and let $\kappa $ be an uncountable cardinal. Suppose we are given a diagram $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ and a natural transformation $\alpha : \underline{ \Delta ^{0} }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$. If $U$ is essentially $\kappa $-small, then the following conditions are equivalent:
- $(1)$
The natural transformation $\alpha $ exhibits $\mathscr {F}$ as a covariant transport representation for $U$.
- $(2)$
The natural transformation $\alpha $ exhibits $\mathscr {F}$ as a left Kan extension of the constant functor $\underline{ \Delta ^{0} }|_{\operatorname{\mathcal{E}}}$ along $U$.
Beware that, if $U$ is not assumed to be essentially $\kappa $-small, then it is possible for condition $(2)$ to be satisfied while condition $(1)$ is not (see Exercise 7.1.2.12).
Corollary 7.4.2.15. Let $\kappa $ be an uncountable cardinal and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of $\infty $-categories which is essentially $\kappa $-small. Then a functor $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ is a covariant transport representation for $U$ (in the sense of Definition 5.6.5.1) if and only if it is a left Kan extension of the constant functor $\underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}}$ along $U$.
Corollary 7.4.2.17. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of simplicial sets, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a diagram, and let $\alpha : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ be a natural transformation which exhibits $\mathscr {F}$ as a covariant transport representation for $U$. Then, for every diagram $\mathscr {G}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$, precomposition with $\alpha $ induces a homotopy equivalence of Kan complexes
\[ \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) }( \mathscr {F}, \mathscr {G} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}}^{< \kappa } ) }( \underline{\Delta ^0}_{\operatorname{\mathcal{E}}}, \mathscr {G}|_{\operatorname{\mathcal{E}}} ). \]
Proof.
Combine Proposition 7.4.2.13 with the universal property of left Kan extensions (Proposition 7.3.6.1).
$\square$
Proof of Proposition 7.4.2.11.
Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}\ar [rr]^{\Gamma } \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]^{U'} \\ & \operatorname{\mathcal{C}}, & } \]
where $U$ and $U'$ are left fibrations. Let $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be diagrams and let
\[ \alpha : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}} \quad \quad \alpha ': \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}'} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}'} \]
be natural transformations exhibiting $\mathscr {F}$ and $\mathscr {F}'$ as covariant transport representations for $U$ and $U'$, respectively. The restriction of $\alpha '$ along $\Gamma $ determines a morphism $\beta : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}'|_{\operatorname{\mathcal{E}}}$. We wish to show that $\beta $ can be realized as the composition of $\alpha $ with $\gamma |_{\operatorname{\mathcal{E}}}$, for some natural transformation $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ which is uniquely determined up to homotopy. To prove this, it suffices to show that the map of Kan complexes
\[ \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) }( \mathscr {F}, \mathscr {F}' ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}}) }( \underline{ \Delta ^0}_{\operatorname{\mathcal{E}}}, \mathscr {F}'|_{\operatorname{\mathcal{E}}} ) \quad \quad \gamma \mapsto \gamma |_{\operatorname{\mathcal{E}}} \circ \alpha \]
is bijective on connected components. In fact, this map is a homotopy equivalence: this is a special case of Corollary 7.4.2.17.
$\square$