8:32 PM
Hey @RuneHaugseng suppose I've got a cocartesian fibration E→B and B has a terminal object x. Then for the fiber over b∊B there's a cocartesian lift E_b→E_x. Can I use the fact that E is the oplax colimit of a functor B→Cat_∞ to conclude that these assemble into a functor E→E_x?
Like, is this something I get for free from the universal property?
(full disclosure, Denis has given me another argument for why I get such a functor, but I was wondering if there was something slick one could do with the oplax colimit stuff)