Re: Fibrewise opposite fibration

["Jon Sterling" <jon@jonmsterling.com>]

Hi Thomas,

I think I see what you mean about global choice in classical math, but I don't think I agree overall. Things like connecting f.f.+e.s.o functors to equivalences in classical math do not require global choice when stated in the way that a careful classical mathematician understands (or is supposed to understand) them.

The statement is "There exists a mapping that takes any f.f.+e.s.o F : C -> D functor to a functor G : D -> F together with natural isomorphisms GF=1 and FG=1". This statement follows from "local" choice easily without making any global choices. I understand that you need global choice for this claimed function to form a 'definitional extension' of ZFC, but that is simply not what is meant by the original claim; it is for this reason that the practical formalisation of mathematics in ZFC emphasises consecutive conservative extensions and not only definitional extensions. Avoiding this distinction is one of the reasons that some people (like Hilbert and Bourbaki) have introduced global choice, but I must emphasise that essentially all the theorems of classical mathematics also work fine with only local choice. This is because the ground statements of classical mathematics are always propositional: when we want to introduce a construction, we describe the specification of that construction by means of a predicate, and then say that there exists something satisfying that predicate. After this, we work with an arbitrary thing satisfying that specification.

Likewise I do not agree with the discussion of geometric morphisms, for reasons that are identical to what I have mentioned above regarding weak and strong equivalences of categories.

For these reasons, I personally would not think of HoTT as an attempt to avoid hidden uses of strong/global choice, because the rest of classical mathematics (with the exception of Bourbaki) also does a perfectly fine job of avoiding global choice. (I'm not arguing against the convenience and utility of global choice though.)

Best,
Jon


On Tue, Feb 13, 2024, at 11:38 AM, Thomas Streicher wrote:
>> 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