Re: Fibrewise opposite fibration

[Dusko Pavlovic <duskgoo@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 6818 bytes --]

it occurs to me that i have been preaching the helpfulness of the
well-ordering of all data in the world, as demonstrated by its utility to
the programmers --- and i totally forgot to mention its utility as a
*categorical structure*!!  i forgot to plug my own work which provides the
categorical underpinning for the well-ordering sermon...

so we all love the **cartesian closed categories**, characterized by the
adjunction
CC(XxA,B) ~ CC(X, A=>B)           (*)

but the cccs are *extensional* universes, corresponding to the extensional
type theories. if we want to capture the world with actual programs, say in
a programming language P, then we have just a family of X-natural
surjections
CC(XxA,B) <<--- CC(X, P)             (#)
the surjections say that every computably X-indexed family of computable
functions from A to B can be programmed by a computably X-indexed family of
programs in P. since computable functions don't always halt, we cannot
avoid at least the computational effect of nontermination, and the AxB is
not a product but a tensor, say from a commutative computational monad.
such (symmetric) monoidal categories with a "programming language" type P
and natural surjections (#) is what i called *monoidal computers*, because
you can program everything using (#), without ever saying anything else
about the programming language. it is turing complete. it's all spelled out
in my book.

but the snag is that (*) is a *property* of a category, whereas (#) is a
structure. a category can be cartesian closed in only one way, but it can
be a monoidal computer in many ways. one is tempted to say that this is
unavoidable since the CT thesis leaves us with many models of computation
and infinitely many unnatural isomorphisms between any two.

**** enter the well-order ****

IF you remember that programming languages are well-ordered, and assume
that the type P carries a well-ordering,
THEN (#) becomes a *property*. a monoidal category CC can have at most one
well-ordered type P with (#), up to isomorphism.

the nices thing is that you prove this by spelling out what came to be
called the cantor-bernstein theorem, but in cantor's way: using the
well-order. (dedekind discouraged publishing this because the well-ordering
of the reals was cantor's by far the deadliest mortal sin. even now, to
really keep the reals well-ordered you need something like levin's
dovetailing approximations...)

anyway, this proof is in Ch 8 of my book *programs as diagrams*.
computability is a *categorical property* --- IF you take into account that
the programming language is well-ordered (which implies that all checkable
types are).

sorry about plugging my book. i know it's a world of tweets and advertising
campaigns but i still feel bad. my alibi is that the fact that
computability+well-order is a categorical property is way more important
than any book and surely goes deeper than i can comprehend no matter how
many turing degrees and oracles i consult...

(can't believe that i only remembered to mention this after like 5 posts...)

-- dusko



On Thu, Feb 22, 2024 at 3:42 PM Dusko Pavlovic <duskgoo@gmail.com> wrote:

> [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/en1jCANpnDCyZOvyTGnciw?domain=outlook.office365.com
>>
>

[-- Attachment #2: Type: text/html, Size: 8122 bytes --]