Proposition 9.2.7.22. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of $\infty $-categories, let $\sigma :$
9.19
\begin{equation} \begin{gathered}\label{equation:solution-space-fibration} \xymatrix@R =50pt@C=50pt{ A \ar [d]^{f} \ar [r] & X \ar [d]^{g} \\ B \ar [r] \ar@ {-->}[ur] & Y } \end{gathered} \end{equation}
be a lifting problem in the $\infty $-category $\operatorname{\mathcal{E}}$, and let $\overline{\sigma } = U \circ \sigma $ denote the associated lifting problem in the $\infty $-category $\operatorname{\mathcal{C}}$. If the morphism $f$ is $U$-cocartesian or the morphism $\widetilde{g}$ is $U$-cartesian, then $U$ induces a homotopy equivalence of solution spaces $\operatorname{Sol}( \sigma ) \rightarrow \operatorname{Sol}( \overline{\sigma } )$.
Proof.
Let us identify the diagram (9.19) with a pair of objects $\widetilde{B}, \widetilde{X} \in \operatorname{\mathcal{E}}_{ A/ \, /Y}$. Note that $U$ induces a functor $\widetilde{U}: \operatorname{\mathcal{E}}_{ A/ \, /Y } \rightarrow \operatorname{\mathcal{C}}_{ U(A) / \, / U(Y) }$, and we have a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \operatorname{\mathcal{E}}_{ A/ \, /Y}}( \widetilde{B}, \widetilde{X} ) \ar [r] \ar [d] & \operatorname{Sol}( \sigma ) \ar [d] \\ \operatorname{Hom}_{ \operatorname{\mathcal{C}}_{ U(A) / \, / U(Y) } }( \widetilde{U}( \widetilde{B} ), \widetilde{U}( \widetilde{X} ) ) \ar [r] & \operatorname{Sol}( \overline{\sigma } ), } \]
where the horizontal maps are the homotopy equivalences supplied by Proposition 9.2.7.11. It will therefore suffice to show that the left vertical map is a homotopy equivalence. Without loss of generality, we may assume that the morphism $f$ is $U$-cocartesian. In this case, we will complete the proof by showing that the object $\widetilde{B} \in \operatorname{\mathcal{E}}_{ A/ \, /Y}$ is $\widetilde{U}$-initial. Let $U_{ / Y}: \operatorname{\mathcal{E}}_{/Y} \rightarrow \operatorname{\mathcal{C}}_{/U(Y)}$ be the inner fibration induced by $U$; by virtue of Example 7.1.6.9, it will suffice to show that the lower left of the diagram (9.19) is $U_{/Y}$-cocartesian when viewed as a morphism in $\operatorname{\mathcal{E}}_{/Y}$. This follows from our assumption that $f$ is $U$-cocartesian (Corollary 5.1.1.15).
$\square$