In Higher Algebra Lemma 6.1.6.3, most of the proof is pretty straightforward, but after thinking I understood it all correctly, I realized I had a gap in my understanding.


Suppose we have a homotopy cartesian square of $\infty$-categories (the Lemma has these as Kan complexes, but I think this is irrelevant to my question here) $$\begin{matrix}X'&\xrightarrow{f'}&Y'\\ \downarrow^{g\_X}&&\downarrow^{g\_Y}\\X&\xrightarrow{f}&Y
\end{matrix}$$


and for simplicity, $C$ is an $\infty$-category with enough limits for $f^\*$ and $f'^\*$ to admit right adjoints.


In the proposition (which has more conditions, though they are irrelevant to this question), we want to see if the Beck-Chevalley transformation $$g^\*\_Yf\_\* \to f'\_\*f'^\*g\_Y^\*f\_\* \simeq f'\_\*g\_X^\*f^\*f\_\*\to f'\_\*g\_X^\*$$
is an is an equivalence.


Lurie suggests we prove this by pointwise evaluation on a functor $F:X\to C$ and an object $y$ of $Y'$ of the Beck-Chevalley transformation as the induced map $$\operatorname{lim}(F|X\times\_Y Y\_{g\_Y(y)/}) \to \operatorname{lim}(F|X'\times\_Y' Y'\_{y/}).$$


The trouble is, it's not clear to me why this map, induced by the diagram


$$\begin{matrix} X' & \to & Y'& \leftarrow & Y'\_{y/}\\
\downarrow &&\downarrow&&\downarrow\\
X&\to&Y&\leftarrow&Y\_{g\_Y(y)/}
\end{matrix}$$


is homotopic to the component of the Beck-Chevalley map at $F$ and $y$.


I tried evaluating the intermediate terms, but they are huge and messy, and I can't find a reference showing that they are indeed homotopic.


Is the proof easy? Does anybody have a reference?


Edit: I think this is related to the proof of 4.3.3 in [Ambidexterity paper](http://www.math.harvard.edu/~lurie/papers/Ambidexterity.pdf) of Lurie and Hopkins. It looks like he uses cartesianness of the square there to identify (the adjuncts of) these maps (in the dual case of left Kan extensions), so I have added a cartesianness condition. 



Pointwise evaluation of the Beck-Chevalley map in $\infty$-categories
The Beck-Chevalley transformation $g^\*\_Y f\_\* \rightarrow f'\_\* g^\*\_X$ from a square of $\infty$-groupoids as above is an equivalence iff it's an equivalence when evaluated at every point of $Y'$, i.e. iff the transformation $p^\*g^\*\_Y f\_\* \rightarrow p^\*f'\_\* g^\*\_X$ is an equivalence for all maps $p : \* \rightarrow Y'$. Consider the homotopy pullback square
$$\begin{matrix} 
F & \xrightarrow{r} & \*\\
\downarrow^{q} & &\downarrow^{p}\\
X' & \xrightarrow{f'} & Y'.
\end{matrix}$$
The corresponding Beck-Chevalley transformation $p^\*f'\_\* \rightarrow r\_{\*}q^\*$ is clearly an equivalence - this just says that $f'\_\*$ evaluated at $p$ is the limit over the homotopy fibre $F$. Indeed, the Beck-Chevalley transformation for a square of this form (with $\*$ in the upper right corner) is an equivalence (for all targets) iff the square is Cartesian. By the naturality of Beck-Chevalley transformations, the composite $(g\_Y p)^\* f\_\* \simeq p^\*g^\*\_Y f\_\* \rightarrow p^\*f'\_\* g^\*\_X \rightarrow r\_{\*}q^\*g^\*\_X \simeq r\_\*(g\_X q)^\*$ is equivalent to the Beck-Chevalley transformation for the composite square
$$\begin{matrix} 
F & \xrightarrow{r} & \*\\
\downarrow^{g\_X q} & &\downarrow^{g\_Y p}\\
X & \xrightarrow{f} & Y
\end{matrix}$$
(this follows from the adjunction identities). This transformation is again an equivalence if this square is Cartesian. So by 2-of-3 the original transformation is an equivalence at every $p$ if the square 
$$\begin{matrix} 
X' & \xrightarrow{f'} & Y'\\
\downarrow^{g\_X} & &\downarrow^{g\_Y}\\
X & \xrightarrow{f} & Y
\end{matrix}$$
is Cartesian. (And conversely, this square is Cartesian if the Beck-Chevalley transformation is always invertible (or if it is invertible for functors to spaces).)


For $\infty$-categories you have to replace the homotopy fibre square with the lax pullback square
$$\begin{matrix} 
X'\_{p/} & \to & \*\\
\downarrow & \Rightarrow &\downarrow\\
X' & \xrightarrow{f'} & Y'
\end{matrix}$$
(which commutes up to a natural transformation in a direction I'm too lazy to work out) - the Beck-Chevalley transformation for this gives the limit formula for a right Kan extension. I'm not aware of a nice criterion for a square of ($\infty$-)categories to have an invertible Beck-Chevalley transformation, but the same argument shows that it can be checked pointwise.


