jamievicary / globular

Globular
37 stars 9 forks source link

Strange bug in braiding #45

Closed turion closed 8 years ago

turion commented 8 years ago

Have a look at this workspace: http://globular.science/1607.001 In particular, look at the last morphism I've added, "Cell 11". It was supposed to be the symmetry of the braiding. (I'm trying to formalise the presentation of 4-3-2-bordisms.) I tried several times to add the relation, but always the source or the target would come out wrong. It misses one of the strands. You'll see that Cell 11 doesn't even typecheck, if I understand it correctly.

jamievicary commented 8 years ago

Hi, thanks for the report. It works fine for me when I load it up. But I think I have noticed this sort of behaviour before. The best thing is to treat this just as a display bug, which it is, and press ahead. I think I know how to fix it; when I get some time I will post an update.

On Thu, Jul 7, 2016 at 11:31 PM, turion notifications@github.com wrote:

Have a look at this workspace: http://globular.science/1607.001 In particular, look at the last morphism I've added, "Cell 11". It was supposed to be the symmetry of the braiding. (I'm trying to formalise the presentation of 4-3-2-bordisms.) I tried several times to add the relation, but always the source or the target would come out wrong. It misses one of the strands. You'll see that Cell 11 doesn't even typecheck, if I understand it correctly.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/jamievicary/globular/issues/45, or mute the thread https://github.com/notifications/unsubscribe/AKHHHtSBRuZZ-Veo1ZCyAi6rdY7GrHtqks5qTX42gaJpZM4JHkBh .

jamievicary commented 8 years ago

Hi Turion, this might be fixed now, can you check it you can still replicate the issue?

turion commented 8 years ago

Yes, works now! It already worked on Chromium before, and it now also works on Firefox. Thanks!

jamievicary commented 8 years ago

Great.

On Wed, Jul 13, 2016 at 10:24 AM, turion notifications@github.com wrote:

Closed #45 https://github.com/jamievicary/globular/issues/45.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/jamievicary/globular/issues/45#event-721294571, or mute the thread https://github.com/notifications/unsubscribe/AKHHHvTadf-vrlVV5L6X9aS2opR6VJ2Yks5qVK6_gaJpZM4JHkBh .