Michael wrote:

> It seems like there should be a skeletal category lurking in there since we are collapsing all isomorphic objects into one object.

No, we're not. The actual proof of Mac Lane's strictification theorem proceeds by creating tons _more_ isomorphic objects. You start with a monoidal category \\(\mathcal{C}\\). Then you create a new monoidal category \\(\mathrm{str}(\mathcal{C})\\) whose objects are _lists_ of objects in \\(\mathcal{C}\\). The tensor product of two lists

$$ (c_1, \dots, c_m) $$

and

$$ (d_1, \dots, d_n) $$

is the list

$$ (c_1, \dots, c_m, d_1, \dots, d_n )$$

It's easy to see that this tensor product is strictly associative. A morphism in \\(\mathrm{str}(\mathcal{C})\\) from

$$ (c_1, \dots, c_m) $$

and

$$ (d_1, \dots, d_n) $$

is defined to be a morphism

$$ f \colon c_1 \otimes (c_2 \otimes (c_3 \otimes \cdots )) \to d_1 \otimes (d_2 \otimes (d_3 \otimes \cdots )) $$

in \\(\mathcal{C}\\).

It takes some work to make \\(\mathcal{C}\\) into a monoidal category and show that \\(\mathrm{str}(\mathcal{C})\\) is monoidally equivalent to \\(\mathcal{C})\\).

But my point here is \\(\mathrm{str}(\mathcal{C}\\) is not skeletal! In this category

$$ (c_1, \dots, c_m) $$

and

$$ (d_1, \dots, d_n) $$

are isomorphic iff

$$ c_1 \otimes (c_2 \otimes (c_3 \otimes \cdots )) $$

and

$$ d_1 \otimes (d_2 \otimes (d_3 \otimes \cdots )) $$

are isomorphic in \\(\mathcal{C}\\). That happens a whole lot! For example, the two-element list

$$ (c_1,c_2) $$

is isomorphic to the one-element list

$$ (c_1 \otimes c_2) .$$

> It seems like there should be a skeletal category lurking in there since we are collapsing all isomorphic objects into one object.

No, we're not. The actual proof of Mac Lane's strictification theorem proceeds by creating tons _more_ isomorphic objects. You start with a monoidal category \\(\mathcal{C}\\). Then you create a new monoidal category \\(\mathrm{str}(\mathcal{C})\\) whose objects are _lists_ of objects in \\(\mathcal{C}\\). The tensor product of two lists

$$ (c_1, \dots, c_m) $$

and

$$ (d_1, \dots, d_n) $$

is the list

$$ (c_1, \dots, c_m, d_1, \dots, d_n )$$

It's easy to see that this tensor product is strictly associative. A morphism in \\(\mathrm{str}(\mathcal{C})\\) from

$$ (c_1, \dots, c_m) $$

and

$$ (d_1, \dots, d_n) $$

is defined to be a morphism

$$ f \colon c_1 \otimes (c_2 \otimes (c_3 \otimes \cdots )) \to d_1 \otimes (d_2 \otimes (d_3 \otimes \cdots )) $$

in \\(\mathcal{C}\\).

It takes some work to make \\(\mathcal{C}\\) into a monoidal category and show that \\(\mathrm{str}(\mathcal{C})\\) is monoidally equivalent to \\(\mathcal{C})\\).

But my point here is \\(\mathrm{str}(\mathcal{C}\\) is not skeletal! In this category

$$ (c_1, \dots, c_m) $$

and

$$ (d_1, \dots, d_n) $$

are isomorphic iff

$$ c_1 \otimes (c_2 \otimes (c_3 \otimes \cdots )) $$

and

$$ d_1 \otimes (d_2 \otimes (d_3 \otimes \cdots )) $$

are isomorphic in \\(\mathcal{C}\\). That happens a whole lot! For example, the two-element list

$$ (c_1,c_2) $$

is isomorphic to the one-element list

$$ (c_1 \otimes c_2) .$$