Re: Fibrewise opposite fibration

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

Dear David and Jon,

when constructing the opposite of a fibrations one usually takes quotients.
But isn't that harmless in topos logic since after all toposes have
quotient types.
However, when doing fibered categories one hardly ever studies only a
finite number of those but has to quantify over them. So when
proceeding formally one has to adopt some universes be they Grothendieck
or type-theoretic in nature.

Most constructions are easier on the fibered side. Taking the opposite
of a fibration is the only example I know which is a bit easier on the
indexed side.
But think of facts like closure of fibrations inder composition. That
is sort of impossible to express on the indexed side.

Of course, for split fibrations things are easier. One obtains fibered
categories and cartesian functors by freely inverting split cartesian
functors that are fiberwise ordinary equivalences. The spotted problem
with the op-construction is thus not unexpected.

Moreover, it is the only thing which is easier on the indexed side. I
rather find it surprising that most things are easier on the fibered side.
Technically at least. And for intuitions and motivation it is quite ok
to work on the indexed side.

It is also ok to choose cleavages when this allows one to express
things in a more intuitive way.

Thomas

PS Maybe the following metaphor is helpful. In topos theory one
performs some arguments in the internal logic and others externally
depending on what appears as more easy. But the external reasoning is
more powerful. For example one cannot express internally something
like well pointedness.

For indexed vs fibered I rather have the impression that fibered is
more flexible. At least emprirically. One usually has no problem to
reformulate indexed as fibered. The other way is less evident as
exemplified by closure of fibrations under composition.



----------

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