Kerodon

Remark 5.2.5.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories, let $f: C \rightarrow D$ be a morphism of $\operatorname{\mathcal{C}}$, and let $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ be given by covariant transport along $f$. If $f$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$, then $f_{!}$ is an equivalence of $\infty $-categories. This follows from the observation that the homotopy transport functor $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ carries isomorphisms to isomorphisms.