Kerodon

Corollary 8.6.1.6. Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration having homotopy transport representation $\operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ (Construction 5.2.5.2), and let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be a cartesian fibration having homotopy transport representation $\operatorname{hTr}_{ \operatorname{\mathcal{E}}^{\dagger } / \operatorname{\mathcal{C}}^{\operatorname{op}} }: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ (Construction 5.2.5.7). If $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ exhibits $U^{\dagger }$ as a cartesian conjugate of $U$, then $T$ induces an isomorphism of functors $\operatorname{hTr}_{\operatorname{\mathcal{E}}^{\dagger } / \operatorname{\mathcal{C}}^{\operatorname{op}}} \xrightarrow {\sim } \operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}}$, carrying each vertex $C \in \operatorname{\mathcal{C}}$ to (the isomorphism class of) the equivalence $T_{C}: \operatorname{\mathcal{E}}^{\dagger }_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$.