About the definition of coproducts of a cloven fibration Let $F : \mathcal X \to \mathcal A$ be a cloven fibration and let the following be a pullback square in $\mathcal A$:
$$\newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex}
\newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex}
\newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}}
\begin{array}{c}
A & \ra{f} & B\\
\da{a} & & \da{b}\\
A' & \ras{f'} & B'\\
\end{array} %this is borrowed from http://meta.math.stackexchange.com/questions/2324/how-to-draw-a-commutative-diagram$$
Then, according for example to B. Jacobs "Categorical Logic and Type Theory" and other sources, the square has the Beck-Chevalley property if 'the canonical natural transformation $\Sigma_f \circ a^* \to b^*\circ \Sigma_{f'}$ is an isomorphism'. Here $f^*$ ($\Sigma_f$) is (co-) reindexing along $f$. This property comes up in the definition of "$F$ has coproducts".

What is this canonical natural transformation explicitly?

Apparently, this is  blatantly obvious but I don't see it.
 A: The nLab page on the Beck-Chevalley condition is good.  The pieces of data we need are that $\Sigma_f \dashv f^*$ and similarly $\Sigma_{f'} \dashv f'^*$.  Ignoring that the above commutative diagram is a pullback diagram, we get from it
$$\require{AMScd}
\begin{CD}
\mathcal{X}_A @<f^*<< \mathcal{X}_B \\
@Aa^*A\qquad \cong A @AAb^*A \\
\mathcal{X}_{A'} @<<f'^*< \mathcal{X}_{B'}
\end{CD}$$
which commutes up to isomorphism.  This can be viewed as a square in the double category of adjunctions, and, as the Beck-Chevalley page states, the notion of mates (or conjugates) gives exactly the "canonical transformation" given the above diagram.  Explicitly, this is the arrow $$\begin{CD}
\Sigma_f \circ a^* @>\Sigma_fa^*\eta>> \Sigma_f \circ a^*\circ f'^*\circ \Sigma_{f'}@>\cong>> \Sigma_f\circ f^*\circ b^*\circ\Sigma_{f'} @>\varepsilon_{b^*\Sigma_{f'}}>> b^* \circ \Sigma_{f'}
\end{CD}$$ where the $\eta$ is the unit of the $\Sigma_{f'}\dashv f'^*$ adjunction and the $\varepsilon$ is the counit of the $\Sigma_f \dashv f^*$ adjunction.  All of this applies for arbitrary adjunctions in an arbitrary 2-category.  The Beck-Chevalley condition simply states that if the above (pseudo-)commutative square is the image of a pullback square, then the above natural transformation is an isomorphism.
The nLab page also has a good description of what the Beck-Chevalley condition means in a logic/type theory context, namely that substitution commutes with dependent sum formation.
