Understanding the Beck-Chevalley Condition

Question

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.

Answer 1

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)$.

The whole process is natural since every step is natural.