Re: **EXTERN** Re: small global sections vs definability of 1

[streicher@mathematik.tu-darmstadt.de]

Hi Dusko,

if you say that both local smallness and definability are formulated as
requirements that certain elementary fibrations are representable
fibrations are reprsentable then I agree.
Elementary fibrations are fibrations of posetal groupoids and
representable means that the total category of fibrations has a terminal
object.

Where I disagree is that local smallness can be formulated as a certain
subfibration being definable.

But, as I said already previously, a posetal fibration P : X --> B of cats
with 1 has comprehension if the subfibration 1 : Id --> P is definable.
Moreover, Lawvere comprehension means "small global elements" which in case
of a fibration of cc's is equivalent to local smallness in the sense of
Benabou.

Best wishes,
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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b