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.


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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.