Re: Fibrewise opposite fibration

[Dusko Pavlovic <duskgoo@gmail.com>]

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

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. <barr.michael@mcgill.ca<mailto:barr.michael@mcgill.ca>> wrote:
We're departing, we're departing.  Just give us a few more years.

Michael
________________________________
From: Dusko Pavlovic <duskgoo@gmail.com<mailto:duskgoo@gmail.com>>
Sent: Thursday, February 8, 2024 7:02 PM
To: David Roberts <droberts.65537@gmail.com<mailto:droberts.65537@gmail.com>>
Cc: categories@mq.edu.au<mailto:categories@mq.edu.au> <categories@mq.edu.au<mailto: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 <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://arxiv.org/abs/1801.02927<https://protect-au.mimecast.com/s/gvWHCWLVn6iBqANRc6iRxY?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://ncatlab.org/nlab/show/David+Roberts<https://protect-au.mimecast.com/s/FaYYCXLW6DiYKxkVsVhW1j?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/vAVeCYW86EsxlzjEC9j_WE?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/uMNZCZY146sNg3XrUy9UvD?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/HgisC1WLjwsYG7L2sYATB_?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/4lZlC2xMRkUw3N0PuMj66s?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/UVrCC3QNl1SQK5W6uY1ft-?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/Eej8C4QO8xS15pRMuNi8Pv?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/4lZlC2xMRkUw3N0PuMj66s?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://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


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