Kerodon

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

Corollary 5.3.5.12. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be cocartesian fibrations of $\infty$-categories, having strict transport representations $\operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ and $\operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}}$, respectively. Then the tautological map

$\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{Set_{\Delta }}) }( \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}, \operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}})_{\bullet }$

is an equivalence of $\infty$-categories.

Proof. By virtue of Remark 5.3.4.10, we have a pullback diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) \ar [d] \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{Set_{\Delta }}) }( \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}, \operatorname{sTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}} )_{\bullet } \ar [d] \\ \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{Set_{\Delta }}) }( \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}, \operatorname{wTr}_{\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}} )_{\bullet }, }$

where the vertical maps are inclusions of replete full subcategories (and are therefore isofibrations; see Example 4.4.1.11). Since the bottom horizontal map is an equivalence of $\infty$-categories (Corollary 5.3.5.11), it follows that the upper horizontal map is also an equivalence of $\infty$-categories (Corollary 4.5.2.23). $\square$