# Understanding the Beck-Chevalley condition

Having opened the black box of Beck's monadicity theorem, I would now like to do the same for monadic descent. While probing around I keep encountering the Beck-Chevalley condition.

Unfortunately, the nlab entry is way above my head. I want to understand the intuitive idea behind this condition in some concrete cases but I don't even know how to start.

What is the intuitive meaning of the Beck-Chevalley condition, either from a geometric perspective or from a logical one? (I don't know type theory.)

$\require{AMScd}$ When you do algebraic geometry, you can consider diagrams like $$\begin{CD} X @>f>> A\\ @VgVV \\ B \end{CD}$$ where $X,A,B$ are spaces and $g,f$ maps thereof. It is fairly natural to think these as "generalized functions" between $A$ and $B$. They are in fact called "correspondences" between $A$ and $B$, and they organize in a category that contains your category of spaces in (actually two) canonical way(s).
Morally, these guys correspond to "pull-push" functors like $g_*f^* : D(A)\to D(B)$. But there is a subtlety: in order for this to be a well-defined (bi)category, you must specify coherence conditions on a composition law: the most natural thing to do, given a diagram $$\begin{CD} @. X @>f>> A\\ @. @VgVV \\ Y @>h>> B\\ @VkVV\\ C \end{CD}$$ is to complete it to a pullback $$\begin{CD} P @>q>> X @>f>> A\\ @VpVV @VgVV \\ Y @>h>> B\\ @VkVV\\ C \end{CD}$$ Notice that you have two seemingly different ways to read your composition, now: the first, as $(kp)_*(fq)^* = k_* p_* q^* f^*$ and the second as $k_* h^* g_* f^*$. When will these two be equal (or rather, canonically isomorphic)?
Let $\pi_! \dashv \pi^*$ where $\pi^*$ is the inverse image of projection, called the weakening functor, and $\pi_!$ is the direct image and corresponds to existential quantification, i.e. $\pi_{!,B}(x:A,y:B\vdash P(x,y))$ corresponds to $x:A\vdash\exists y:B.P(x,y)$. The inverse image $\pi_B^*(x:A\vdash P(x))$ corresponds to $x:A,y:B\vdash P(x)$, hence "weakening". Now the problem is there are two ways to get $x:A\vdash \exists y:B.R(\sigma(x),y)$ starting from $x:A,y:B\vdash R(x,y)$. You could first existentially quantify getting $x:A\vdash\exists y:B.R(x,y)$ and then substitute, or you could first substitute $x:A,y:B\vdash R(\sigma(x),y)$ and then existentially quantify. The pullback square in the base is $$\require{AMScd} \begin{CD} A\stackrel{\times}{{}_{\pi_B,\sigma}} B @>\hat\pi_B>> A\\ @V\hat\sigma VV @VV\sigma V \\ A\times B @>\pi_B>> A \end{CD}$$ and we get $\hat\pi_{!,B}\circ\hat\sigma^* \to \sigma^*\circ\pi_{!,B}$. The natural transformation arises as described here and in this case looks like $$\cfrac{\cfrac{ x:A\vdash\exists y:B.[\sigma(x)/x,y/y]_{x,y}R(x,y)} {x:A\vdash\exists y:B.[\sigma(x)/x,y/y]_{x,y}[x/x]_{x,y}\exists w:B.R(x,w)}}{ \cfrac{x:A\vdash \exists y:B.[x/x]_{x,y}[\sigma(x)/x]_{x}\exists w:B.R(x,w)}{ x:A\vdash[\sigma(x)/x]_{x}\exists w:B.R(x,w)}}$$ where I'm using e.g. $[\sigma(x)/x]_{x,y}$ as a substitution replacing $x$ with $\sigma(x)$ in terms of the variables $x$, and $y$. That the above implication should be an equivalence is the Beck-Chevalley condition.