# 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$:


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.

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.