Re: Fibrewise opposite fibration

["Jon Sterling" <jon@jonmsterling.com>]

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