Hey, are there any other known proofs of straightening for infty-cat-valued functors? I know of Lurie's version and there is a short paper by Boavida that proves it a somewhat different way

I know of ~6 proofs for the space-valued functors

some people here are working on another version of marked straightening, but I'm not too familiar with the literature. There is a paper by Haugseng, Nikolaus, and someone else that proves an alternative version works, assuming straightening

has anyone tried to see if this can be worked out at the model category level?

In the paper I'm talking about, they show that Cart(S) is equivalent to the infty cat of algebras for a free fibration monad then construct a weight for oplax colimits and show the weighted colim is equivalent to unstraightening, but it's all done in infty cats rather than model cats

@HarryGindi are you aware of this arxiv.org/abs/1512.04815 ?

"Subsequent to the posting of the first version of the paper to the arXiv, the pre-print [13] [=Heuts–Moerdijk] appeared which also gives a new proof of the straightening theorem as well as a result analogous to Theorem 1.4 above.

Our work complements [13] in the following ways: firstly, our methods are quite different to those of [13] and lead to what we believe is also a fairly conceptual proof of the straightening theorem; secondly, our work has the virtue of being self-contained, in particular ..."

@GijsHeuts . I was aware Heuts-Moerdijk I and II, but if possible I'm wondering if it's possible to avoid markings by showing that the weighted colimit lands in an honest model category of algebras for the slice monad. Those papers are very nice though and definitely in the direction I'm thinking about.

@DavidRoberts Nope, I'll check it out though!

My hope is that there is some kind of canonical algebra structure on the weighted colimit if you can find a very specific model for the weight.

@GijsHeuts I'd definitely be pleased to see the update even with markings though!

To make my idea precise, given a simplicial set S, there is a slice of the Joyal model structure to sSet/S and a nice monad (-)x_S S^{\Delta^1} on sSet/S. There should be a simplicial model cat of algebras for this monad.

So the question is: Can you choose a weight C[S]^op-> sSet such that the weighted colimit lands in that category of algebras on the nose

Nikolaus and Haugseng and the other coauthor show this up to weak equivalence, but yeah, it depends on Lurie's machinery already

A proof that doesn't use markings would be ideal because I know what this monad is for infty,n-categories (it uses the lax version of S^{\Delta^1}), but computing an explicit marking for this thing looks really difficult)

the lax inner hom is already horrible, and giving explicit markings everywhere looks intractable