Proposition 8.6.8.9 (05WM)

Proposition 8.6.8.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets, let $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{QC}}$ be a diagram, and let $T: \operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{Tw}(\operatorname{\mathcal{C}}^{\operatorname{op}} ) \rightarrow \int _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F}$ exhibit $\mathscr {F}$ as a contravariant transport representation for $U$ (Remark 8.6.8.2). Then, for every edge $e: C \rightarrow C'$ of $\operatorname{\mathcal{C}}$, the diagram of $\infty $-categories

\[ \xymatrix { \operatorname{\mathcal{E}}_{C'} \ar [d]^{ e^{\ast } } \ar [r]^{T_{C'}}_{\sim } & \{ C'\} \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \int _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F} \ar [d]^{ e_{!} } & \mathscr {F}(C') \ar [l]^{\sim } \ar [d]^{ \mathscr {F}(e) } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{T_{C'}}_{\sim } & \{ C\} \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \int _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F} & \mathscr {F}(C) \ar [l]^{\sim } } \]

commutes up to isomorphism. Here the horizontal maps are the equivalences of Remark 8.6.8.2, $e^{\ast }$ is given by contravariant transport for the cartesian fibration $U$, and $e_{!}$ is given by covariant transport for the cocartesian fibration $\int _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$.

Proof. The commutativity of the left square follows from Proposition 8.6.1.5, and the commutativity of the right square from Corollary 5.6.2.23. $\square$