Kerodon

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

Example 5.2.2.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of simplicial sets and let $C$ be a vertex of $\operatorname{\mathcal{C}}$. Then the projection map

\[ \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \twoheadrightarrow \operatorname{\mathcal{E}}_{C} \hookrightarrow \operatorname{\mathcal{E}} \]

exhibits the identity functor $\operatorname{id}_{ \operatorname{\mathcal{E}}_{C} }$ as given by covariant transport along the degenerate edge $\operatorname{id}_{C}$. See Example 5.1.3.6.