# Kerodon

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

Proposition 5.2.4.16. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty$-categories. Then:

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

• The map

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

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

Proof. Proposition 5.2.4.11 guarantees that the relative join $\operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is an $\infty$-category, so that the projection map $\pi : \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \Delta ^1$ is automatically an inner fibration (Proposition 4.1.1.10). To prove that it is a cocartesian fibration, we must show that for every object $X \in \operatorname{\mathcal{C}}$ there exists an object $Y \in \operatorname{\mathcal{D}}$ and a $\pi$-cocartesian morphism $f: X \rightarrow Y$ in the $\infty$-category $\operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$. By virtue of Lemma 5.2.4.15, this is equivalent to the statement that there exists an object $Y \in \operatorname{\mathcal{D}}$ equipped with an isomorphism $e: F(X) \rightarrow Y$, which is clear (we can take $Y = F(X)$ and $e$ to be the identity morphism). This proves assertion $(1)$. To prove assertion $(2)$, we first observe that the restriction $h|_{ \{ 1\} \times \operatorname{\mathcal{C}}}$ coincides with the functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. It will therefore suffice to show that, for each object $X \in \operatorname{\mathcal{C}}$, the edge $h|_{ \Delta ^1 \times \{ X\} }$ is $\pi$-cocartesian. Note that the correspondence of Remark 5.2.4.14 carries $h|_{ \Delta ^1 \times \{ X\} }$ to the identity morphism $\operatorname{id}_{ F(X)}$ in the $\infty$-category $\operatorname{\mathcal{D}}$, so the desired result follows from the criterion of Lemma 5.2.4.15. $\square$