Proposition 8.6.1.5. Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration, and let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be a cartesian fibration. Let $e: C \rightarrow C'$ be an edge of $\operatorname{\mathcal{C}}$, and let
\[ e^{\ast }: \operatorname{\mathcal{E}}^{\dagger }_{C} \rightarrow \operatorname{\mathcal{E}}^{\dagger }_{C'} \quad \quad e_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C'} \]
be functors given by contravariant and covariant transport along $e$ for the fibrations $U^{\dagger }$ and $U$, respectively. If $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ is a morphism which satisfies conditions $(0)$ and $(2)$ of Definition 8.6.1.1, then the diagram of $\infty $-categories
\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}^{\dagger }_{C} \ar [d]^{ T_{C} } \ar [r]^-{ e^{\ast } } & \operatorname{\mathcal{E}}^{\dagger }_{C'} \ar [d]^{ T_{C'} } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^-{ e_{!} } & \operatorname{\mathcal{E}}_{C'} } \]
commutes up to isomorphism.
Proof.
The restriction of $T$ to the inverse image of the vertex $\{ e\} \subseteq \operatorname{Tw}(\operatorname{\mathcal{C}})$ determines a functor of $\infty $-categories $T_{e}: \operatorname{\mathcal{E}}^{\dagger }_{C} \rightarrow \operatorname{\mathcal{E}}_{C'}$. To complete the proof, it will suffice to verify the following pair of assertions:
- $(a)$
The functor $T_{e}$ is isomorphic to the composition $T_{C'} \circ e^{\ast }$.
- $(b)$
The functor $T_{e}$ is isomorphic to the composition $e_{!} \circ T_{C}$.
We begin by proving $(a)$. Choose a diagram
\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}^{\dagger }_{C} \times \Delta ^1 \ar [r]^-{H} \ar [d] & \operatorname{\mathcal{E}}^{\dagger } \ar [d]^{U^{\dagger } } \\ \Delta ^1 \ar [r]^-{e} & \operatorname{\mathcal{C}}^{\operatorname{op}} } \]
which witnesses $e^{\ast } = H_{\operatorname{\mathcal{E}}^{\dagger }_{C} \times \{ 0\} }$ as given by contravariant transport along $e$ (see Definition 5.2.2.14). Let $e_{L}: \operatorname{id}_{C} \rightarrow e$ and $e_{R}: \operatorname{id}_{C'} \rightarrow e$ denote the edges of $\operatorname{Tw}(\operatorname{\mathcal{C}})$ described in Example 8.1.3.6, and let $\widetilde{H}$ denote the product morphism
\[ \operatorname{\mathcal{E}}^{\dagger }_{C} \times \Delta ^1 \xrightarrow {H \times e_{R}} \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}). \]
Then the composition $T \circ \widetilde{H}$ can be regarded as a natural transformation from the functor $T_{C'} \circ e^{\ast }$ to $T_{e}$. For each object $X$ of the $\infty $-category $\operatorname{\mathcal{E}}^{\dagger }_{C}$, the restriction $H|_{ \{ X\} \times \Delta ^1 }$ is a $U^{\dagger }$-cartesian edge of $\operatorname{\mathcal{E}}^{\dagger }$. Using condition $(2)$ of Definition 8.6.1.1, we conclude that $(T \circ \widetilde{H})|_{ \{ X\} \times \Delta ^1 }$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ lying over the degenerate edge $\operatorname{id}_{C'}$ of $\operatorname{\mathcal{C}}$, and is therefore an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C'}$ (Proposition 5.1.4.11). Applying Theorem 4.4.4.4, we conclude that $T \circ \widetilde{H}$ is an isomorphism of functors from $T_{C'} \circ e^{\ast }$ to $T_{e}$.
We now prove $(b)$. Let $H'$ denote the composite map
\[ \operatorname{\mathcal{E}}^{\dagger }_{C} \times \Delta ^1 \xrightarrow {\operatorname{id}\times e_{L}} \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \xrightarrow {T} \operatorname{\mathcal{E}}, \]
We then have a commutative diagram
\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}^{\dagger }_{C} \times \Delta ^1 \ar [r]^-{H'} \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{ U} \\ \Delta ^1 \ar [r]^-{e} & \operatorname{\mathcal{C}}. } \]
Condition $(2)$ of Definition 8.6.1.1 guarantees that, for each object $X \in \operatorname{\mathcal{E}}^{\dagger }_{C}$, the restriction $H'|_{ \{ X\} \times \Delta ^1 }$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$. It follows that $H'$ determines an isomorphism of $T_{e} = H'|_{ \operatorname{\mathcal{E}}^{\dagger }_{C} \times \{ 1\} }$ with the composition $e_{!} \circ (H'|_{ \operatorname{\mathcal{E}}^{\dagger }_{C} \times \{ 0\} } ) = e_{!} \circ T_{C}$.
$\square$