Re: Fibrewise opposite fibration

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

Hi Jon,

I didn't want to say that HoTT just wants to avoid global choice.

I also said that for most weak equivalences you meet the pseudoinverse
can be constructed. But for establishing this in general you need
global choice. Just look at the proof in MacLane or similar textbooks.

Or where do they prove that the assumption of a pseudo inverse is a
conservative extension without having a pseudo inverse at hand?

I do not believe that big choice is needed in down to earth mathematics.
I agree when applying general results to particular situations these
general principles can be mostly (always? but why?) eliminated.
But I do not know of any argument that for all functors between
Grothendieck toposes preserving finite limits and small colimits entails
the existence of a right adjoint.

These (unintentionally) strong principle have been introduced just for
convenience and later it has been found out that they have suprising
consequences.

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