Re: Fibrewise opposite fibration

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

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