Kerodon

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

Variant 5.2.3.19. Let $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a functor of $\infty $-categories. Then:

  • The projection map $\pi : \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}\rightarrow \Delta ^1$ is a cartesian fibration of $\infty $-categories.

  • The map

    \[ h: \Delta ^1 \times \operatorname{\mathcal{D}}\simeq ( \operatorname{\mathcal{D}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}} \]

    witnesses the functor $G$ as given by contravariant transport along the nondegenerate edge of $\Delta ^1$.