Kerodon

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

Warning 5.2.2.3. In the situation of Construction 5.2.2.2, the covariant transport functor $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ depends not only on the cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and the morphism $f: C \rightarrow D$, but also on the system of $U$-cocartesian lifts $\{ \widetilde{f}_{X}: X \rightarrow f_{!}(X) \} _{X \in \operatorname{\mathcal{E}}_{C}}$. A different system of cocartesian lifts $\{ \widetilde{f}'_{X}: X \rightarrow f'_{!}(X) \} _{X \in \operatorname{\mathcal{E}}_{C} }$ will give rise to a different covariant transport functor $f'_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$. However, there is a canonical isomorphism of functors $\alpha : f_{!} \simeq f'_{!}$, which is uniquely determined by the requirement that for every object $X \in \operatorname{\mathcal{E}}_{C}$, the diagram

\[ \xymatrix@R =50pt@C=50pt{ & f_{!}(X) \ar [dr]^{ \alpha _{X} }_-{\sim } & \\ X \ar [ur]^-{ \widetilde{f}_{X} } \ar [rr]^-{ \widetilde{f}'_{X} } & & f'_{!}(X) } \]

is commutative.