Michael wrote:

> Basically, the theorem proved that \$$\mathcal{C}\$$ and \$$\mathrm{str}(\mathcal{C})\$$ are equivalent by showing there are two functors that are inverses between them.

Close but not quite. These two functors are just 'weak' inverses. This is a great excuse to talk about an important issue.

Suppose in general we have two functors \$$F \colon \mathcal{A} \to \mathcal{B}\$$ and \$$G \colon \mathcal{B} \to \mathcal{A} \$$ with

$G F = 1_{\mathcal{A}} , \qquad F G = 1_{\mathcal{B}}$

Then we say \$$F\$$ and \$$G\$$ are **inverses**, and the categories \$$\mathcal{A}\$$ and \$$\mathcal{B}\$$ are **isomorphic**.

In this case \$$\mathcal{A}\$$ and \$$\mathcal{B}\$$ look exactly alike except for the names of objects and morphisms: we've got a one-to-one correspondence between their objects, and a one-to-one correspondence between their morphisms which sends identities to identities and preserves composition.

But now suppose we have two functors \$$F \colon \mathcal{A} \to \mathcal{B}\$$ and \$$G \colon \mathcal{B} \to \mathcal{A} \$$ with natural isomorphisms

$\alpha \colon G F \Rightarrow 1_{\mathcal{A}} , \qquad \beta \colon F G \Rightarrow 1_{\mathcal{B}}$

Then we say \$$F\$$ and \$$G\$$ are **weak inverses**, and the categories \$$\mathcal{A}\$$ and \$$\mathcal{B}\$$ are **equivalent**.

In this case there's no need for \$$\mathcal{A}\$$ and \$$\mathcal{B}\$$ to have the same number of objects, or morphisms. And yet, it turns out that equivalent categories are "the same for all practical purposes" - practical according to category theory, that is!

For example, \$$\mathcal{A}\$$ could have infinitely many objects, with exactly one morphism from any object to any other object, while \$$\mathcal{B}\$$ could be \$$\mathbf{1}\$$, with exactly one object and one morphism. These categories are not isomorphic, but they are equivalent. In fact \$$\mathcal{B}\$$ is skeletal, and every category is equivalent to a skeletal category.

Mac Lane's strictification theorem is also a way of finding a 'nicer' category (namely a strict monoidal one) that's equivalent (in fact monoidally equivalent) to one you started with (namely any monoidal one). But Mac Lane's theorem does the opposite of making your category skeletal! It takes your category and throws in _more_ objects... all isomorphic to ones you had already.