ericfinster / catt.io

Revised Omega-categorical Typechecker
24 stars 3 forks source link

Gordon, Power, and Street's weak equivalence between Gray-categories and tricategories? #15

Open eternaleye opened 3 years ago

eternaleye commented 3 years ago

I just watched the HoTTest presentation @jamievicary gave in December, and Emily Riehl's question (and the answer) brought to mind that there may be a (ready-made) proof of a stronger weak equivalence than the one stated as WIP in the talk, which might get you both strict unitality and strict associativity.

Specifically, in "Coherence for tricategories", Gordon, Power, and Street show that Gray-categories (which are strict in everything except interchange, as the answer mentioned) are weakly equivalent to tricategories.

I'm just an interested hobbyist, so I don't know if this has already been considered and is unsuitable in some way, but I thought I'd bring it up.

EDIT: On consideration, it may be that what's missing is the generalization to higher n, and perhaps the proof doesn't generalize straightforwardly - I could certainly see how that could be the case.

jamievicary commented 3 years ago

Hello Eternaleye, yes you've got it right in your edit. Our work gives a definition of strictly unital n-category, which we could in principle extend to a definition of strictly associative and unital n-category, which we might expect to agree with Gray categories for n=3. It's a very reasonable conjecture that every weak n-category is equivalent to a strictly unital and associative n-category, and Gordon, Power and Street's work could be useful to see how to prove this for n=3. But it is unlikely to give a complete guide to the proof for general n.

That's not to say Gordon, Power and Street's work is not relevant here, quite the contrary --- it is a deep inspiration for the entire research project.