turion
commented
8 years ago I'm still dabbling with Globular's version system of published workspaces. I actually mean version 2 of that workspace: http://globular.science/1607.001v2
Open turion opened 8 years ago
turion
commented
8 years ago I'm still dabbling with Globular's version system of published workspaces. I actually mean version 2 of that workspace: http://globular.science/1607.001v2
I mentioned before that I'm trying to formalise the 4-3-2-bordism presentation in Globular, see http://globular.science/1607.001 for the first published thing (incomplete). So far I couldn't do it because of numerous bugs. I'm going to post all of them now, don't dispair ;) The "cleanest" way would have been to take a 5-category with trivial 0- to 2-cells, and a single generating 3-cell for S^2. That would be a symmetric monoidal bicategory. But since you told me in Leeds this wouldn't work, I'm going with a 4-category with trivial 0- and 1-cells, and S^2 as the single generating 2-cell. I tried to add the symmetry of the braiding as an axiom by hand.
Here is the first bug:
Globular has these nice yellow areas to display where cells fit into the big picture. Sometimes they are displayed in completely wrong places. For example, try to recreate the 5-cell "Braid hexagon", projection 1, slice 1-1. Let's create the target for that 5-cell. We take a pair of pants, attach another one at the left leg and take the identity of that. Now we need to attach the 4-cell beta. The yellow areas of the two possible places to attach coincide! But only the first one is the correct one, the second one will attach beta in a completely different place.
I have tons of similar bugs for yellow areas, and I can post them if you want. I'll first post other bugs and feature requests.
In case this only happens because I'm using too high-dimensional cells: There should definitely be a warning as soon as one uses a cell that Globular can't deal with properly.