Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
tried to give the references to online resources more canonical and more informative formatting: how about doing pointers to Kerdodon like this (with an eye towards their own request here on how to cite them):
- Jacob Lurie, chapter 5 Fibrations of ∞-Categories (2021) in: Kerodon
added pointer to:
Here’s a subtle issue in my construction of the universal cocartesian fibration that I’m wondering if there is an easy solution to.
Consider two functors from small -categories to large -categories given as follows:
Lurie defines pointwise by setting , so the content of the first bullet point is to make it into a functor.
These two functors are closely related; for any functor , Proposition 5.2.6.3 of Higher Topos Theory proves that .
Let be the cartesian fibration classified by . This is a presentable fibration, so it is also a cocartesian fibration that is classified by a covariant functor .
It’s clear and agree strictly objects and up to equivalence on arrows… but I realize now I have a gap in that I don’t actually know there is a natural equivalence between them. Is there any easy or general method for arriving at that conclusion from that sort of method? Or does closing this gap rely more on diving into the specifics of how is defined?
Here’s a concrete conjecture.
Let and . Suppose:
I conjecture that this data can be extended to a natural equivalence , where is the functor constructed from by reversing the action on arrows via taking left adjoints. To be more precise, I claim this data can be used to produce a bundle such that is both a cocartesian fibration classified by and a cartesian fibration classified by . I probably want to include some consistency constraint with the specified adjunctions as well.
The reason that there is hope that it is enough to observe the relationship between how and act on arrows is that uniqueness of adjoints might be able to fill in the rest of the missing data. This seems like a mess to actually work through, though.
Where the universal left fibration was mentioned (here), I have added pointer also to
added these pointers:
Discussion of straightening and unstraightening entirely within the context of quasi-categories:
which (along the lines of the discussion of the universal left fibration from Cisinski 2019) allows to understand the universal coCartesian fibration as categorical semantics for the univalent type universe in directed homotopy type theory:
(see video 3 at 1:16:58 and slides 3.33).
1 to 10 of 10