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/pw9JCk815RCQBglBI2ERjy?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/FuxkClx1OYUZELGEt9Uog4?domain=ncatlab.org Blog: https://protect-au.mimecast.com/s/qblGCmO5wZsnlvXlhB28KI?domain=thehighergeo...
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 | Leave group | Learn more about Microsoft 365 Groups
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 | Leave group | Learn more about Microsoft 365 Groups