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 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 > 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 > 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 > > >