@YuriSulyma you’re welcome to do some house cleaning. it looks like “other books” is a decent target, but less so misc: sort the files by size to see what’s actually going to improve the situation

Does anyone know a reference that proved, in detail, that giving a monoidal category is equivalent to giving a Grothendieck opfunctor over \Delta^op satisfying the Segal condition?

@Dedalus so I think that this is (to some extent) proven in my paper with Liang Ze Wong, in the setting of simplicially enriched monoidal categories, but of course you can just take something with a discrete simplicial enrichment. arxiv.org/pdf/1808.08020.pdf

(also that's in the strict case, but this isn't a big deal because any monoidal category can be rigidified to a strict monoidal category up to monoidal equivalence)

cf. basically Prop 4.1.4 and the things that follow it

it relies on an enriched version of the grothendieck construction, which, again, restricts to the unenriched version if you take a discrete enrichment

Although I guess we don't really say anything explicitly about the Segal condition. You could restrict to subcategories on both sides though and I think prove your statement pretty easily, as the equivalence is described explicitly.

Thanks! I want a reference of the fact that if we have a Grothendieck opfibration over \Delta^op, then the pentagon axiom holds.

@Dedalus the pentagon axiom follows immediately from a certain equality inside of the hom-set $hom_{\Delta^{op}}([4],[1])$

@AaronMazel-Gee I agree that is the way to do it, but when I do it I get something quite messy. One works out the different factorizations of the map [1] \to [4] etc. It is clear what to do, but messy (at least when I write it down carefully). Is this what you meant by immediate?

@Dedalus well, that is the argument i was referring to (and i couldn't imagine a fundamentally different argument); but as for whether it's messy, i guess that depends what you're taking as given. one subtlety here is that an opfibration over C only determines a functor C --> Cat up to natural equivalence.

this is starting to get out of my wheelhouse, but you might be interested in the notion of a "cloven opfibration", which is essentially an opfibration equipped with choices of cocartesian morphisms (which are a priori only well-defined up to a contractible groupoid of choices). every opfibration admits a cleaving, and if i recall correctly, this gives you a well-defined choice of straightening at the point-set level.