The n-Category Café

Strict2Cat = [strict 2-categories, strict 2-functors, strict natural transformations, modifications]

Weak2Cat = [weak 2-categories, weak 2-functors, weak natural transformations, modifications]

Gray = [strict 2-categories, strict 2-functors, weak natural transformations, modifications]

We have inclusions of weak 3-categories: Strict2Cat → Gray → Weak2Cat: and Lack shows, not only that the second inclusion fails to be an equivalence, but that there’s no equivalence between Gray and Weak2Cat.

But to be fair, there’s another possibility intermediate between Gray and Weak2Cat:

Toby = [strict 2-categories, weak 2-functors, weak natural transformations, modifications]

Except nobody is ever going to talk about the 3category Toby, because it is equivalent to Weak2Cat!

And that’s why everybody kept citing some comment of Bénabou’s, to the effect that the really important thing was not weak 2categories (which he invented) but weak 2functors (which I guess he also invented at the same time, at least in full generality).

Model category theory formalizes this by speaking of a category C equipped with a classes of morphisms called “weak equivalences”. We can formally invert these and get a new category Ho(C) where the weak equivalences are isomorphisms: this is called the “homotopy category” or “derived category” of our model category. But this loses information, so it’s often good not to do this.

But since we have a notion of homotopy of homotopies of … in a model category, what we really ought to do is insert these inverses, but declare them inverses only up to a homotopy (an invertible 2morphism, which we insert), and this is invertible only up to a homotopy of homotopies (an invertible 3morphism, which we insert), and so on. I’m unsure to what extent the resulting (∞,1)category has lost information.