[sorry, i always lag behind.]

a global well-order assumption is not a conservative extension even of ZFC.
it would make all models of computation extensional. it is also not a
conservative extension of the nice non-ZF universes we like these days,
including categorical, for basically the same reason.

my earlier point was that, since we live among computers, the assumption of
local well-ordering seems unavoidable, sooner or later.  for the simple
reason that all data and code are well-ordered as binaries. but the
ordering is not a property, either global or local, but structure. we keep
reordering things whenever we write a program. imposing a global ordering
structure would require deciding what is what: identifying the intensional
and the extensional equality. extensionally :)

you are probably right that all this is a sort of a religious war. or maybe
not a war, but rather a theological dispute. but note that theologians
considered it to be self-evident that they were the bearers of the torch of
logical truth. just like we.

if we assume that the world is built of sets, like we were taught in math
101, then assuming well-order is indeed questionable in all kinds of ways,
burdensome practically, and zermelo's solution to package it behind a big
quantifier is a convenient solution.

but while discussons whether the world is built of sets as the simplest
foundation of everything might be interesting, or not, programmers tend to
ignore them and only use sets when pedagogically unavoidable. the reason is
that all types in their world are well-ordered AND that transitioning to
sets and cardinalities is still as just costly as it was for cantor. so the
math that runs in the computers that we use to exchange these messages,
discuss foundations, and make calls home, tends to be built on well-ordered
types --- which we reorder and reprogram whenever needed. intensionally :)

2c
-- dusko


On Mon, Feb 12, 2024 at 6:56 PM Nath Rao <khazanarao@gmail.com> wrote:

> [This no longer about how to define fibrewise opposite fibration, so may
> be it is time t change the subject line.]
>
> IMHO, this seems to be more like a religious war. In "mathematics in the
> small", local axiom of choice allows us to choose representatives only
> when needed. So we are grew up believing that putting things in the
> definition that are not preserved by morphisms is "not done" (the
> religious dogma) . But them we run up against issues when we try to do
> the same thing in "mathematics in the large", and either ignore the
> problem or argue endlessly about how to solve it.
>
> Also, if are willing to assume that every set comes with a
> well-ordering, why not assume a global well-ordering and be done with
> it? [If I am going to use universes anyway, it seems to be trivial to do
> this, as long as I live inside a fixed universe in any given proof.] For
> ZFC, global choice is a conservative extension. Not being a logician, am
> not sure, but perhaps it can be shown for global choice is a
> conservative extension of local choice of 'all suitable set theories'.
> Then we can do global choice with no qualms.
>
> Regards
> Nath Rao
>
>
>
>
>
> ----------
>
> You're receiving this message because you're a member of the Categories
> mailing list group from Macquarie University.
>
> Leave group:
>
> https://url.au.m.mimecastprotect.com/s/IRyOC1WLjwsyM5vLTL23r1?domain=outlook.office365.com
>