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 incredibly 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?
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}$"? I suspected it was (collections of) connected diagrams in $\mathcal{T}$ - i.e. I interpreted as something like $[\pi_0 \mathcal{D},\mathcal{T}]$ - but then I cannot really make sense of what he says at the last sentence of the first full paragraph of pg. 278. Basically, what categories are we dealing with on the bottom square of the diagram on pg. 277?