Kerodon

Proof. For each vertex $C \in \operatorname{\mathcal{C}}$, choose an $\infty $-category $\mathscr {F}'(C) \in \operatorname{\mathcal{Q}}$ which is equivalent to the fiber $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. The construction $C \mapsto \mathscr {F}'(C)$ determines a morphism of simplicial sets $\mathscr {F}': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{Q}}$, where $\operatorname{\mathcal{C}}' = \operatorname{sk}_0(\operatorname{\mathcal{C}})$ is the $0$-skeleton of $\operatorname{\mathcal{C}}$, which is a covariant transport representation of the projection map $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}'$ (see Example 5.6.5.5). Applying Corollary 5.6.5.13, we can extend $\mathscr {F}'$ to a morphism $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ which is a covariant transport representation of $U$. By construction, the morphism $\mathscr {F}$ takes values in the full subcategory $\operatorname{\mathcal{Q}}\subseteq \operatorname{\mathcal{QC}}$. $\square$

Proof. Let $U_{\Delta ^1}: \Delta ^1 \times \operatorname{\mathcal{E}}\rightarrow \Delta ^1 \times \operatorname{\mathcal{C}}$ be the product of $U$ with the identity map $\operatorname{id}_{ \Delta ^1}$, and define $U_{\operatorname{\partial \Delta }^1}: \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{C}}$ similarly. Note that the map $( \mathscr {F}_0, \mathscr {F}_1 ): \operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ is a covariant transport representation of $U_{\operatorname{\partial \Delta }^1}$. Applying Corollary 5.6.5.13, we deduce that $U_{\Delta ^1}$ admits a covariant transport representation $\mathscr {F}: \Delta ^1 \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ which satisfies $\mathscr {F}|_{ \{ 0\} \times \operatorname{\mathcal{C}}} = \mathscr {F}_0$ and $\mathscr {F}|_{ \{ 1\} \times \operatorname{\mathcal{C}}} = \mathscr {F}_1$. Let us identify $\mathscr {F}$ with a morphism $u: \mathscr {F}_{0} \rightarrow \mathscr {F}_{1}$ in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$. We will complete the proof by showing that $u$ is an isomorphism. By virtue of Theorem 4.4.4.4, it will suffice to show that for each vertex $C \in \operatorname{\mathcal{C}}$, the induced map $u_ C: \mathscr {F}_0(C) \rightarrow \mathscr {F}_1(C)$ is an isomorphism in $\operatorname{\mathcal{QC}}$. Using Remark 5.6.5.10 (and Remark 5.2.8.5), we see that the homotopy class $[u_ C]$ is isomorphic (as an object of the arrow category $\operatorname{Fun}( [1], \mathrm{h} \mathit{\operatorname{QCat}} )$) to the homotopy class of the functor $\operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$ given by covariant transport along the degenerate edge $\operatorname{id}_{C}$ of $\operatorname{\mathcal{C}}$: that is, the homotopy class of the identity functor $\operatorname{id}_{ \operatorname{\mathcal{E}}_{C} }$. $\square$

Proof of Theorem 5.6.0.2. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small cocartesian fibrations of simplicial sets. We wish to show that $U$ admits a covariant transport representation $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$, which is uniquely determined up to isomorphism (as an object of the functor $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$). The existence statement follows by applying Theorem 5.6.5.12 in the special case $\operatorname{\mathcal{C}}_0 = \emptyset $, and the uniqueness follows from Corollary 5.6.5.15. $\square$

Proof. Combine Example 5.6.5.7, Theorem 5.3.5.6, and Theorem 5.6.0.2. $\square$

Proof. The implication $(2) \Rightarrow (1)$ follows from Corollary 5.6.3.5 and Proposition 5.6.2.2. For each vertex $C \in \operatorname{\mathcal{C}}$, our assumption that $U$ is an inner covering map guarantees that the fiber $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is isomorphic to the nerve of a (small) category $\mathscr {F}_0(C)$ (Example 4.1.5.3). Let $\operatorname{\mathcal{C}}_0$ be the $0$-skeleton of $\operatorname{\mathcal{C}}$, so that the construction $C \mapsto \mathscr {F}_0(C)$ determines a morphism of simplicial sets $\mathscr {F}_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{N}_{\bullet }^{\operatorname{D}}( \operatorname{Pith}(\mathbf{Cat}) )$. Let $\operatorname{\mathcal{E}}_0$ denote the inverse image $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, so that Proposition 5.6.3.4 supplies an isomorphism of simplicial sets $G_0: \operatorname{\mathcal{E}}_0 \simeq \int _{\operatorname{\mathcal{C}}_0} \mathscr {F}_0$. In particular, $G_0$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}_0$. Invoking Theorem 5.6.5.12, we can extend $\mathscr {F}_0$ to a diagram $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{N}_{\bullet }^{\operatorname{D}}( \operatorname{Pith}( \mathbf{Cat} ) )$ and $G_0$ to a morphism of simplicial sets $G: \operatorname{\mathcal{E}}\rightarrow \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ which is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$. We will complete the proof by showing that $G$ is an isomorphism of simplicial sets. To prove this, it will suffice to show that for every simplex $\sigma : \Delta ^{n} \rightarrow \operatorname{\mathcal{C}}$, the induced map

is an isomorphism of simplicial sets. Replacing $U$ by the projection map $\Delta ^{n} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^ n$, we are reduced to proving that $G$ is an isomorphism under the additional assumption that $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. Since $U$ and the projection map $\int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ are inner covering maps, the simplicial sets $\operatorname{\mathcal{E}}$ and $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$ are isomorphic to the nerves of their homotopy categories $\mathrm{h} \mathit{\operatorname{\mathcal{E}}}$ and $\mathrm{h} \mathit{ \int _{\operatorname{\mathcal{C}}} \mathscr {F} }$, respectively; it will therefore suffice to show that the functor of ordinary categories $\mathrm{h} \mathit{G}: \mathrm{h} \mathit{\operatorname{\mathcal{E}}} \rightarrow \mathrm{h} \mathit{ \int _{\operatorname{\mathcal{C}}} \mathscr {F} }$ is an isomorphism. Our assumption that $G$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}= \Delta ^ n$ guarantees that it is an equivalence of $\infty $-categories (Corollary 5.1.7.8), so that $\mathrm{h} \mathit{G}$ is an equivalence of ordinary categories. It will therefore suffice to show that the functor $\mathrm{h} \mathit{G}$ is bijective on objects: that is, that the morphism $G$ is bijective on vertices. This is clear, since the morphism $G_0 = G|_{\operatorname{\mathcal{E}}_0}$ is an isomorphism. $\square$

Proof. We will show that $(1) \Rightarrow (2)$; the reverse implication follows from Corollary 5.6.1.16. Note that the map $\operatorname{N}_{\bullet }(U): \operatorname{N}_{\bullet }(\operatorname{\mathcal{E}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is a cocartesian fibration of simplicial sets (Example 5.1.4.2) and an inner covering map (Proposition 4.1.5.10). By virtue of Proposition 5.6.5.20, there exists a morphism of simplicial sets $\mathscr {F}': \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{D}}( \operatorname{Pith}( \mathbf{Cat}) )$ and an isomorphism of simplicial sets $V: \int _{\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})} \mathscr {F} \simeq \operatorname{N}_{\bullet }(\operatorname{\mathcal{E}})$ which is compatible with $\operatorname{N}_{\bullet }(U)$. By virtue of Theorem 2.3.4.1 (and Corollary 2.3.4.5), we have $\mathscr {F}' = \operatorname{N}_{\bullet }^{\operatorname{D}}( \mathscr {F} )$ for a unique functor of $2$-categories $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$. In this case, we can use Proposition 5.6.3.4 to identify $\int _{ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})} \mathscr {F}'$ with the nerve of the ordinary category of elements $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Under this identification, $V$ corresponds to the nerve of an isomorphism $\int _{\operatorname{\mathcal{C}}} \mathscr {F}' \simeq \operatorname{\mathcal{E}}$ which is compatible with $U$. $\square$

Proof. Combine Corollary 5.6.5.21 with Exercise 5.0.0.6. $\square$