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<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
Dear David, I did also find the quotienting to be kind of a hack, but it is indeed a bit unclear what one should do in the context of a "weak fibration" in the sense of Ahrens and Lumsdaine, i.e. one that does not come equipped with a cleaving. On the other hand, if your fibration comes cloven, then it is easy to define the opposite in terms of this cleaving, and this construction is clearly involutive. There is plenty of reason to think that cloven fibrations are the correct notion to work with in settings that do not satisfy the axiom of choice (of course, we would not ask that morphisms of fibrations preserve cleavings). Evidence for this viewpoint is provided by univalent foundations, in which fibrations of univalent categories automatically have (unique!) cleavings — but, here we mean unique up to homotopy. As we can always take a Rezk completion, there is nothing really lost by restricting attention to fibrations of univalent categories, which by virtue of their (unique) cleaving admit a very simple description of fiberwise opposites. Best, Jon On Sun, Jan 28, 2024, at 12:51 AM, 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/yc6pC5QP8ySGoRWrSzfuzE?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/zq_BC6XQ68fKEMG4t6fSnX?domain=ncatlab.org
Blog: https://protect-au.mimecast.com/s/pBrRC71R63CkvyWBtBluYx?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
Dear David and Jon, when constructing the opposite of a fibrations one usually takes quotients. But isn't that harmless in topos logic since after all toposes have quotient types. However, when doing fibered categories one hardly ever studies only a finite number of those but has to quantify over them. So when proceeding formally one has to adopt some universes be they Grothendieck or type-theoretic in nature. Most constructions are easier on the fibered side. Taking the opposite of a fibration is the only example I know which is a bit easier on the indexed side. But think of facts like closure of fibrations inder composition. That is sort of impossible to express on the indexed side. Of course, for split fibrations things are easier. One obtains fibered categories and cartesian functors by freely inverting split cartesian functors that are fiberwise ordinary equivalences. The spotted problem with the op-construction is thus not unexpected. Moreover, it is the only thing which is easier on the indexed side. I rather find it surprising that most things are easier on the fibered side. Technically at least. And for intuitions and motivation it is quite ok to work on the indexed side. It is also ok to choose cleavages when this allows one to express things in a more intuitive way. Thomas PS Maybe the following metaphor is helpful. In topos theory one performs some arguments in the internal logic and others externally depending on what appears as more easy. But the external reasoning is more powerful. For example one cannot express internally something like well pointedness. For indexed vs fibered I rather have the impression that fibered is more flexible. At least emprirically. One usually has no problem to reformulate indexed as fibered. The other way is less evident as exemplified by closure of fibrations under composition. ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27
Thanks to those that replied. In the setting I'm interested in, a cleaving would be tantamount to choosing class-many pullbacks, where I am working in Algebraic Set Theory, with the base category of the fibration the category of classes, and the fibration one of a number of given subfibrations of the codomain fibration. In some examples there is a cleaving (for instance working with the definable classes of ZF(C)). But the whole point of the project is to avoid global choice, so avoiding it in one place only to use it to assume a cleaving doesn't sit well with me. Further, I am not committing to an ambient metatheory (like type theory or set theory), where I might get some cleavings for free. Regarding taking a quotient, I am also considering foundations where one might not even have something like (or analogous to) Scott's trick, where you can take a quotient by an equivalence relation on a proper class. Saying, for instance, that a morphism consists of a collection of things with conditions assumes one can collect those things! I don't think I need to quantify over fibrations in my intended application: it's constructing a single fibred anafunctor between two canonical fibrations attached to a class category. I'm pretty sure I don't need universes anywhere in what I'm doing. I agree with Thomas that this is really a curiosity that it's on the very short list of things where fibrations do not give a clean abstract picture. I'll have to ponder what is my best option. Regards, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com On Mon, 29 Jan 2024 at 06:34, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
Dear David and Jon,
when constructing the opposite of a fibrations one usually takes quotients. But isn't that harmless in topos logic since after all toposes have quotient types. However, when doing fibered categories one hardly ever studies only a finite number of those but has to quantify over them. So when proceeding formally one has to adopt some universes be they Grothendieck or type-theoretic in nature.
Most constructions are easier on the fibered side. Taking the opposite of a fibration is the only example I know which is a bit easier on the indexed side. But think of facts like closure of fibrations inder composition. That is sort of impossible to express on the indexed side.
Of course, for split fibrations things are easier. One obtains fibered categories and cartesian functors by freely inverting split cartesian functors that are fiberwise ordinary equivalences. The spotted problem with the op-construction is thus not unexpected.
Moreover, it is the only thing which is easier on the indexed side. I rather find it surprising that most things are easier on the fibered side. Technically at least. And for intuitions and motivation it is quite ok to work on the indexed side.
It is also ok to choose cleavages when this allows one to express things in a more intuitive way.
Thomas
PS Maybe the following metaphor is helpful. In topos theory one performs some arguments in the internal logic and others externally depending on what appears as more easy. But the external reasoning is more powerful. For example one cannot express internally something like well pointedness.
For indexed vs fibered I rather have the impression that fibered is more flexible. At least emprirically. One usually has no problem to reformulate indexed as fibered. The other way is less evident as exemplified by closure of fibrations under composition.
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=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
Could you not also work representably? Given a fibration p: E --> B a map in the opposite fibration from e to e' comprises some f: pe --> pe' in B together with a map f*(e') --> e in E over 1_e. If you hom into this from an arbitrary object e'' in E this amounts to giving a family of functions which assign to each map h: e'' -> e' and factorisation p(h) = f.k a map e'' -> e over k, naturally in e''. Erik Palmgren did something similar to this in defining LCCCs without chosen pullbacks. Of course for this you have to quantify over objects and morphisms of E which may be more or less palatable. Richard David Roberts <droberts.65537@gmail.com> writes:
Thanks to those that replied.
In the setting I'm interested in, a cleaving would be tantamount to choosing class-many pullbacks, where I am working in Algebraic Set Theory, with the base category of the fibration the category of classes, and the fibration one of a number of given subfibrations of the codomain fibration. In some examples there is a cleaving (for instance working with the definable classes of ZF(C)). But the whole point of the project is to avoid global choice, so avoiding it in one place only to use it to assume a cleaving doesn't sit well with me. Further, I am not committing to an ambient metatheory (like type theory or set theory), where I might get some cleavings for free.
Regarding taking a quotient, I am also considering foundations where one might not even have something like (or analogous to) Scott's trick, where you can take a quotient by an equivalence relation on a proper class. Saying, for instance, that a morphism consists of a collection of things with conditions assumes one can collect those things!
I don't think I need to quantify over fibrations in my intended application: it's constructing a single fibred anafunctor between two canonical fibrations attached to a class category. I'm pretty sure I don't need universes anywhere in what I'm doing.
I agree with Thomas that this is really a curiosity that it's on the very short list of things where fibrations do not give a clean abstract picture.
I'll have to ponder what is my best option.
Regards, David
David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com
On Mon, 29 Jan 2024 at 06:34, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
Dear David and Jon,
when constructing the opposite of a fibrations one usually takes quotients. But isn't that harmless in topos logic since after all toposes have quotient types. However, when doing fibered categories one hardly ever studies only a finite number of those but has to quantify over them. So when proceeding formally one has to adopt some universes be they Grothendieck or type-theoretic in nature.
Most constructions are easier on the fibered side. Taking the opposite of a fibration is the only example I know which is a bit easier on the indexed side. But think of facts like closure of fibrations inder composition. That is sort of impossible to express on the indexed side.
Of course, for split fibrations things are easier. One obtains fibered categories and cartesian functors by freely inverting split cartesian functors that are fiberwise ordinary equivalences. The spotted problem with the op-construction is thus not unexpected.
Moreover, it is the only thing which is easier on the indexed side. I rather find it surprising that most things are easier on the fibered side. Technically at least. And for intuitions and motivation it is quite ok to work on the indexed side.
It is also ok to choose cleavages when this allows one to express things in a more intuitive way.
Thomas
PS Maybe the following metaphor is helpful. In topos theory one performs some arguments in the internal logic and others externally depending on what appears as more easy. But the external reasoning is more powerful. For example one cannot express internally something like well pointedness.
For indexed vs fibered I rather have the impression that fibered is more flexible. At least emprirically. One usually has no problem to reformulate indexed as fibered. The other way is less evident as exemplified by closure of fibrations under composition.
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 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<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
We're departing, we're departing. Just give us a few more years. Michael ________________________________ From: Dusko Pavlovic <duskgoo@gmail.com> Sent: Thursday, February 8, 2024 7:02 PM To: David Roberts <droberts.65537@gmail.com> Cc: categories@mq.edu.au <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 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<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
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 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<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
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 <duskgoo@gmail.com<mailto:duskgoo@gmail.com>> 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. <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 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<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
Dear David, In case it helps, there is a nicely typeset paper by Bénabou and Streicher about distributors between fibrations here: https://protect-au.mimecast.com/s/YViBCP7L1NfxXmNZtzkmO4?domain=mathematik.t.... Best, Jon On Sat, Feb 10, 2024, at 6:28 AM, David Roberts wrote:
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://protect-au.mimecast.com/s/BO5DCQnM1WfWPql9SPfE1j?domain=ncatlab.org
Blog: https://protect-au.mimecast.com/s/0ymoCRONg6sLWl0QuPWulZ?domain=thehighergeo...
On Sat, 10 Feb 2024 at 06:25, Dusko Pavlovic <duskgoo@gmail.com> 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. <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> *Sent:* Thursday, February 8, 2024 7:02 PM *To:* David Roberts <droberts.65537@gmail.com> *Cc:* categories@mq.edu.au <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> 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/Xv6nCVARmOHAyKkXHJDjBn?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/BO5DCQnM1WfWPql9SPfE1j?domain=ncatlab.org Blog: https://protect-au.mimecast.com/s/0ymoCRONg6sLWl0QuPWulZ?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
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
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
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=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< 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
participants (7)
-
David Roberts -
Dusko Pavlovic -
Jon Sterling -
Michael Barr, Prof. -
Richard Garner -
Sergei Soloviev -
Thomas Streicher