Hi all, So here's the thing: my setup is fibrations (non-cloven in general) over a given model of algebraic set theory, with anafunctors over the base built using functors preserving cartesian morphisms in the usual way. So I'm avoiding choice both internal to the model of AST, as well as externally, so that eso + ff faithful functors aren't always equivalences in the 2-category of fibrations over the given base. I presume Bénabou thought at some point about distributors between fibrations, but I'd have to dig through those old scanned documents to see if there is a paper record. My approach would presumably be a special case of that, as he so forcefully pointed out to me a bit over a decade ago on this list. If anyone recalls anything along these lines, I'd appreciate a pointer. All the best, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com On Sat, 10 Feb 2024 at 06:25, Dusko Pavlovic > wrote: we are all departing, of course. there is no power law there. the way i understand plack's statement about the paradigm changes when people depart is that some people leave behind houses for other people to live in, whereas others leave behind fortresses with nothing to defend. there is a paper by thomas kuhn about "The Function of Dogma in Scientific Research" which i think speaks to us more clearly than his famous "Scientific Revolutions". -- dusko On Thu, Feb 8, 2024 at 3:48 PM Michael Barr, Prof. > wrote: We're departing, we're departing. Just give us a few more years. Michael ________________________________ From: Dusko Pavlovic > Sent: Thursday, February 8, 2024 7:02 PM To: David Roberts > Cc: categories@mq.edu.au > Subject: Re: Fibrewise opposite fibration 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://arxiv.org/abs/1801.02927 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://ncatlab.org/nlab/show/David+Roberts Blog: https://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 | 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 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