Kerodon

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

Corollary 5.2.5.2. Let $\pi : \operatorname{\mathcal{M}}\rightarrow \Delta ^1$ be a cocartesian fibration of $\infty $-categories with fibers $\operatorname{\mathcal{C}}= \{ 0\} \times _{\Delta ^1} \operatorname{\mathcal{M}}$ and $\operatorname{\mathcal{D}}= \{ 1\} \times _{\Delta ^1} \operatorname{\mathcal{M}}$. Let $h: \Delta ^1 \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{M}}$ be a functor which witnesses the functor $F = h|_{ \{ 1\} \times \operatorname{\mathcal{C}}}$ as given by covariant transport along the nondegenerate edge of $\Delta ^1$ (Definition 5.2.2.1). Then $h$ induces a categorical equivalence of simplicial sets

\[ (\Delta ^1 \times \operatorname{\mathcal{C}}) \coprod _{ (\{ 1\} \times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{M}}. \]