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 ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27