Understanding the Beck-Chevalley Condition

I've been reading through Bart Jacobs' "Categorical Logic and Type Theory", and lemma 1.8.9 has me stumped. The lemma is stated as follows:

Let $$p : \mathbb E \to \mathbb B$$ and $$q : \mathbb D \to \mathbb B$$ be fibrations and let $$H : \mathbb E \to \mathbb D$$ be a fibred functor. This functor $$H$$ has a fibred left adjoint if and only if both

(a) For each object $$I \in \mathbb B$$ the functor $$H_I : \mathbb E_I \to \mathbb D_I$$ restricted to the fibres over $$I$$ has a left adjoint $$K(I)$$

(b) The Beck-Chevalley Condition holds, i.e. for every map $$u : I \to J$$ in $$\mathbb B$$ and for every pair of reindexing functors $$\mathbb E_J \overset{u^*}{\longrightarrow} \mathbb E_I$$ and $$\mathbb D_J \overset{u^\#}{\longrightarrow} \mathbb D_I$$, the canonical natural transformation $$K(I)u^\# \Rightarrow u^* K(J)$$ is an isomorphism.

What does the canonical natural transformation $$K(I)u^\# \Rightarrow u^* K(J)$$ refer to? I was having a lot of fun reading this book. However, since the Beck-Chevalley condition is used throughout the rest of the book, this particular lemma has become a road block.

I'm not sure if this is considered a research level question, but I don't know where else to ask this.

So we need to construct a natural transformation $$\phi : K(I)u^\# \Rightarrow u^*(K(J))$$, which are functors from $$D_J$$ to $$E_I$$. So for every $$d \in D_J$$ we need a morphism $$K(I)(u^\#(d)) \to u^*(K(J)(d))$$ in $$E_I$$.
1. Since $$K(I) \dashv H(I)$$, this is equivalent to constructing a morphism $$u^\#(d) \to H(I)(u^*(K(J)(d)))$$ in $$E_J$$.
2. Now since $$H$$ is a fibred functor, $$H(I)(u^*(e)) \cong u^\#(H(J)(e))$$ for any $$e$$ so by composition with this isomorphism it is sufficient to construct a morphism $$u^\#(d) \to u^\#(H(J)(K(J)(d)))$$.
3. $$u^\#$$ is a functor so it is sufficient to construct a morphism $$d \to H(J)(K(J)(d))$$
4. So we can just use the unit of the adjunction $$K(J) \dashv H(J)$$.
• Oh, so that's what Jacobs is talking about in the text directly below the lemma. I tried to reverse engineer that, but I got stuck on the natural isomorphism $𝐻(𝐼)𝑢^*≅𝑢^{\#}𝐻(J)$; I couldn't figure out where it came from, but now I see that it's just an appeal to Cartesianness. Your step-by-step explanation was much easier to follow. Shouldn't H(I)K(I) in steps 2,3,and 4 be H(J)K(J)? Commented May 18, 2019 at 19:09