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.) 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=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>