hi thomas,

i am not managing to find time to think of this during the day and wise people make sure to be asleep at 2am but i am way too young for that ;)

i do think that there is more to the link between definability and comprehension than just my confusions. the reason is that the two of them are trying to say closely related things and there must be a way to spell it out, invariant under any mistakes that i could ever make.

lawvere said early on that categories could be used as the foundation of mathematics. eilenberg and maclane were shaking their heads about the crazy idea of sets without elements (as he recounted) but then, as we know, they invited him to write the introductory paper for la jolla proceedings. after that he went on: "the main foundational operation is comprehension. **how are categorical predicates (in hyperdoctrines) comprehended as categorical constructs?**" --- and he spelled out comprehension as the right adjoint. (yes, he used the fibrewise terminals and direct images to display the logical intuitions behind this particular adjunction in the foundations. but the construction is more general than that.)

benabou, on the other hand, says (i just looked up the paper): "In 1970 I realised the possibility of doing all of naive category theory, without sets, in the context of fibrations, and started work on proving that claim." and his naive category theory is the usual category theory, for which he wants to provide a non-set-theoretic categorical axiomatics. his main question was: "*how are categorical predicates (in fibrations) definable as categorical constructs?**.

"morally" (as they say in cambridge) the two of them are trying to do the same thing! there must be some truth in morality (contrary to all evidence :)))

the way definability is defined in your benabou notes, as far as i can tell in the middle of the night, seems to be saying that
* a subfibration CC>--->XX--P-->BB is definable
* when there is a cartesian functor XX--->Sub(BB)
** whose image is a subfibration SC>--->Sub(BB) such that
** the reflection XX/XX--->>BB/P (whose right adjoint makes P into fibration)
** restricts along the inclusion SC/P>--->BB/P
** to the reflection CC/XX--->>SC/P.

there is probably a better way to say all this. but the main point is that there is, i think, a bijective correspondence between
* definable subfibrations of XX--->BB and
* subfibrations of Sub(B)--->BB.

g'night and sorry about the typos ;)
-- dusko

On Tue, Jan 23, 2024 at 12:12 AM Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:

Dear Dusko,

I think in your mail you confuse small global sections and
definability of 1.

What I mean is the following. Let P : XX --> BB be a fibration of cats
with 1, i.e. P has a right adjoint right inverse 1.
Lawvere"s notion of comprehension means that 1 has a right adjoint
right inverse G. The counit eps_X : 1_{GX} --> X of 1 --| G at X has
the following universal property: for every f : 1_I --> X (over u : I --> PX)
there exists a unique \check{f} : I --> GX with eps_X \circ 1_{\check{f}} = f.
This is an instance local smallness for for P in the sense that GX = hom(1,X).

This is more general than Lawvere's notion of comprehension which
assumes that P has also internal sums in which case maps f : 1_I --> X
over u : I --> PX correspond uniquely to maps \coprod_u 1_I --> X.
But f also corresponds uniquely to \check{f} : I --> GX with
P(eps_X) \circ \check{f} = u .

But all this has nothing to do with definablity in the sense of Benabou.
But one may consider Id_BB as a full subfibration of P via 1. This being
definable in the sense of Benabou would mean that for every X in P(I)
there exists a greatest subobject m of I such that m^*X is terminal in
its fiber.

But notice that P(eps_X) is not monic for Lawvere comprehension as
considered above.
But for posetal fibrations P(eps_X) is always monic, of course.
Indeed for posetal fibrations having small global sections may be
thought of as a kind of comprehension. But for non-posetal fibrations P
the map P(eps_X) is better thiought of as the P(X)-indexed family whose
fiber at i \in PX is thought of as the "set of global elements of X_i".

Thomas