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

On Mon, Jan 22, 2024 at 3:05 PM Dusko Pavlovic <duskgoo@gmail.com> wrote:

> as we are talking about lawvere's and benabou's nachlasse, it occurred to
> me to ask what would benabou's definability be in lawvere's terms. maybe
> they both knew this and maybe other people do, but i hope it doesn't hurt
> to spell it out.
>
> let B be a category with pullbacks so we have the fibrations
> Arr(B)--Cod-->B and
> Sub(B)--Cod-->B,
> where Arr(B) is the category of arrows and Sub(B) is the category of
> subobjects. the cartesian functors B>--Ids-->Sub(B) and B>--Ids-->Arr(B)
> are the right adjoints.
>
> Prop. B>--Ids-->Sub(B) is the classifier of definable subfibrations. more
> precisely, for any fibration E--P-->B and a subfibration C>---->E here is a
> unique cartesian functor E--c-->Sub(B) such that the fibration C---->B is
> the pullback of c along B>--Ids-->Sub(B).
>
> i did check this, but i didn't check it twice, so i may still be missing
> something.
>
> -- dusko
>
> On Mon, Jan 22, 2024 at 10:00 AM Francis Borceux <
> francis.borceux@uclouvain.be> wrote:
>
>>
>> Sorry, and thanks to Jon for noticing the slip of terminology in my mail.
>>
>> Indeed, Bénabou was insisting on the importance of his notion of
>> definability.
>>
>> Francis
>>
>> ***********************************
>> Francis Borceux
>> 6 rue François
>> 1490 Court-Saint-Étienne
>> Belgique
>> Fixe: +32(0)10614205
>> Mobile: +32(0)478390328
>>
>>
>> ----------
>>
>> You're receiving this message because you're a member of the Categories
>> mailing list group from Macquarie University.
>>
>> Leave group:
>>
>> https://protect-au.mimecast.com/s/JhEqC5QP8ySGq6xkfzFqDC?domain=outlook.office365.com
>>
>