@Dedalus I'm not aware of Nguyen's work; where is it found?. Cisinski has a very nice formulation for left/right fibrations; If he has one for cartesian/cocartesian fibrations I'm not aware of it. Riehl&Verity have an approach for cartesian/cocartesian fibrations, though not all details are available (some of it is here: arxiv.org/abs/1706.10023 ).

I'd guess Lurie's version is still needed, since no other formulation is in print (to my knowledge).

Ultimately, you want to have a setup that lives entirely in quasicategories, and does not require thinking about other model categories (like the model category of simplicially enriched categories). [Note: you will need to deal with simplicially enriched categories a little bit, since qCat is one.]

@CharlesRezk I should clarify that the work on cocartesian fibrations is done by Nguyen, however, it is very inspired by Cisinski’s work.

epub.uni-regensburg.de/38448/1/nguyen_thesis.pdf is the thesis

In 3.4 he constructs a universal cocartesian fibration. Thus I am curious, what more does Lurie’s approach give us? (I know quite little about this subject, so some of this is probably very naive)

@Dedalus Just glancing through, it looks like they construct a universal cocartesian fibration, but I don't see that it's obvious this is homotopical; for instance, that their quasicategory Q of quasicategories is equivalent to any other quasicategory of infinity categories.

@Dedalus Unless I'm misunderstanding, Nguyen proves something like an equivalence between the homotopy category of cocartesian fibrations over X and the homotopy category of functors from X to quasi-categories. This is a far cry from showing that the infty-categories are equivalent. One issue with the Cisinski/Nguyen setup is that we don't appear to actually get straightening/unstraightening functors between the infty-category Fun(X, Cat_infty) and the infty-category coCart(X)- just

a correspondence between objects on either side

The issue is always that Cat_infty is playing both an "external" and "internal" role in the statement of straightening/unstraightening... so it's hard to imagine a purely "internal" proof without maybe some kind of axiomatization of (infty,2)-categorical things

I see. Thanks for the comments!

@DylanWilson I don't understand the objection about functors. Does Lurie produce functors between the quasicagory $\mathrm{Fun}(X, \mathrm{Cat}_\infty)$ and the quasicategory $\mathrm{coCart}(X)$?

@DylanWilson For an individual X, an equivalence ho(Fun(X,Cat_infty)) = ho(coCart(X)) isn't much, but maybe having an equivalence for all X can be improved to equivalences without the ho(_)? (It feels possible, but if it were easy they would have done it, I guess.)

Can someone remind me of the proof that if $p\colon C\to S$ is an inner fibration of simplicial sets, then every degenerate edge of $C$ is $p$-Cartesian?

@CharlesRezk yes: he produces a quillen equivalence between two model categories with those as their underlying infty-categories.

I think the intuition behind Lurie's argument runs as follows: Start with $p: X \to S$. You want to define functorial pullbacks, but that involves a choice. So first, get rid of the choice: replace $X$ with a new category whose objects over $s$ look like $(x, s \to px)$, and then the 'pullback along $t \to s$' is given by precomposing. There are two issues: (1) this new category is nothing like the old one, and (2) composition itself is not strictly functorial in quasicategories

To fix (2) Lurie builds a simplicial category that models that replacement, and then marks some edges (which is like inverting those maps) to fix (1).

That's the straightening functor. If you could somehow implement this procedure without using simplicial categories, then you'd be in business.

I think that Cisinski gives a functorial equivalence of infinity categories between a category of left fibrations over A and the category of functors from A to infinity groupoids. But even the same could be done for cocartesian fibrations, this would fall short of what Lurie does?

@Dedalus Last thing I know, is that Cisinski is trying to adapt the technique to cocartesian fibrations (thus recovering Lurie's theorem) but he's not quite there yet. But stuff might have changed in the meantime

@DylanWilson I'm aware Lurie gives a Quillen equivalence, which is not what I asked. I want a map between the two simplicial sets which is a categorical equivalence. Presumably that such a map exists is implicit given the Quillen equivalence, but nowhere do I see Lurie write down such a map (or a zig-zag that realizes one).

@CharlesRezk This is not true in general. The op-dual of the morphism $f : \Delta^1 \to S$ in 1904.04965 is a counterexample: $f$ is an inner fibration, but the degenerate edge $00$ in $\Delta^1$ is not $f$-cocartesian. It is of course true if the base is a quasi-category, in which case it is a special case of Joyal lifting.

@AlexanderCampbell Oh really? That seems like it will cause a problem for the theory of Cartesian fibrations over non-quasi-categories.

@CharlesRezk I shouldn't think so; I see it instead as a shortcoming of the class of inner fibrations. If $p \colon C \to S$ is not merely an inner fibration, but also has the right lifting property with respect to all monic bijective-on-0-simplices weak categorical equivalences, then every degenerate edge of $C$ is $p$-cartesian and $p$-cocartesian.