Proof of Theorem 7.4.1.1.
Suppose we are given a pullback diagram of small simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleleft }, } \]
where $U$ and $\overline{U}$ are cocartesian fibrations. Assume first that the restriction map
\[ \theta : \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \]
is an equivalence of $\infty $-categories; we wish to show that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$.
Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$, where $\operatorname{\mathcal{C}}'$ is an $\infty $-category. Note that the induced map $\operatorname{\mathcal{C}}^{\triangleleft } \hookrightarrow \operatorname{\mathcal{C}}'^{\triangleleft }$ is also inner anodyne (Proposition 4.3.6.4). Applying Corollary 5.6.7.3, we can realize $\overline{U}$ as the pullback of a cocartesian fibration of $\infty $-categories $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleleft }$. Set $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{ \operatorname{\mathcal{C}}'^{\triangleleft } } \overline{\operatorname{\mathcal{E}}}'$, so that we have a commutative diagram of restriction functors
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}'^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}'^{\triangleleft }, \overline{\operatorname{\mathcal{E}}}' ) \ar [r]^-{ \theta ' } \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}' }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{E}}' ) \ar [d] \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^-{\theta } & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}), } \]
where the vertical maps are trivial Kan fibrations (Proposition 5.3.1.21). It follows that $\theta '$ is also an equivalence of $\infty $-categories.
Using Corollary 5.6.5.11, we can extend $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ to a functor
\[ \operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleleft } }: \operatorname{\mathcal{C}}'^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}} \]
which is a covariant transport representation for the cocartesian fibration $\overline{U}'$. Since $\operatorname{\mathcal{C}}'$ is an $\infty $-category, Proposition 7.4.2.1 guarantees that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleleft } }$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$. Since the inclusion map $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$ is left cofinal (Proposition 7.2.1.3), it follows that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is also a limit diagram in $\operatorname{\mathcal{QC}}$.
We now prove the converse. Assume that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$; we wish to show that $\theta $ is an equivalence of $\infty $-categories. Using Proposition 7.4.1.6, we can choose another pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \operatorname{\mathcal{E}}^{+} \ar [d]^{ U^{+} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleleft }, } \]
where $U^{+}$ is a cocartesian fibration for which the restriction map $\theta ^{+}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{E}}^{+} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}^{+} )$ is an equivalence of $\infty $-categories. Applying Corollary 5.6.5.11, we see that $U^{+}$ admits a covariant transport representation $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ satisfying $(\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleleft } })|_{\operatorname{\mathcal{C}}} = (\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } })|_{\operatorname{\mathcal{C}}}$. The first part of the proof shows that $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is also a limit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$, and is therefore isomorphic to $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{QC}})$. Applying Theorem 5.6.0.2, we deduce that there exists a morphism $F: \overline{\operatorname{\mathcal{E}}} \rightarrow \overline{\operatorname{\mathcal{E}}}^{+}$ which is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}^{\triangleleft }$. We have a commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{E}}^{+} ) \ar [r]^-{ \theta ^{+} } \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}' ) \ar [d] \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^-{\theta } & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}), } \]
where the vertical maps are given by precomposition with $F$ and are therefore equivalences of $\infty $-categories. Since $\theta ^{+}$ is an equivalence of $\infty $-categories, it follows that $\theta $ is also an equivalence of $\infty $-categories.
$\square$