Re: Fibrewise opposite fibration + computers

[Dusko Pavlovic <duskgoo@gmail.com>]

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

yes, computations do need to be monotone, but no, that does not require
recording traces. the padding lemma says that.

-- dusko

On Fri, Feb 9, 2024 at 1:25 AM Sergei Soloviev <Sergei.Soloviev@irit.fr>
wrote:

> >in the world where math is done in collaboration with computers,
> everything *is* well-ordered, and cantor was right.
>
> I think, only if we record each run of each programme. The ordering is not
> stable
> in this sense.
>
> Sergei Soloviev
>
> Le Vendredi, Février 09, 2024 01:02 CET, Dusko Pavlovic <duskgoo@gmail.com>
> a écrit:
>
> > FWIW, the history of problems around choosing representatives of
> equivalence classes may very well be a completely self-inflicted artifact
> of academic politics. if it were up to young cantor, sets could be taken
> with well-orders and any equivalence class would have a minimal
> representative. in the world where math is done in collaboration with
> computers, everything *is* well-ordered, and cantor was right. if a
> fibration E is computable, the equivalence classes of spans that define
> E^op have minimal representatives and are effectively defined. in lawvere's
> words: if we don't transition to cardinalities but stay in a boolean topos
> with cantor-bernstein, all surjections split effectively.
> >
> > but dedekind convinced cantor that he should yield to the great
> professors and not assume that the reals can be well-ordered. then dedekind
> used cantor's basic construction in Zahlenbericht (with a reference to
> cantor in the manuscript, no reference in the published version), whereas
> cantor spent 10 years trying to *prove* that all sets can be well-ordered.
> enter zermelo to edit cantor's collected works, to criticize cantor for
> well-ordering, and to packages this problematic idea behind the
> second-order quantifier in his own contribution: the axiom of choice. so
> that we could happily choose the representatives of equivalence classes
> ever after from behind the second-order quantifier =&
> >
> > but it will be like max planck said: the new paradigm will win when the
> generations suppressing it depart. in the world where math is computed,
> zermelo was wrong, cantor was right, and equivalence classes have minimal
> representatives. OR if we develop category theory categorically, the dual
> hom-sets will be effectively definable...
> >
> > :)
> > -- dusko
> >
> > On Sat, Jan 27, 2024 at 7:21 PM David Roberts <droberts.65537@gmail.com
> <mailto:droberts.65537@gmail.com>> wrote:
> > Hi all
> >
> > what with all the discussion of Bénabou and fibrations, I have a
> > question about what happens at a foundational level when one takes the
> > opposite of a fibration E --> B fibrewise. Call this (E/B)^op --> B
> >
> > For reference, one can see section 5 of Streicher's
> > https://protect-au.mimecast.com/s/pqE7CD1vRkCVAR2ncWHgr1?domain=arxiv.org<
> https://protect-au.mimecast.com/s/pqE7CD1vRkCVAR2ncWHgr1?domain=arxiv.org>
> for the construction. The point is
> > that the morphisms are defined to be equivalence classes of certain
> > data. However, in a setting where one cannot necessarily form
> > equivalence classes, it's less clear how to proceed. The point is that
> > I don't want to be assuming any particular foundations here, just
> > working at the level of a first-order theory (in the way that ETCS is
> > a first-order theory of sets, say)
> >
> > The only thing I can think of is that the construction actually
> > describes a category weakly enriched in 0-truncated groupoids (or
> > whatever you want to call the first-order description of such a
> > thing). You still get a functor down to the base 1-category, and
> > perhaps one has to now think about what it means for such a thing to
> > be a fibration, without passing to the plan 1-category quotient.
> >
> > That is probably fine for my purposes, but then you have to worry that
> > taking the fibrewise opposite again should return the original
> > fibration, at least up to equivalence. The original construction with
> > the equivalence classes gives back the original thing up to
> > *isomorphism*: ((E/B)^op/B)^op \simeq E, over B. So now one has to
> > think about what the fiberwise opposite construction looks like for
> > these slightly generalised fibrations (enriched with 0-truncated
> > groupoids), and one would hope that this gives back the original thing
> > after two applications (again, up to the appropriate notion of
> > equivalence).
> >
> > Note that the construction in the literature (eg Streicher's notes, or
> > Jacob's book) has the fibres (E/B)^op_b of the fibrewise opposite be
> > *isomorphic* to the opposite of the original fibres E_b. In this
> > fancier setting, one might also only get equivalence, but I haven't
> > checked that.
> >
> > Has anyone thought about something like this before? Or any pointers
> > to anything related?
> >
> > Best wishes,
> >
> > David Roberts
> > Webpage: https://protect-au.mimecast.com/s/NsKOCE8wlRCDxQrgCwE3__?domain=ncatlab.org<
> https://protect-au.mimecast.com/s/NsKOCE8wlRCDxQrgCwE3__?domain=ncatlab.org
> >
> > Blog: https://protect-au.mimecast.com/s/s75rCGv0Z6fM4Vx0cp9nZr?domain=thehighergeometer.wordpress.com<
> https://protect-au.mimecast.com/s/s75rCGv0Z6fM4Vx0cp9nZr?domain=thehighergeometer.wordpress.com
> >
> >
> >
> > You're receiving this message because you're a member of the Categories
> mailing list group from Macquarie University. To take part in this
> conversation, reply all to this message.
> >
> > View group files<
> https://protect-au.mimecast.com/s/usD5CJyBZ6tYw7G1hLuPj-?domain=outlook.office365.com>
>  |   Leave group<
> https://protect-au.mimecast.com/s/gg31CK1DOrCnWjgBIppYLA?domain=outlook.office365.com>
>  |   Learn more about Microsoft 365 Groups<
> https://protect-au.mimecast.com/s/SGV0CL7Eg9f19Jxmug1lBk?domain=aka.ms>
> >
> >
> >
> > You're receiving this message because you're a member of the Categories
> mailing list group from Macquarie University. To take part in this
> conversation, reply all to this message.
> >
> > View group files<
> https://protect-au.mimecast.com/s/ONEZCMwGj8CZ3QKRHG2Xn2?domain=outlook.office365.com>
>  |   Leave group<
> https://protect-au.mimecast.com/s/Rl4xCNLJxkiB32KEUVwCv7?domain=outlook.office365.com>
>  |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/SGV0CL7Eg9f19Jxmug1lBk?domain=aka.ms>
> >
>

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