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=6bf90c14-94d1-45b7-a0b5-9dd447734d27