# Kerodon

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

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$.