# Where else has Proposition B1.3.17 in the Elephant been proved?

(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?

-
I haven't been through this, but here's my guess as to what the notation means. (I assume that D is a category.) Every category D has a set of connected-components: it's the set of equivalence classes of the equivalence relation ~ on ob(D) generated by x~y whenever there exists a map x --> y. So I guess T^{pi_0 D} is the product of (pi_0 D) copies of T, as you say in your penultimate sentence. – Tom Leinster Aug 13 '12 at 21:26
(Sorry, I guess I should have said "Every small category D", or something. Anyway, that doesn't seem to be the issue here.) – Tom Leinster Aug 13 '12 at 21:51
@Tom Leinster Yes $\mathcal{D}$ in this case is a finite category, so that's fine. – Chuck Aug 14 '12 at 1:38
What is reference [101], for those without the Elephant at hand? – David Roberts Aug 14 '12 at 3:07
@David Roberts "Fibrations Petites et localement petites", J. Benabou C. R. Acad. Sci. Paris 281 (1975) – Chuck Aug 14 '12 at 14:29