i did, of course, miss something (as i suspected before hitting return, but didn't resist :)
but it seems that fixing the error makes the benabou/lawvere link even nicer. (even if i am still missing something i am sure that the link is there.)
the one-to-one correspondence between definable subfibrations of E---->B and the "comprehensions" E---->Sub(B) stands. the claim that the subfibration C---->B is obtained by pullback is wrong, because we don't want to pull back along the "truth" into Sub(B) but along the "comprehension".
remember how lawvere defined comprehension of the bifibration E---->B to be (in equivalent to hyperdoctrines) the right adjoint of the cartesian functor Arr(B)---->E mapping (i--f-->j) to f_!(top_i). [[i even introduced Arr(B) in the previous message but oversimplified and didn't use it.]]
now i can of course restrict that functor to Sub(B)---->E. a definable subfibration C of E, determines a right adjoint E---->Sub(B) and the adjunction localizes on C.
how can i say this for fibrations, without using the direct images? well (now i write Arr(E) as E/E and B/P is the comma into P) E--P-->B is a fibration if and only if the induced functor E/E---->B/P is a reflection (the cartesian liftings induce a right adjoint right splitting). a subcategory C of E is a definable subfibration of P if and only E/E---->B/P restricts to C/E---->Sub/P. i think.
apologies that i am thinking so much in public, but there is no shortage of private thinking and there is a shortage of public thinking and we should all think together how to bring lawvere and benabou together :)
-- dusko