cycle construction for symmetric monoidal categories

[Alizter]

In this PR, we introduce what I've termed the "cycle construction" for symmetric monoidal categories. Like the "twist construction" it is a slicker way to build symmetric monoidal categories without having to give all the data from the beginning. But this time, instead of asking for a twist map ABC -> BAC we ask for a cycle map ABC -> CAB. We then have variants of the hexagon and pentagon axioms which appear to be slicker than in the twist construction.

TODO

• more comments
• use somewhere?

[jdchristensen]

This is great! Do you think it can be used to prove that Join satisfies the pentagon law? That would be helpful for something I'm working on.

[Alizter]

@jdchristensen I don't recall off the top of my head, but you are more than welcome to try!

[jdchristensen]

@Alizter Do you have any partial work on the pentagon law for Join, either using the current twist approach to associativity or the cycle approach added in this PR? I vaguely recall that you worked on it.

[Alizter]

@Alizter Do you have any partial work on the pentagon law for Join, either using the current twist approach to associativity or the cycle approach added in this PR? I vaguely recall that you worked on it.

I can't find anything about joins, but I have some partial work on instantiating these constructions with the smash product.