Kerodon

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$