search

jamievicary / globular

Globular
37 stars 9 forks source link

Snake equations for invertible cells #41

Open cdgls opened 8 years ago

cdgls commented 8 years ago

The interchanger at the moment does not satisfy the snake equation, but life would be better if it did. We are actually encountering this as an obstruction to simplifying diagrams when attempting to prove things.

jamievicary commented 8 years ago

This is more general than interchangers: it should be implemented for all invertible cells.

This is the first level of coherent structure. At the next level there is the swallowtail equation (and a lot more); at the level after that there is the butterfly equation (and an awful lot more.) I'm not sure it's reasonable to add all those.

cdgls commented 8 years ago

Maybe it could be done one step at a time --- first snake equation for the invertible cells, then worry about more later as it arises.

mlharaujo commented 6 years ago

I would be good to at least have the snake equation for the interchangers. In principle, if one is creating invertible cells, it's possible to create an inverse and put in the coherence equations by hand to get around this issue. But for the interchanger this is not possible, since it is part of the underlying structure. This has the consequence that some equations which should be true in any 4-category are not true in globular.

jamievicary commented 6 years ago

Hi Manuel, thanks for your comment and your interest in this project. Three things come to mind. Firstly, you can indeed add generators to your signature to allow interchanger snake cancellation. It's far from ideal, as you would have to add it for every distinct instance of the interchanger snake that you want to cancel, but it's possible in principle, and gives a way to handle this issue. Secondly, although I completely agree this should have been there all along, adding this feature to the current version of Globular would be quite intricate and time-consuming. Thirdly, the next version of Globular is well into development, which will allow arbitrary (infty,infty)-computations, including in particular snake equations for interchangers. So, I encourage you to use the workaround I'm suggesting, and hold tight for Globular 2.0!