According to the [periodic table of k-tuply monoidal n-categories](http://ncatlab.org/nlab/show/k-tuply+monoidal+n-category), it should be the case that a tetracategory (= weak 4-category) with one object, one 1-morphism and one 2-morphism is effectively equivalent to a symmetric monoidal category. I understand geometrically why one should expect this, but I cannot see how it arises directly from an algebraic definition of tetracategory.


I do know how we get a *braided* monoidal category: if $X$ and $Y$ are 3-morphisms, then the braiding $\gamma\_{X,Y}$ is defined as the interchanger of $X$ and $Y$. What one then needs to show is that $\gamma\_{X,Y} \circ \gamma\_{Y,X} = \text{id}$. My understanding is that one would not expect an algebraic definition of tetracategory to carry this equation explicitly as an axiom; it would have to be derived.


I am aware that, of course, there does not exist a stable easily-referenced definition of tetracategory. (*Edit: John Baez links below to an explicit definition due to Todd Trimble, written up by Alex Hoffnung.*) I would be happy if someone could give me an answer along the lines of ''this is the sort of way a tetracategory should be defined, and one would reasonably expect it to have such-and-such algebraic data associated to it, and hence $\gamma\_{X,Y} \circ \gamma \_{Y,X} = \text{id}$ would follow in such-and-such a way."



Why does a tetracategory with one object, one 1-morphism and one 2-morphism give a symmetric monoidal category
It will come from a compatibility between different ways of composing interchangers.


(I'm going to use = to mean iso/homotopy in a HoTT-like way throughout, for ease of notation. I will also confuse proofs and homotopies throughout.)


To get a better intuition, let's first think about the case of higher groupoids. As a warmup let's think about the braided case first. So there we have a homotopy 3-type which is 1-connected and we want to understand why there's a braiding on 2-loops. (Note that universally it's enough to just do this for the sphere $S^2$, so secretly we're trying to understand $\pi\_3(S^2)$.) But, as you know, this is just the usual Eckmann-Hilton argument where we just braid the maps around each other. Translating this into compositions turns into the interchange law because the first half of the argument is:
$$x \circ\_1 y = (x \circ\_2 1) \circ\_1 (1 \circ\_2 y) = (x \circ\_1 1) \circ\_2 (1 \circ\_1 y) = x \circ\_2 y.$$
Note carefully that there are actually two proofs of Eckmann-Hilton: one where you rotate clockwise and one where you rotate counterclockwise. These proofs are different and they correspond to the two generators of $\pi\_3(S^2) = \mathbb{Z}$. It is the fact that these two proofs of Eckmann-Hilton are different that makes these categories braided and not symmetric.


Alright, now let's move up one dimension higher. Now we're looking at 2-connected 4-groupoids. Now the algebraic topology question is the well-known fact that the generator of $\pi\_3(S^2) = \mathbb{Z}$ has only order 2 when you stabilize it to put it in $\pi\_4(S^3)$. Where does this come from? Well, it's clearly the same thing as asking why the two proofs of Eckmann-Hilton become the same when applied to 3-loops. Here the topological intuition is clear: take your clockwise proof and rotate it around the x-axis until it comes back into the plane becoming the counterclockwise proof.


Let's think about this in more detail. You can think of Eckmann-Hilton as taking place on a big square made up of four little squares with two tiles labelled x and y and the blanks labelled by identities and then sliding them around. Now we're looking in 3-dimensions at cubes and we want to slide one proof into the other by moving into the third dimension.


So we start with the proof:
$$x \circ\_1 y = (x \circ\_2 1) \circ\_1 (1 \circ\_2 y) = (x \circ\_1 1) \circ\_2 (1 \circ\_1 y) = x \circ\_2 y = \ldots = y \circ\_1 x.$$
Next we need to introduce a third dimension to give ourselves more room to work. So maybe:
$$x \circ\_1 y = (x \circ\_2 1) \circ\_1 (1 \circ\_2 y) = (x \circ\_1 1) \circ\_2 (1 \circ\_1 y) = ((x \circ\_1 1) \circ\_2 (1 \circ\_1 y)) \circ\_3 ((1 \circ\_1 1) \circ\_2 (1 \circ\_1 1)) = \ldots$$
Then one gradually moves the clockwise proof around into the third dimension (so the interesting part is in the $\circ\_2$ $\circ\_3$ plane instead of the $\circ\_1$ $\circ\_2$ plane) and then back into the plane until it becomes the counterclockwise proof. I'm not going to write down the rest of this proof because it would take a while to get it entirely right and it would be hard to fit nicely on the screen anyway. But I'm confident that given a couple days I could write such a proof in Agda, and hopefully the idea is clear.


Just like the key lemma in proving Eckmann-Hilton is the interchange law, in order to prove this result we're going to need a higher interchanger relating the three compositions and their pairwise interchangers. Once you have such a higher interchanger the above proof should work for any doubly monoidal 4-category without groupoid-ness appearing anywhere.


