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

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?

-
"Elliptical" appears to have two contradictory meanings (I had to look these up): the first meaning is "so condensed as to be difficult to understand" and the second meaning is "long-winded." Which meaning did you intend? – Qiaochu Yuan Aug 11 '12 at 20:34
@Qiaochu Haha, you are right - I meant the former, i.e. so condensed as to make it difficult to understand. – Chuck Aug 11 '12 at 22:36
If $\mathbb{C}$ is an fibred/indexed category then $\mathbb{C}^I$ refers to the fibre of $\mathbb{C}$ over the object $I$. However, since $\pi_0 \mathcal{D}$ is just a set and $\mathcal{T}$ is an ordinary category, I suspect $\mathcal{T}^{\pi_0 \mathcal{D}}$ means the $\pi_0 \mathcal{D}$-fold product of $\mathcal{T}$ as an ordinary category. – Zhen Lin Aug 12 '12 at 2:44
You may want to look at Streicher's notes on fibred categories, particular Chapters 12 and 13. – Zhen Lin Aug 12 '12 at 2:51
@ZhenLin Yes I do have Streicher's notes which are generally very helpful. He proves this result for the specific property of local smallness (Lemma 13.3) but not the much more general result that Johnstone proves. Of course reading Streicher more carefully, he seems to imply (top of pg. 47, just before the proof of 13.3) that Benabou also only proved such results for specific properties. So it seems Johnstone was the first to present this result in this general form - and therefore that this is the only proof that we have... – Chuck Aug 13 '12 at 16:18