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 $\infty Cat \to \widehat{\infty Cat}$ from small $\infty$-categories to large $\infty$-categories given as follows:
Lurie defines $P$ pointwise by setting $P(C) = Fun(C^{op}, \infty Gpd)$, so the content of the first bullet point is to make it into a functor.
These two functors are closely related; for any functor $f : C \to D$, Proposition 5.2.6.3 of Higher Topos Theory proves that $P(f) \dashv R(f)$.
Let $\overline{el}(R) \to \infty Cat$ be the cartesian fibration classified by $R$. This is a presentable fibration, so it is also a cocartesian fibration that is classified by a covariant functor $R^{ladj}$.
It’s clear $P$ and $R^{ladj}$ 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 $P$ is defined?
Here’s a concrete conjecture.
Let $F : C^{op} \to \infty\!Cat$ and $G : C \to \infty\!Cat$. Suppose:
I conjecture that this data can be extended to a natural equivalence $G \simeq F^{ladj}$, where $F^\ladj$ is the functor constructed from $F$ 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 $p : X \to C$ such that $p$ is both a cocartesian fibration classified by $G$ and a cartesian fibration classified by $F$. 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 $F$ and $G$ 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