jamievicary
commented
8 years ago This is an interesting idea, which Dominic and I discussed at some length. I see where this is coming from: when building big proofs, especially in a 4-category, the vast majority of what you can see are interchangers, which often 'get in the way' of seeing what's really going on geometrically.
However, the vast majority of the actual axiom steps that you need to apply in these situations directly involve the interchangers. So I think that most of the time, although they're annoying, they're an annoyance you need to deal with.
The most time-consuming thing about Globular at the moment is playing with the interchangers. At present, at every level Globular treats interchangers as natural isomorphisms rather than identities. This means that when we project we get huge diagrams mostly filled with braidings.
However, users will always be working with n-categories for some finite n. At the highest level, therefore, interchangers will indeed be identities. Would it be possible to easily introduce a feature that allowed one to pick a highest level so that Globular 'stopped caring' about interchangers at that level, and therefore showed more reasonably-sized projections?