(I asked the same question here and got some helpful comments, but thought I'd re-ask in case I get a more direct response.)
This is a sort of reference request. Proposition B1.3.17 in Johnstone's Elephant reads:
Proposition 1.3.17 Let $\mathcal{S}$ and $\mathcal{T}$ be categories with pullbacks, $F \colon \mathcal{S} \rightarrow \mathcal{T}$ a functor having a right adjoint $R$, and $\Pi \colon \mathcal{C} \rightarrow \mathcal{T}$ a fibration. Then $F^* \Pi \colon F^* \mathcal{C} \rightarrow \mathcal{S}$ satisfies any comprehension scheme satisfied by $\Pi$.
I find the proof Johnstone offers very confusing (partly because it's very elliptical.) Does anyone know where this was originally proved? I haven't found the result in Benabou's writing (unless it's in the paper in French, referenced as [101] in Johnstone, which I cannot read) nor anywhere else. Is there another version of this proof in print? Or was Johnstone the first to prove this result in this generality?
Furthermore, if someone patient among you actually looks at the proof, could you possibly clarify this for me: What is the notation $\mathcal{T}^{\pi_0\mathcal{D}}$ supposed to describe ($\pi_0 \mathcal{D}$ is described as the "set of connected components of $\mathcal{D}$"? At first I suspected it was (collections of) connected diagrams in $\mathcal{T}$ - i.e. I interpreted as something like a component-wise $[\pi_0 \mathcal{D},\mathcal{T}]$ where the diagrams are sent to $\mathcal{T}$ via $\Pi$ (because of what Johnstone says right before the diagram, namely that "applying $\Pi$ to objects and morphisms of Rect($\mathcal{D},\mathcal{C}$) yields a functor Rect($\mathcal{D},\mathcal{C}) \rightarrow \mathcal{T}^{\pi_0 \mathcal{D}}$"- but then I cannot really make sense of what he says at the last sentence of the first full paragraph of pg. 278, for which interpreting it as the $\pi_0 \mathcal{D}$-fold product of $\mathcal{T}$ makes sense. Basically, what categories are we dealing with on the bottom square of the diagram on pg. 277?