Re: Fibrewise opposite fibration

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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