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

Proposition 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, 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:


The functor $T_{e}$ is isomorphic to the composition $T_{C'} \circ e^{\ast }$.


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 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, 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, 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 Applying Theorem, 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 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$