You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Not literally!
I have a big 3d commuting diagram, of shape the face poset of a 3-cube (so: 1 body vertex, 6 face vertices etc). It commutes on the nose, but it is a diagram in a bicategory. Really it's a diagram in the 1-category underlying a 2-category, and then there is a functor including the 2-category into the bicategory. Ultimately I need to build a 2-commuting cube with all the paths starting at one vertex and going to an opposite vertex. But the face poset has all the arrows only point from higher to lower dimensions. Here's the outside of the poset
All of the arrows are weakly invertible in the bicategory, and so I can turn around all the "wrong-way" ones using adjoint inverses, and then all the commuting squares with wrong-way edges turn into their mates, which now only commute up to an invertible 2-arrow.
Now I presume the calculus of mates then guarantees that the resulting pasting diagram (I'm relying on strictification/coherence theorems here) indeed gives me a cube whose faces are 2-arrows such that the cube 2-commutes. Is this right? Is it a standard thing I can just say?
I think this should follow from knowing that for the case of a single (2-)commutative cube, and adjunctions/adjoint inverses for all the edges in a given direction, then the mates paste together into a 2-commutative cube. But this follows, I believe, from the functoriality of the mate construction with respect to vertical and horizontal pasting. Excellent!