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 | Leave group | Learn more about Microsoft 365 Groups