Corollary 7.4.2.17. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of simplicial sets, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a diagram, and let $\alpha : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ be a natural transformation which exhibits $\mathscr {F}$ as a covariant transport representation for $U$. Then, for every diagram $\mathscr {G}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$, precomposition with $\alpha $ induces a homotopy equivalence of Kan complexes
\[ \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) }( \mathscr {F}, \mathscr {G} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}}^{< \kappa } ) }( \underline{\Delta ^0}_{\operatorname{\mathcal{E}}}, \mathscr {G}|_{\operatorname{\mathcal{E}}} ). \]