$p\circ q_{K^\lhd}:I\times K^\lhd\to K^\lhd$ is just the projection, so $p\circ q_{K^\lhd}$ is a Cartesian fibration; and by [@Lurie:2009un Proposition 4.2.2.4.] $\bar X^{q_{K^\lhd}/}\to K^\lhd$ is a coCartesian fibration classified by $(\bar p')^{q/}:({K})^\lhd \to {{\mathscr{C}\mathrm{at}}}_\infty$. In particular, the fibre of $\bar X^{q_{K^\lhd}/}$ over any $k\in K^\lhd$ may be identified with the undercategory $\big(\bar p'(k)\big)^{\pi_k\circ q/}$ (cf. [@Lurie:2009un § 4.2.2]). Let $X=\bar X\times_{K^\lhd} K$, and $q_{K}=q_{K^\lhd}\rvert_{I\times K}:I\times K\to X$. Then $\bar X^{q_{K^\lhd}/}\times_{K^\lhd} K\to K$ is canonically isomorphic to $X^{q_K/}\to K$. Consequently, by [@Lurie:2009un Proposition 3.3.3.1], it suffices to show that whenever

$$\label{eq:thetaequiv}\theta:{\operatorname}{Fun}_{K^\lhd}^{{\operatorname}{coCart}}(K^\lhd,\bar X)\to {\operatorname}{Fun}_{K}^{{\operatorname}{coCart}}(K,X)$$

is an equivalence of $\infty$-categories, so is $$\label{eq:thetaqequiv}{\operatorname}{Fun}_{K^\lhd}^{{\operatorname}{coCart}}(K^\lhd,\bar X^{q_{K^\lhd/}})\to {\operatorname}{Fun}_{K}^{{\operatorname}{coCart}}(K^\sharp,X^{q_K/}).$$

Using the identification $(I\times {K^\lhd})\diamond_{K^\lhd} (\Delta^n\times {K^\lhd})\cong (I\diamond \Delta^n)\times {K^\lhd}$, one sees that the $n$ simplices of ${\operatorname}{Fun}_{K^\lhd}^{{\operatorname}{coCart}}(K^\lhd,\bar X^{q_{K^\lhd/}})$ are lifting diagrams of the form $$\protect\tikz{
\node (m-1-1) at (0,2) {$I\times {K^\lhd}$};
\node (m-1-2) at (3,2) {$\bar X$};
\node (m-2-1) at (0,0) {$(I\diamond \Delta^n)\times {K^\lhd}$};
\node (m-2-2) at (3,0) {${K^\lhd}$};
        \draw[->] (m-1-1) -- node {$q_{K^\lhd}$} (m-1-2);
    \draw[right hook->] (m-1-1) --  (m-2-1);
    \draw[->] (m-1-2) -- node {$p$} (m-2-2);
    \draw[->] (m-2-1) -- (m-2-2);
    \draw[dashed,->] (m-2-1) -- node {$\sigma$}  (m-1-2);
}$$ such that for each vertex $v$ of $I\diamond \Delta^n$, the restriction $\sigma\rvert_{\{v\}\times {K^\lhd}}:{K^\lhd}\to \bar X$ is coCartesian. Thus, ${\operatorname}{Fun}_{K^\lhd}^{{\operatorname}{coCart}}(K^\lhd,\bar X^{q_{K^\lhd/}})\cong \big({\operatorname}{Fun}_{K^\lhd}^{{\operatorname}{coCart}}({K^\lhd},\bar 