search

jamievicary / globular

Globular
37 stars 9 forks source link

Problem with adjunctions #55

Open turion opened 8 years ago

turion commented 8 years ago

This is still about the 4-3-2-bordism presentation. When trying to formalise that mu and nu are adjoint on the cap, there is a problem.

Take the 3-cell "Cap", take its identity and try to attach the 4-cell nu. There is only one place to put it, and that's left of it! But of course I want it on top!

Note that this works for the Cup, so it's an intricate bug I guess. (Unrelatedly, when attaching nu to the identity of the Cup, the yellow areas go in wrong places again.)

(My current workaround: I have to add nu on the left side, and then I fiddle around with interchangers)

jamievicary commented 8 years ago

Hi, thanks for the report. Can you attach a minimal workspace exhibiting the problem?

On 14 Jul 2016 5:37 a.m., "turion" notifications@github.com wrote:

This is still about the 4-3-2-bordism presentation. When trying to formalise that mu and nu are adjoint on the cap, there is a problem.

Take the 3-cell "Cap", take its identity and try to attach the 4-cell nu. There is only one place to put it, and that's left of it! But of course I want it on top!

Note that this works for the Cup, so it's an intricate bug I guess. (Unrelatedly, when attaching nu to the identity of the Cup, the yellow areas go in wrong places again.)

(My current workaround: I have to add nu on the left side, and then I fiddle around with interchangers)

— 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/55, or mute the thread https://github.com/notifications/unsubscribe/AKHHHiATCmSH_7jXu2p1lFxuOyhmVYlfks5qVfVEgaJpZM4JMM_j .

turion commented 8 years ago

I was thinking of this one: http://globular.science/1607.001v2 Although it's not minimal. Do you want a simpler version exhibiting the same problem?

jamievicary commented 8 years ago

Hi, this seems to work OK for me. I follow the following steps:

  1. Click on "Cap" to load it into the workspace.
  2. Press "Identity"
  3. Click just above the cap, where the tooltip says "* @ t [1,0,0,0]".

This attaches the nu in the appropriate way for the first part of the adjunction equation. Let me know if that works for you.

On Thu, Jul 14, 2016 at 12:39 PM, turion notifications@github.com wrote:

I was thinking of this one: http://globular.science/1607.001v2 Although it's not minimal. Do you want a simpler version exhibiting the same problem?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/jamievicary/globular/issues/55#issuecomment-232641504, or mute the thread https://github.com/notifications/unsubscribe/AKHHHkD6u3DjotfzKGJGSO72wOhzpBDNks5qViAKgaJpZM4JMM_j .

turion commented 8 years ago

Yes, that works. What doesn't work is the following:

  1. Click on Cap
  2. Press Identity
  3. Click on nu

This gives only one way of attaching nu, although there should be 3 (left, above, right).