From a pragmatic point of view it certainly works to work with fibrations endowed with a (non-split) cleaving and arbitrary cartesian functors (not preserving these cleavings). And I think this solves David R.'s problem. It is also true that fibrations you consider always come equipped with some cleaving. Well, the fundamental fibration of a category BB with pullbacks only does if you assume BB being andowed with a choice of pullbacks. So from a pragmatic point of view choice is often needed just for restoring information you have deliberately forgotten. When speaking about arbitrary fibrations, of course, this information is not present and has to be assumed as given. But admitting strong choice principles allows one to remove this clutter from definitions and rather to restore them when needed. But this cleaning up has the unintended side effect of getting logically very strong. I have never seen any amazing consequence of AC for classes but maybe there are.

BTW Benabou himself put quite some emphasis on avoiding choice in his JSL paper. But in the practice of working with fibered categories you introduce cleavages whenever convenient. I did so in my notes and I guess so did Benabou in his various notes. This is no suprise in the light of the above discussion because it is simply convenient. In any case this issue does not influence the practice of working with fibered categories. There are just different ways of explaining this practice from a foundational point of view... Thomas PS In analysis you often apply number choice without saying. In very applied texts they use Skolem functions more often then existential quantifiers. But not for foundational reasons rather because they find it more intuitive. You really have to be a logician for having a problem with choice :-) ---------- 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