Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 5.3.5.2. Let $\operatorname{\mathcal{C}}$ be a category and suppose we are given a pair of functors $\mathscr {F}_0, \mathscr {F}_1 \rightarrow \operatorname{\mathcal{C}}$. Then $\mathscr {F}_0$ is levelwise equivalent to $\mathscr {F}_1$ (in the sense of Definition 5.3.5.1) if and only if the cocartesian fibrations $U_0: \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ and $U_1: \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ are equivalent (in the sense of Definition 5.1.6.1).

Proof of Proposition 5.3.5.2. Assume first that the functors $\mathscr {F}_0, \mathscr {F}_1: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ are levelwise equivalent. Then there exists a functor $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ together with levelwise categorical equivalences $\mathscr {F}_0 \rightarrow \mathscr {F} \leftarrow \mathscr {F}_1$. Applying Corollary 5.3.3.17, we see that the induced maps $\operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \leftarrow \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}})$ are equivalences of cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$.

We now prove the converse. Suppose that there exists a functor $T: \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}})$ which is an equivalence of cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$. Let $\lambda _0: \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}_0) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}})$ and $\lambda _{1}: \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}_1) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}})$ be the taut scaffolds of Construction 5.3.4.11. Then $T \circ \lambda _0$ is a scaffold of the cocartesian fibration $U_1$ (Remark 5.3.4.6). Applying Remark 5.3.4.10, we obtain levelwise categorical equivalences $\mathscr {F}_0 \rightarrow \operatorname{sTr}_{ \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}} \leftarrow \mathscr {F}_1$. $\square$