# Kerodon

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

Lemma 5.2.2.13. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, let $K$ be a simplicial set, and suppose we are given a lifting problem

5.13
\begin{equation} \begin{gathered}\label{equation:existence-uniqueness-cocartesian-lift} \xymatrix@R =50pt@C=50pt{ \{ 0\} \times K \ar [r]^-{H_0} \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^1 \times K \ar [r]^-{\overline{H}} \ar@ {-->}[ur]^{H} & \operatorname{\mathcal{C}}. } \end{gathered} \end{equation}

Then:

$(1)$

The lifting problem (5.13) admits a solution $H: \Delta ^1 \times K \rightarrow \operatorname{\mathcal{E}}$ which is a $U$-cocartesian lift of $\overline{H}$.

$(2)$

Let $F$ be any object of the $\infty$-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \{ 1\} \times K, \operatorname{\mathcal{E}})$. Then $F$ is isomorphic to $H|_{ \{ 1\} \times K}$ (as an object of $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \{ 1\} \times K, \operatorname{\mathcal{E}})$) if and only if $F = H'|_{ \{ 1\} \times K }$, where $H'$ is another $U$-cocartesian lift of $\overline{H}$ which solves the lifting problem (5.13).

Proof. By virtue of Remark 5.2.2.11 (and Theorem 5.2.1.1), we can replace $U$ by the induced map $\operatorname{Fun}(K, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}(K,\operatorname{\mathcal{C}})$ and thereby reduce to the case where $K = \Delta ^0$. In this case, assertion $(1)$ follows immediately from our assumption that $U$ is a cocartesian fibration, and assertion $(2)$ follows from Remark 5.1.3.8. $\square$