12:15 AM
@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

19 hours later…
7:36 PM
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?

8:05 PM
@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.

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

9:51 PM
@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?

2 hours later…
11:36 PM
@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.
if you are working homotopy-coherently, you can just say that the functor $\bDelta^{op} \to Cat$ takes this equality to a natural isomorphism (a path in a hom-space), but if you want to think about categories at the point-set level (i.e. having a set of objects, etc.) then you may have to be more careful, and indeed things may get messy.
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.