Re: Fibrewise opposite fibration

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

> In fact, the reference shows that global choice really is inconsistent in HoTT. Univalence asserts (among other things) that all operations on the universe (even the universe of sets) are "natural" under equivalences, but a global choice operator cannot be natural in this sense.

Thanks for this clarification!

One needs global choice in CT for establishing that full and faithful
functors which are essentially surjective are actually categorical
equivalences.
In practice you just have the stronger notion.

In my eyes HoTT is an attempt to live with the weaker notion.

In basic topos theory global choice is assumed when identifying
inverse images of geometric morphisms with cocontinuous functors
preserving finite limits. Therefore, I never believed that you can do
topos theory in a weak meta theory without strong choice principles.
At least not the way it is done in the traditional texts.

Maybe HoTT is an attempt to avoid these hidden uses of strong choice...
But it is a mystery to me why people have overlooked that they were
using very strong choice principle. Well, it is the usual difference between
ideology and practice as it seems to me...

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