Fibrewise opposite fibration

Fibrewise opposite fibration

[David Roberts]

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

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/ULb4CgZ05Jf2rlDBs3sP1k?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/ygpkCjZ12Rfq2jVOS1CfGU?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/bSqFCk815RCQ7nPwt8C6hN?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://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: 5168 bytes --]

Re: Fibrewise opposite fibration

[Jon Sterling]

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

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 
> <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 
> <https://protect-au.mimecast.com/s/zq_BC6XQ68fKEMG4t6fSnX?domain=ncatlab.org>
> Blog: https://protect-au.mimecast.com/s/pBrRC71R63CkvyWBtBluYx?domain=thehighergeometer.wordpress.com 
> <https://protect-au.mimecast.com/s/pBrRC71R63CkvyWBtBluYx?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/byccC81Vq2CRlQwytMdB38?domain=outlook.office365.com> 
>   |   Leave group 
> <https://protect-au.mimecast.com/s/DPBTC91W8rCBvxYwIP19ms?domain=outlook.office365.com> 
>   |   Learn more about Microsoft 365 Groups <https://protect-au.mimecast.com/s/LmnsC0YKgRs3K4rAS3C408?domain=aka.ms>

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

Re: Fibrewise opposite fibration

[Thomas Streicher]

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[David Roberts]

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

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<https://protect-au.mimecast.com/s/nxkvCk815RCQPnMOCQexkK?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/3hU7Clx1OYUZjoB2sqyfqO?domain=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=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: 6826 bytes --]

Re: Fibrewise opposite fibration

[Richard Garner]

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.

Re: Fibrewise opposite fibration

[Christian Sattler]

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

Here is a similar suggestion.

---------- Forwarded message ---------
From: Christian Sattler <sattler.christian@gmail.com<mailto:sattler.christian@gmail.com>>
Date: Sun, 28 Jan 2024 at 16:40
Subject: Re: Fibrewise opposite fibration
To: David Roberts <droberts.65537@gmail.com<mailto:droberts.65537@gmail.com>>


Note that there is also a "universal" description instead of an "existential" description, with the quotient replaced by coherence. There, a map in (E/B)^op from x to y over f : a → b consists of the following:
* for each cartesian lift u : x' → y of f, a vertical map h_u : x' → x,
* such that for any two such cartesian lifts u₀ : x'₀ → y and u₁ : x'₁ → y related by a vertical map k : x'₀ → x'₁ (necessarily invertible), the maps h_u₀ and h_u₁ are also related by k.

This is a common situation when working with property-like structure.

In foundations without choice, it can be productive to work with objects with a choice for a property-like structure (e.g., a cleavage) and morphisms that ignore that structure. This is a way around the problem you describe.

On Wed, 31 Jan 2024 at 01:45, Richard Garner <richard.garner@mq.edu.au<mailto:richard.garner@mq.edu.au>> wrote:

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<mailto: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<https://protect-au.mimecast.com/s/6h7AC1WLjwsYZXB0FL1nc1?domain=ncatlab.org>
> Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/A-5kC2xMRkUwmQZ4F1BUVR?domain=thehighergeometer.wordpress.com>
>
> On Mon, 29 Jan 2024 at 06:34, Thomas Streicher
> <streicher@mathematik.tu-darmstadt.de<mailto: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=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: 9984 bytes --]

Re: Fibrewise opposite fibration

[streicher]

If we work with split fibrations and arbitrary cartesian functors between
them we can construct the opposite of a fibration without quotienting.
That is possible but in my eyes less elegant than the usual approach where
one assumes that one can factorize modulo equivalence relations even if
they are big.

Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Martin Bidlingmaier]

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

2-monad theory and related model categories of sketches could be relevant here, because these techniques reduce the problematic case of a non-split fibrations F that was raised by David in his initial message to the easy case of an equivalent but split fibration F’. In terms of logical foundations, this requires sufficiently large universes, but I expect (but haven’t verified) that you can do without choice.

I’m not sure I remember all the details correctly, but let me try to outline how this should work. Consider the category of sketches for fibrations: A sketch for a fibration is given by a functor E -> B and for each morphism f in B a set of “cartesian-marked” morphisms M_f in E that map to f. Morphism of sketches are commuting squares of functors that preserve Cartesian markings. Note that Cartesian-marked morphisms need not actually be Cartesian. Every fibration has a natural strucuture as sketch, where precisely the Cartesian morphisms are Cartesian-marked. And every sketch generates a fibration with natural marking. Informally, this generated fibration is obtained by freely adding morphisms to E so that all the M_f are non-empty and then adding commutative diagrams so that every Cartesian-marked morphism is actually Cartesian. Finally, one closes M_f under isomorphism over E.

More formally, there is a model category structure on sketches such that precisely the naturally marked fibrations are fibrant objects, and the equivalences of fibrant objects are the componentwise equivalences in the arrow category on Cat. Fibrant replacement of a sketch is given by the informal free generation I explained in the previous paragraph. (Note that there’s a naming collision here: Fibrations in the sense of Grothendieck fibrations and in the model categorical sense.)

Now, if you use Garner’s small object argument you get a fibrant replacement functor. Crucially, this fibrant replacement functor is the monad you get from a 1-categorical adjunction with the category of “strict” Grothendieck fibrations. These are given by Grothendieck fibrations with a cleavage, and their morphisms are commuting squares of functors that preserve cleavage on the nose.

Why does this give you the equivalent split fibration F’ from a non-split fibration F I promised in the beginning? Like so: You first map F (considered as a naturally marked sketch) into the category of strict (in particular: split) fibrations via the left adjoint I mentioned in the preceding paragraph. From there you apply the right adjoint to get back to sketches, which is simply given by forgetting the cleavage and taking the natural marking to obtain F’. F -> F’ is an equivalence, and F’ has a cleavage by construction.

If you want to know more about this you might want to take a look at my paper on models of type theory in lcc categories and its citations: https://protect-au.mimecast.com/s/J0ogCoV1Y2SzmkQri1YV08?domain=arxiv.org
Among other things, this paper defines the model categories of sketches for lcc categories and strict lcc categories. Grothendieck fibrations should work entirely analogously. I believe Lack’s “Homotopy theoretic aspects of 2-category theory” works out the “strict” model category of strict Grothendieck fibrations I mentioned above in the generality of an arbitrary 2-monad, but I’m not aware of a general model categorical treatment of sketches.

On Wed, Jan 31, 2024 at 17:41, <[streicher@mathematik.tu-darmstadt.de](mailto:On Wed, Jan 31, 2024 at 17:41,  <<a href=)> wrote:

> If we work with split fibrations and arbitrary cartesian functors between
> them we can construct the opposite of a fibration without quotienting.
> That is possible but in my eyes less elegant than the usual approach where
> one assumes that one can factorize modulo equivalence relations even if
> they are big.
>
> Thomas
>
> ----------
>
> You're receiving this message because you're a member of the Categories mailing list group from Macquarie University.
>
> Leave group:
> https://protect-au.mimecast.com/s/H5fJCp81gYC8Z57nfDKrk8?domain=outlook.office365.com

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

Re: Fibrewise opposite fibration

[Jon Sterling]

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

Hi Thomas et al,

I believe the proposed non-quotiented construction works even with a cleaving that is not split. Does anyone know if this is true? (I thought I had checked this a while ago, but now I cannot find my notes and am less confident; however, it is claimed by Von Glehn in Example 3.9 here: http://www.tac.mta.ca/tac/volumes/33/36/33-36.pdf<https://protect-au.mimecast.com/s/bbuoCwV1jpS1nNELuq9eMh?domain=tac.mta.ca>.) Glancing at it briefly, it looks rather like the identity and associativity laws follow from the higher identities governing associators and unitors in a pseudofunctor.

I agree it is inelegant to assume a splitting, but I think it is rather elegant to assume a (non-split) cleaving as property-like structure (so we do not ask that it be preserved) — Indeed, this is precisely what you get from the Chevalley criterion for fibrations in a 2-category. I think this is analogous to the way that in an internal setting we must assume chosen structures but not typically ask to preserve the choices; when we do not wish to assume chosen structures at all, we can either pass to stacks or work in a univalent / fully saturated setting.

Best,
Jon


On Wed, Jan 31, 2024, at 11:41 PM, streicher@mathematik.tu-darmstadt.de wrote:
> If we work with split fibrations and arbitrary cartesian functors between
> them we can construct the opposite of a fibration without quotienting.
> That is possible but in my eyes less elegant than the usual approach where
> one assumes that one can factorize modulo equivalence relations even if
> they are big.
>
> Thomas


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: 4136 bytes --]

Re: Fibrewise opposite fibration

[Thomas Streicher]

Dear Jon,

for constructing the opposite of a fibration you do not need at all
that the chosen cleavage is split. It is easy to see that fixing the
cartesian arrow also fixes the vertical arrow.

If everybody is happy with this solution I am fine. It is in the same spirit
as chosen pullbacks or chosen finite limits.
The reason for my reluctance is that nobody would consider as a
natural notion a vector space with a chosen basis.
The virtue of strong choice is that then such additional structure can be
pulled out of the hat at demand.


Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Jon Sterling]

Hi Thomas,

I'm sympathetic, but I don't agree about the comparison to vector spaces because a cleaving is nothing like a basis. My evidence for this is that for fibrations of univalent categories, cleavings are always canonical; on the other hand, there is no foundational tweak that could make vector spaces have canonical bases.

Best,
Jon


On Thu, Feb 1, 2024, at 11:06 AM, Thomas Streicher wrote:
> Dear Jon,
>
> for constructing the opposite of a fibration you do not need at all
> that the chosen cleavage is split. It is easy to see that fixing the
> cartesian arrow also fixes the vertical arrow.
>
> If everybody is happy with this solution I am fine. It is in the same spirit
> as chosen pullbacks or chosen finite limits.
> The reason for my reluctance is that nobody would consider as a
> natural notion a vector space with a chosen basis.
> The virtue of strong choice is that then such additional structure can be
> pulled out of the hat at demand.
>
>
> Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Christian Sattler]

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

I think there is a problem with this analogy. A basis for a vector space is actual (higher) data, but a cleavage for a fibration is property-like data.

Morphisms of fibrations that weakly preserve the cleavage are just morphisms of fibrations.

Morphisms of vector spaces that preserve a chosen basis are very different from just morphisms of vector spaces.

On Thu, 1 Feb 2024, 12:07 Thomas Streicher, <streicher@mathematik.tu-darmstadt.de<mailto:streicher@mathematik.tu-darmstadt.de>> wrote:
Dear Jon,

for constructing the opposite of a fibration you do not need at all
that the chosen cleavage is split. It is easy to see that fixing the
cartesian arrow also fixes the vertical arrow.

If everybody is happy with this solution I am fine. It is in the same spirit
as chosen pullbacks or chosen finite limits.
The reason for my reluctance is that nobody would consider as a
natural notion a vector space with a chosen basis.
The virtue of strong choice is that then such additional structure can be
pulled out of the hat at demand.


Thomas


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: 3913 bytes --]

Re: Fibrewise opposite fibration

[Thomas Streicher]

> I'm sympathetic, but I don't agree about the comparison to vector spaces because a cleaving is nothing like a basis. My evidence for this is that for fibrations of univalent categories, cleavings are always canonical; on the other hand, there is no foundational tweak that could make vector spaces have canonical bases.

I agree that from a univalent point of view all cleavages are equal.
But from a univalent point of view all cleavages are even split!
That is a bit too much for me (see Warning (1) on p.10 of my notes on
fibered cats).

But I do not want to take up old discussions! I really prefer to disagree.

Instead I admit that all choices of cleavages are uniquely isomorphic
which certainly is not teh case for bases.

Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Thomas Streicher]

From a pragmatic point of view it certainly works to work with
fibrations endowed with a (non-split) cleaving and arbitrary
cartesian functors (not preserving these cleavings). And I think
this solves David R.'s problem.
It is also true that fibrations you consider always come equipped
with some cleaving. Well, the fundamental fibration of a category
BB with pullbacks only does if you assume BB being andowed with a
choice of pullbacks.
So from a pragmatic point of view choice is often needed just for
restoring information you have deliberately forgotten. When speaking
about arbitrary fibrations, of course, this information is not present
and has to be assumed as given.
But admitting strong choice principles allows one to remove this clutter
from definitions and rather to restore them when needed. But this
cleaning up has the unintended side effect of getting logically very
strong. I have never seen any amazing consequence of AC for classes
but maybe there are.

BTW Benabou himself put quite some emphasis on avoiding choice in his
JSL paper. But in the practice of working with fibered categories you
introduce cleavages whenever convenient. I did so in my notes and I
guess so did Benabou in his various notes. This is no suprise in the
light of the above discussion because it is simply convenient.

In any case this issue does not influence the practice of working with
fibered categories. There are just different ways of explaining this
practice from a foundational point of view...

Thomas


PS In analysis you often apply number choice without saying. In very
applied texts they use Skolem functions more often then existential
quantifiers. But not for foundational reasons rather because they find
it more intuitive. You really have to be a logician for having a
problem with choice :-)





----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Dusko Pavlovic]

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

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/JQQrCzvkmpf2ooA0c4GaAU?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/DNIaCANpnDCWAAzvC8EeEA?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/JbslCBNqgBC455OghNfAGM?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/-u9uCD1vRkCVllkRhZYm-_?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/0UV7CE8wlRCD55NQiZ9Odk?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/Bb5LCGv0Z6fM55QVS0JKAe?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: 9862 bytes --]

Re: Fibrewise opposite fibration

[Michael Barr, Prof.]

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

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<https://protect-au.mimecast.com/s/LAaXC0YKgRs3wv9yUwVjKm?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/GhFVCgZ05Jf2Z6jBson1eT?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/MYi0CjZ12RfqQEwOU5GmXu?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/866DCk815RCQzlRwS9DGXk?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/Q49wClx1OYUZNG3MT1vJod?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/XAReCmO5wZsnNX7MTDd_ss?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: 12822 bytes --]

Re: Fibrewise opposite fibration + computers

[Sergei Soloviev]

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

>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<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<https://protect-au.mimecast.com/s/FuxkClx1OYUZELGEt9Uog4?domain=ncatlab.org>
> Blog: https://protect-au.mimecast.com/s/qblGCmO5wZsnlvXlhB28KI?domain=thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/qblGCmO5wZsnlvXlhB28KI?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/OxXBCnx1Z5UoDnwDTZf7XQ?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/2AJpCoV1Y2SzYk9YFOgDms?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/yBcOCp81gYC8o5koh2VBAb?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/2OXtCq71jxf5N9BNsqH7aG?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/qu6bCr810kCvZxMZtQqPOW?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/yBcOCp81gYC8o5koh2VBAb?domain=aka.ms>
>

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

Re: Fibrewise opposite fibration

[Dusko Pavlovic]

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

Re: Fibrewise opposite fibration + computers

[Dusko Pavlovic]

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

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=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<https://protect-au.mimecast.com/s/SGV0CL7Eg9f19Jxmug1lBk?domain=aka.ms>
> >
>

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

Re: Fibrewise opposite fibration

[David Roberts]

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

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<https://protect-au.mimecast.com/s/pAyTCK1DOrCnW5potMTgxQ?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/spbWCL7Eg9f19n8WsqojnV?domain=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<https://protect-au.mimecast.com/s/tjAKCMwGj8CZ34mrFJj1nS?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/pAyTCK1DOrCnW5potMTgxQ?domain=ncatlab.org>
Blog: https://thehighergeometer.wordpress.com<https://protect-au.mimecast.com/s/spbWCL7Eg9f19n8WsqojnV?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/e296CNLJxkiB3myWcRqhJV?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/4-wFCOMK7YcKxmQ8TPoZlH?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/q-BLCP7L1NfxXEVwSr0Yyx?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/hVcNCQnM1WfWPjZQF9aAEJ?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/CeXXCRONg6sLWqZ6F0r5VA?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/q-BLCP7L1NfxXEVwSr0Yyx?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: 16594 bytes --]

Re: Fibrewise opposite fibration

[Jon Sterling]

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

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.tu-darmstadt.de.

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 
> <https://protect-au.mimecast.com/s/BO5DCQnM1WfWPql9SPfE1j?domain=ncatlab.org>
> Blog: https://protect-au.mimecast.com/s/0ymoCRONg6sLWl0QuPWulZ?domain=thehighergeometer.wordpress.com 
> <https://protect-au.mimecast.com/s/0ymoCRONg6sLWl0QuPWulZ?domain=thehighergeometer.wordpress.com>
>
>
> 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 <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 <https://protect-au.mimecast.com/s/BO5DCQnM1WfWPql9SPfE1j?domain=ncatlab.org>
>>>> Blog: https://protect-au.mimecast.com/s/0ymoCRONg6sLWl0QuPWulZ?domain=thehighergeometer.wordpress.com <https://protect-au.mimecast.com/s/0ymoCRONg6sLWl0QuPWulZ?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/DcXZCWLVn6iBqYXxtmMdt6?domain=outlook.office365.com>   |   Leave group <https://protect-au.mimecast.com/s/m1FyCXLW6DiYKNDGi9Qe0I?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups <https://protect-au.mimecast.com/s/N_joCYW86EsxlZpgt3wBdu?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/rMH6CZY146sNgR8xTNoDs8?domain=outlook.office365.com>   |   Leave group <https://protect-au.mimecast.com/s/dY-uC1WLjwsYGmBOim9ihq?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups <https://protect-au.mimecast.com/s/N_joCYW86EsxlZpgt3wBdu?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/KsWeC2xMRkUw3GZ6tv82Rs?domain=outlook.office365.com> 
>   |   Leave group 
> <https://protect-au.mimecast.com/s/S9PHC3QNl1SQKM9xiji1dh?domain=outlook.office365.com> 
>   |   Learn more about Microsoft 365 Groups <https://protect-au.mimecast.com/s/N_joCYW86EsxlZpgt3wBdu?domain=aka.ms>

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

Re: Fibrewise opposite fibration

[Nath Rao]

[This no longer about how to define fibrewise opposite fibration, so may
be it is time t change the subject line.]

IMHO, this seems to be more like a religious war. In "mathematics in the
small", local axiom of choice allows us to choose representatives only
when needed. So we are grew up believing that putting things in the
definition that are not preserved by morphisms is "not done" (the
religious dogma) . But them we run up against issues when we try to do
the same thing in "mathematics in the large", and either ignore the
problem or argue endlessly about how to solve it.

Also, if are willing to assume that every set comes with a
well-ordering, why not assume a global well-ordering and be done with
it? [If I am going to use universes anyway, it seems to be trivial to do
this, as long as I live inside a fixed universe in any given proof.] For
ZFC, global choice is a conservative extension. Not being a logician, am
not sure, but perhaps it can be shown for global choice is a
conservative extension of local choice of 'all suitable set theories'.
Then we can do global choice with no qualms.

Regards
Nath Rao





----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Jon Sterling]

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

Dear Nath,

It is important to note that although global choice is a very useful tool indeed, it is not consistent with the interpretation of the universe of sets in univalent foundations (UF) — despite the fact that the usual axiom of choice can be added to univalent foundations without any problems. The contradiction is described in Theorem 3.2.2 of the HoTT Book.

Of course, one is free to use traditional set theoretic foundations (either in terms of ZFC, or in terms of its embedding into UF + choice via iterative notions of set), and in this case the usual classical results about the consistency of indefinite descriptions would be available — but the reason I bring this up is that univalent foundations offers a compelling alternative to the usual approach of filling in missing data via choice that you bring up. In set theoretic foundations, the missing data is not uniquely determined (it is only unique up to isomorphism) and so you need some kind of choice to get it back; but in univalent foundations, it very often (in fact, usually!) happens that this missing data is uniquely determined in the appropriate sense — in this way, univalence increases the scope of *definite* descriptions so much that many classical uses of choice and/or indefinite descriptions become obsolete. This is why, in univalent foundations, you can avoid choosing a cleaving of a fibration because all fibrations are automatically, canonically, cloven.

It makes sense that there is a variety of approaches to deal with such issues.

Best,
Jon


On Mon, Feb 12, 2024, at 1:20 PM, Nath Rao wrote:
> [This no longer about how to define fibrewise opposite fibration, so may
> be it is time t change the subject line.]
>
> IMHO, this seems to be more like a religious war. In "mathematics in the
> small", local axiom of choice allows us to choose representatives only
> when needed. So we are grew up believing that putting things in the
> definition that are not preserved by morphisms is "not done" (the
> religious dogma) . But them we run up against issues when we try to do
> the same thing in "mathematics in the large", and either ignore the
> problem or argue endlessly about how to solve it.
>
> Also, if are willing to assume that every set comes with a
> well-ordering, why not assume a global well-ordering and be done with
> it? [If I am going to use universes anyway, it seems to be trivial to do
> this, as long as I live inside a fixed universe in any given proof.] For
> ZFC, global choice is a conservative extension. Not being a logician, am
> not sure, but perhaps it can be shown for global choice is a
> conservative extension of local choice of 'all suitable set theories'.
> Then we can do global choice with no qualms.
>
> Regards
> Nath Rao
>
>
>
>
>
> ----------
>
> You're receiving this message because you're a member of the Categories 
> mailing list group from Macquarie University.
>
> Leave group:
> https://protect-au.mimecast.com/s/Uy0cCp81gYC8WpnQSP-lCQ?domain=outlook.office365.com

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

Re: Fibrewise opposite fibration

[Thomas Streicher]

Dear Nath and Jon,

I am naturally sympathizing with Nath's remark.
Thanks, Jon, for giving precise reference for why global choice
implies classical logic in HoTT (it is not inconsistent as far as I know).
I am grateful for the quite non-ideological discussion of the issue BTW !

My scepticism w.r.t. HoTT is not ideological (or "self destructive" as
some people may have thought) but was rather motivated by the fact that it
caused problems with one of my favourite notions of category theory, namely
Grothendieck fibrations. There is the notion of Street fibration which
you obtain when closing Groth. fibrations by closing under categorical
equivalences. But there are not too many examples as far as I can see.

There is a way out of it suggested by Ahrens and Lumsdaine, namely
"displayed categories", which are systematically employed in Jon's very
nice notes on relative category theory with C. Angiuli. This is certainly a way
how to proceed in case one wants to keep the univalence principle without
enforcing classical logic.

But it makes things technically more complicated and I personally prefer a
non-univalent setting. Lurie also can live without univalence both in
his book and the Kerodon.
This confirms my impression that univalence is a radical thought experiment
whose consequences still have to be evaluated. For me (and many other people)
foundations is not a religious business but rather a question which setting is
the most convenient one for doing the things one wants to do in maths. This
can be evaluated only a posteriori and a certain pluralism might be a healthy
attitude.

In any case I think w.r.t. fibered categories the most reasonable thing
seems to be cleaved fibrations and arbitrary cartesian functors. It is
foundationally tolerant and close to the practice of fibered category theory.

Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Jon Sterling]

Dear Thomas,

In fact, the reference shows that global choice really is inconsistent in HoTT. Univalence asserts (among other things) that all operations on the universe (even the universe of sets) are "natural" under equivalences, but a global choice operator cannot be natural in this sense.

Best,
Jon


On Tue, Feb 13, 2024, at 10:04 AM, Thomas Streicher wrote:
> Dear Nath and Jon,
>
> I am naturally sympathizing with Nath's remark.
> Thanks, Jon, for giving precise reference for why global choice
> implies classical logic in HoTT (it is not inconsistent as far as I know).
> I am grateful for the quite non-ideological discussion of the issue BTW !
>
> My scepticism w.r.t. HoTT is not ideological (or "self destructive" as
> some people may have thought) but was rather motivated by the fact that it
> caused problems with one of my favourite notions of category theory, namely
> Grothendieck fibrations. There is the notion of Street fibration which
> you obtain when closing Groth. fibrations by closing under categorical
> equivalences. But there are not too many examples as far as I can see.
>
> There is a way out of it suggested by Ahrens and Lumsdaine, namely
> "displayed categories", which are systematically employed in Jon's very
> nice notes on relative category theory with C. Angiuli. This is certainly a way
> how to proceed in case one wants to keep the univalence principle without
> enforcing classical logic.
>
> But it makes things technically more complicated and I personally prefer a
> non-univalent setting. Lurie also can live without univalence both in
> his book and the Kerodon.
> This confirms my impression that univalence is a radical thought experiment
> whose consequences still have to be evaluated. For me (and many other people)
> foundations is not a religious business but rather a question which setting is
> the most convenient one for doing the things one wants to do in maths. This
> can be evaluated only a posteriori and a certain pluralism might be a healthy
> attitude.
>
> In any case I think w.r.t. fibered categories the most reasonable thing
> seems to be cleaved fibrations and arbitrary cartesian functors. It is
> foundationally tolerant and close to the practice of fibered category theory.
>
> Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Thomas Streicher]

> In fact, the reference shows that global choice really is inconsistent in HoTT. Univalence asserts (among other things) that all operations on the universe (even the universe of sets) are "natural" under equivalences, but a global choice operator cannot be natural in this sense.

Thanks for this clarification!

One needs global choice in CT for establishing that full and faithful
functors which are essentially surjective are actually categorical
equivalences.
In practice you just have the stronger notion.

In my eyes HoTT is an attempt to live with the weaker notion.

In basic topos theory global choice is assumed when identifying
inverse images of geometric morphisms with cocontinuous functors
preserving finite limits. Therefore, I never believed that you can do
topos theory in a weak meta theory without strong choice principles.
At least not the way it is done in the traditional texts.

Maybe HoTT is an attempt to avoid these hidden uses of strong choice...
But it is a mystery to me why people have overlooked that they were
using very strong choice principle. Well, it is the usual difference between
ideology and practice as it seems to me...

Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Jon Sterling]

Hi Thomas,

I think I see what you mean about global choice in classical math, but I don't think I agree overall. Things like connecting f.f.+e.s.o functors to equivalences in classical math do not require global choice when stated in the way that a careful classical mathematician understands (or is supposed to understand) them.

The statement is "There exists a mapping that takes any f.f.+e.s.o F : C -> D functor to a functor G : D -> F together with natural isomorphisms GF=1 and FG=1". This statement follows from "local" choice easily without making any global choices. I understand that you need global choice for this claimed function to form a 'definitional extension' of ZFC, but that is simply not what is meant by the original claim; it is for this reason that the practical formalisation of mathematics in ZFC emphasises consecutive conservative extensions and not only definitional extensions. Avoiding this distinction is one of the reasons that some people (like Hilbert and Bourbaki) have introduced global choice, but I must emphasise that essentially all the theorems of classical mathematics also work fine with only local choice. This is because the ground statements of classical mathematics are always propositional: when we want to introduce a construction, we describe the specification of that construction by means of a predicate, and then say that there exists something satisfying that predicate. After this, we work with an arbitrary thing satisfying that specification.

Likewise I do not agree with the discussion of geometric morphisms, for reasons that are identical to what I have mentioned above regarding weak and strong equivalences of categories.

For these reasons, I personally would not think of HoTT as an attempt to avoid hidden uses of strong/global choice, because the rest of classical mathematics (with the exception of Bourbaki) also does a perfectly fine job of avoiding global choice. (I'm not arguing against the convenience and utility of global choice though.)

Best,
Jon


On Tue, Feb 13, 2024, at 11:38 AM, Thomas Streicher wrote:
>> In fact, the reference shows that global choice really is inconsistent in HoTT. Univalence asserts (among other things) that all operations on the universe (even the universe of sets) are "natural" under equivalences, but a global choice operator cannot be natural in this sense.
>
> Thanks for this clarification!
>
> One needs global choice in CT for establishing that full and faithful
> functors which are essentially surjective are actually categorical
> equivalences.
> In practice you just have the stronger notion.
>
> In my eyes HoTT is an attempt to live with the weaker notion.
>
> In basic topos theory global choice is assumed when identifying
> inverse images of geometric morphisms with cocontinuous functors
> preserving finite limits. Therefore, I never believed that you can do
> topos theory in a weak meta theory without strong choice principles.
> At least not the way it is done in the traditional texts.
>
> Maybe HoTT is an attempt to avoid these hidden uses of strong choice...
> But it is a mystery to me why people have overlooked that they were
> using very strong choice principle. Well, it is the usual difference between
> ideology and practice as it seems to me...
>
> Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Thomas Streicher]

Hi Jon,

I didn't want to say that HoTT just wants to avoid global choice.

I also said that for most weak equivalences you meet the pseudoinverse
can be constructed. But for establishing this in general you need
global choice. Just look at the proof in MacLane or similar textbooks.

Or where do they prove that the assumption of a pseudo inverse is a
conservative extension without having a pseudo inverse at hand?

I do not believe that big choice is needed in down to earth mathematics.
I agree when applying general results to particular situations these
general principles can be mostly (always? but why?) eliminated.
But I do not know of any argument that for all functors between
Grothendieck toposes preserving finite limits and small colimits entails
the existence of a right adjoint.

These (unintentionally) strong principle have been introduced just for
convenience and later it has been found out that they have suprising
consequences.

Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Thomas Streicher]

Have sorted out off line with Jon Sterling what I meant.
I am working in ZFC together wit the axiom that every set is element
of a Grothendieck universe. So I do not use class choice at all but
instead choice in all Grothendieck universes.

What I meant is that one should not reduce choice to the first
universe but instead have it for all sets irrespective of the universe
they live in!

I always found this the most convient setting to work in. But not many
people do it. But if you work in it then there is no need for class
choice anymore.

Sorry for not having expanded my general implicit assumptions beforehand.
I do see that my view is not the majority view.

But it is the most convenient setting for doing category theory in my
eyes and it is weaker than real large cardinal axioms that set theorists
study consider.

Thomas



----------

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b

Re: Fibrewise opposite fibration

[Dusko Pavlovic]

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

[sorry, i always lag behind.]

a global well-order assumption is not a conservative extension even of ZFC.
it would make all models of computation extensional. it is also not a
conservative extension of the nice non-ZF universes we like these days,
including categorical, for basically the same reason.

my earlier point was that, since we live among computers, the assumption of
local well-ordering seems unavoidable, sooner or later.  for the simple
reason that all data and code are well-ordered as binaries. but the
ordering is not a property, either global or local, but structure. we keep
reordering things whenever we write a program. imposing a global ordering
structure would require deciding what is what: identifying the intensional
and the extensional equality. extensionally :)

you are probably right that all this is a sort of a religious war. or maybe
not a war, but rather a theological dispute. but note that theologians
considered it to be self-evident that they were the bearers of the torch of
logical truth. just like we.

if we assume that the world is built of sets, like we were taught in math
101, then assuming well-order is indeed questionable in all kinds of ways,
burdensome practically, and zermelo's solution to package it behind a big
quantifier is a convenient solution.

but while discussons whether the world is built of sets as the simplest
foundation of everything might be interesting, or not, programmers tend to
ignore them and only use sets when pedagogically unavoidable. the reason is
that all types in their world are well-ordered AND that transitioning to
sets and cardinalities is still as just costly as it was for cantor. so the
math that runs in the computers that we use to exchange these messages,
discuss foundations, and make calls home, tends to be built on well-ordered
types --- which we reorder and reprogram whenever needed. intensionally :)

2c
-- dusko


On Mon, Feb 12, 2024 at 6:56 PM Nath Rao <khazanarao@gmail.com> wrote:

> [This no longer about how to define fibrewise opposite fibration, so may
> be it is time t change the subject line.]
>
> IMHO, this seems to be more like a religious war. In "mathematics in the
> small", local axiom of choice allows us to choose representatives only
> when needed. So we are grew up believing that putting things in the
> definition that are not preserved by morphisms is "not done" (the
> religious dogma) . But them we run up against issues when we try to do
> the same thing in "mathematics in the large", and either ignore the
> problem or argue endlessly about how to solve it.
>
> Also, if are willing to assume that every set comes with a
> well-ordering, why not assume a global well-ordering and be done with
> it? [If I am going to use universes anyway, it seems to be trivial to do
> this, as long as I live inside a fixed universe in any given proof.] For
> ZFC, global choice is a conservative extension. Not being a logician, am
> not sure, but perhaps it can be shown for global choice is a
> conservative extension of local choice of 'all suitable set theories'.
> Then we can do global choice with no qualms.
>
> Regards
> Nath Rao
>
>
>
>
>
> ----------
>
> You're receiving this message because you're a member of the Categories
> mailing list group from Macquarie University.
>
> Leave group:
>
> https://url.au.m.mimecastprotect.com/s/IRyOC1WLjwsyM5vLTL23r1?domain=outlook.office365.com
>

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

Re: Fibrewise opposite fibration

[Dusko Pavlovic]

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

sorry, i first lag behind with reading, and then rush with writing before i
have read everything that was said. i hope the first paragraph of what i
wrote will reawake confusion. it is just a slight variation to what thomas
said more precisely. sorry about not reading first :) -- dusko

On Tue, Feb 13, 2024 at 9:16 AM Thomas Streicher <
streicher@mathematik.tu-darmstadt.de> wrote:

> Have sorted out off line with Jon Sterling what I meant.
> I am working in ZFC together wit the axiom that every set is element
> of a Grothendieck universe. So I do not use class choice at all but
> instead choice in all Grothendieck universes.
>
> What I meant is that one should not reduce choice to the first
> universe but instead have it for all sets irrespective of the universe
> they live in!
>
> I always found this the most convient setting to work in. But not many
> people do it. But if you work in it then there is no need for class
> choice anymore.
>
> Sorry for not having expanded my general implicit assumptions beforehand.
> I do see that my view is not the majority view.
>
> But it is the most convenient setting for doing category theory in my
> eyes and it is weaker than real large cardinal axioms that set theorists
> study consider.
>
> Thomas
>
>
>
> ----------
>
> You're receiving this message because you're a member of the Categories
> mailing list group from Macquarie University.
>
> Leave group:
>
> https://url.au.m.mimecastprotect.com/s/JYQgCE8wlRCr3MGkHNht4i?domain=outlook.office365.com
>

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

Re: Fibrewise opposite fibration

[Dusko Pavlovic]

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

CORR:
i hope the first paragraph of what i wrote will NOT awake confusion.


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: 2573 bytes --]

Re: Fibrewise opposite fibration

[Dusko Pavlovic]

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

it occurs to me that i have been preaching the helpfulness of the
well-ordering of all data in the world, as demonstrated by its utility to
the programmers --- and i totally forgot to mention its utility as a
*categorical structure*!!  i forgot to plug my own work which provides the
categorical underpinning for the well-ordering sermon...

so we all love the **cartesian closed categories**, characterized by the
adjunction
CC(XxA,B) ~ CC(X, A=>B)           (*)

but the cccs are *extensional* universes, corresponding to the extensional
type theories. if we want to capture the world with actual programs, say in
a programming language P, then we have just a family of X-natural
surjections
CC(XxA,B) <<--- CC(X, P)             (#)
the surjections say that every computably X-indexed family of computable
functions from A to B can be programmed by a computably X-indexed family of
programs in P. since computable functions don't always halt, we cannot
avoid at least the computational effect of nontermination, and the AxB is
not a product but a tensor, say from a commutative computational monad.
such (symmetric) monoidal categories with a "programming language" type P
and natural surjections (#) is what i called *monoidal computers*, because
you can program everything using (#), without ever saying anything else
about the programming language. it is turing complete. it's all spelled out
in my book.

but the snag is that (*) is a *property* of a category, whereas (#) is a
structure. a category can be cartesian closed in only one way, but it can
be a monoidal computer in many ways. one is tempted to say that this is
unavoidable since the CT thesis leaves us with many models of computation
and infinitely many unnatural isomorphisms between any two.

**** enter the well-order ****

IF you remember that programming languages are well-ordered, and assume
that the type P carries a well-ordering,
THEN (#) becomes a *property*. a monoidal category CC can have at most one
well-ordered type P with (#), up to isomorphism.

the nices thing is that you prove this by spelling out what came to be
called the cantor-bernstein theorem, but in cantor's way: using the
well-order. (dedekind discouraged publishing this because the well-ordering
of the reals was cantor's by far the deadliest mortal sin. even now, to
really keep the reals well-ordered you need something like levin's
dovetailing approximations...)

anyway, this proof is in Ch 8 of my book *programs as diagrams*.
computability is a *categorical property* --- IF you take into account that
the programming language is well-ordered (which implies that all checkable
types are).

sorry about plugging my book. i know it's a world of tweets and advertising
campaigns but i still feel bad. my alibi is that the fact that
computability+well-order is a categorical property is way more important
than any book and surely goes deeper than i can comprehend no matter how
many turing degrees and oracles i consult...

(can't believe that i only remembered to mention this after like 5 posts...)

-- dusko



On Thu, Feb 22, 2024 at 3:42 PM Dusko Pavlovic <duskgoo@gmail.com> wrote:

> [sorry, i always lag behind.]
>
> a global well-order assumption is not a conservative extension even of
> ZFC. it would make all models of computation extensional. it is also not a
> conservative extension of the nice non-ZF universes we like these days,
> including categorical, for basically the same reason.
>
> my earlier point was that, since we live among computers, the assumption
> of local well-ordering seems unavoidable, sooner or later.  for the simple
> reason that all data and code are well-ordered as binaries. but the
> ordering is not a property, either global or local, but structure. we keep
> reordering things whenever we write a program. imposing a global ordering
> structure would require deciding what is what: identifying the intensional
> and the extensional equality. extensionally :)
>
> you are probably right that all this is a sort of a religious war. or
> maybe not a war, but rather a theological dispute. but note that
> theologians considered it to be self-evident that they were the bearers of
> the torch of logical truth. just like we.
>
> if we assume that the world is built of sets, like we were taught in math
> 101, then assuming well-order is indeed questionable in all kinds of ways,
> burdensome practically, and zermelo's solution to package it behind a big
> quantifier is a convenient solution.
>
> but while discussons whether the world is built of sets as the simplest
> foundation of everything might be interesting, or not, programmers tend to
> ignore them and only use sets when pedagogically unavoidable. the reason is
> that all types in their world are well-ordered AND that transitioning to
> sets and cardinalities is still as just costly as it was for cantor. so the
> math that runs in the computers that we use to exchange these messages,
> discuss foundations, and make calls home, tends to be built on well-ordered
> types --- which we reorder and reprogram whenever needed. intensionally :)
>
> 2c
> -- dusko
>
>
> On Mon, Feb 12, 2024 at 6:56 PM Nath Rao <khazanarao@gmail.com> wrote:
>
>> [This no longer about how to define fibrewise opposite fibration, so may
>> be it is time t change the subject line.]
>>
>> IMHO, this seems to be more like a religious war. In "mathematics in the
>> small", local axiom of choice allows us to choose representatives only
>> when needed. So we are grew up believing that putting things in the
>> definition that are not preserved by morphisms is "not done" (the
>> religious dogma) . But them we run up against issues when we try to do
>> the same thing in "mathematics in the large", and either ignore the
>> problem or argue endlessly about how to solve it.
>>
>> Also, if are willing to assume that every set comes with a
>> well-ordering, why not assume a global well-ordering and be done with
>> it? [If I am going to use universes anyway, it seems to be trivial to do
>> this, as long as I live inside a fixed universe in any given proof.] For
>> ZFC, global choice is a conservative extension. Not being a logician, am
>> not sure, but perhaps it can be shown for global choice is a
>> conservative extension of local choice of 'all suitable set theories'.
>> Then we can do global choice with no qualms.
>>
>> Regards
>> Nath Rao
>>
>>
>>
>>
>>
>> ----------
>>
>> You're receiving this message because you're a member of the Categories
>> mailing list group from Macquarie University.
>>
>> Leave group:
>>
>> https://url.au.m.mimecastprotect.com/s/en1jCANpnDCyZOvyTGnciw?domain=outlook.office365.com
>>
>

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