Proposition 7.4.2.11. Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}\ar [rr]^{\Gamma } \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]^{U'} \\ & \operatorname{\mathcal{C}}, & } \]
where $U$ and $U'$ are left fibrations having covariant transport representations $\mathscr {F} = \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ and $\mathscr {F}' = \operatorname{Tr}_{\operatorname{\mathcal{E}}' / \operatorname{\mathcal{C}}}$, respectively. Then there exists a natural transformation $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ such that $\Gamma $ is compatible with $\gamma $. Moreover, $\gamma $ is unique up to homotopy.
Proof of Proposition 7.4.2.11.
Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}\ar [rr]^{\Gamma } \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]^{U'} \\ & \operatorname{\mathcal{C}}, & } \]
where $U$ and $U'$ are left fibrations. Let $\mathscr {F}, \mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be diagrams and let
\[ \alpha : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}} \quad \quad \alpha ': \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}'} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}'} \]
be natural transformations exhibiting $\mathscr {F}$ and $\mathscr {F}'$ as covariant transport representations for $U$ and $U'$, respectively. The restriction of $\alpha '$ along $\Gamma $ determines a morphism $\beta : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}'|_{\operatorname{\mathcal{E}}}$. We wish to show that $\beta $ can be realized as the composition of $\alpha $ with $\gamma |_{\operatorname{\mathcal{E}}}$, for some natural transformation $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ which is uniquely determined up to homotopy. To prove this, it suffices to show that the map of Kan complexes
\[ \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) }( \mathscr {F}, \mathscr {F}' ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{S}}) }( \underline{ \Delta ^0}_{\operatorname{\mathcal{E}}}, \mathscr {F}'|_{\operatorname{\mathcal{E}}} ) \quad \quad \gamma \mapsto \gamma |_{\operatorname{\mathcal{E}}} \circ \alpha \]
is bijective on connected components. In fact, this map is a homotopy equivalence: this is a special case of Corollary 7.4.2.17.
$\square$