# Kerodon

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

Proposition 5.2.2.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, let $C$ and $D$ be objects of $\operatorname{\mathcal{C}}$, and let $f: K \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D)$ be a morphism of simplicial sets. Then:

• There exists a diagram $F: K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ which is given by covariant transport along $f$.

• An arbitrary diagram $F': K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is given by covariant transport along $f$ if and only if it is isomorphic to $F$ (as an object of the $\infty$-category $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )$).

Proof of Proposition 5.2.2.5. It follows from Theorem 5.2.1.1 that postcomposition with $U$ induces a cocartesian fibration of simplicial sets

$U': \operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{C}}).$

Let $F_0$ denote the composite map

$K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C} \hookrightarrow \operatorname{\mathcal{E}},$

which we regard as a vertex of the simplicial set $\operatorname{Fun}( K' \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$. Note that $U'( F_0 )$ is equal to the constant morphism $\underline{C}: K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{C}}$ taking the value $C$. The composite map

$\Delta ^1 \times K \times \operatorname{\mathcal{E}}_{C} \rightarrow \Delta ^1 \times K \xrightarrow {\operatorname{id}\times f} \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \rightarrow \operatorname{\mathcal{C}}$

determines an edge $e: \underline{C} \rightarrow \underline{D}$ of the simpicial set $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{C}})$. We can therefore choose a $U'$-cocartesian edge $\widetilde{e}: F_0 \rightarrow F$ of the simplicial set $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ satisfying $U'( \widetilde{e} ) = e$. Unwinding the definitions, we can identify $\widetilde{e}$ with a morphism of simplicial sets

$\widetilde{F}: \Delta ^1 \times K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$

satisfying conditions $(1)$ and $(2)$ of Definition 5.2.2.1. The characterization of $U'$-cocartesian morphisms supplied by Theorem 5.2.1.1 guarantees that $\widetilde{F}$ also satisfies condition $(3)$, so that $\widetilde{F}$ witnesses the diagram $F: K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ as given by covariant transport along $f$. This completes the proof of existence.

We now prove uniqueness. Suppose we are given another diagram $F': K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$. If $\widetilde{F}': \Delta ^1 \times K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$ witnesses $F'$ as given by covariant transport along $f$, then we can identify $\widetilde{F}'$ with a $U'$-cocartesian edge of $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ satisfying $U'( \widetilde{F}' ) = e$. Applying Remark 5.1.3.8, we conclude that $F$ and $F'$ are isomorphic as objects of the functor $\infty$-category $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )$. Conversely, if $u: F \rightarrow F'$ is any isomorphism in $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )$, then we can regard $u$ as a $U'$-cocartesian edge of $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ (Proposition 5.1.4.11). Since $U'$ is an inner fibration, we can choose a $2$-simplex $\sigma$ of $\operatorname{Fun}(K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ as indicated in the diagram

$\xymatrix@R =50pt@C=50pt{ & F \ar [dr]^-{u} & \\ F_0 \ar [ur]^-{\widetilde{e}} \ar [rr]^-{\widetilde{e}'} & & F', }$

where $\widetilde{e}'$ is an edge of $\operatorname{Fun}( K \times \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ satisfying $U'( \widetilde{e}' ) = e$. It follows from Proposition 5.1.4.12 that $\widetilde{e}'$ is $U'$-cocartesian, and therefore corresponds to a diagram $\Delta ^1 \times K \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ which witnesses $F'$ as given by covariant transport along $f$. $\square$