search

jamievicary / globular

Globular
37 stars 9 forks source link

Custom definitions/macros #58

Open turion opened 8 years ago

turion commented 8 years ago

Very often, I'll start with the same composite cells. For example in http://globular.science/1607.001, I don't know how many times I've put a pair of copants on top of a pair of pants. It would be great if it were possible to define cells that aren't generators, but that are just composites of existing cells. They should be on the left hand side with the generating cells, I guess, but maybe displayed in a slightly different way in order to distinguish them.

I guess "Theorem" does something similar, but not exactly the same, for example the graphical representation of the theorem looks different than the composite cell. Maybe it's possible to have a second button "Definition" that works a lot like "Theorem", but keeps the graphics of the composed cell, and just inserts the composed cell when clicked upon.

jamievicary commented 7 years ago

This is something we've often thought about. The 'official solution' is to use the 'Theorem' button. This creates two new cells. The higher-dimensional one of these has your diagram as its target. So to get your diagram back again, click this higher-dimensional one, decrement Project by 1, go to Slice=1, and click Restrict.

I appreciate it's more steps than you were envisioning. But the point is that 'giving a diagram a special name' is really a homotopical notion, so it can be done natively, without any additional features (=complications) to the user interface.

On Thu, Jul 14, 2016 at 5:58 AM, turion notifications@github.com wrote:

Very often, I'll start with the same composite cells. For example in http://globular.science/1607.001, I don't know how many times I've put a pair of copants on top of a pair of pants. It would be great if it were possible to define cells that aren't generators, but that are just composites of existing cells. They should be on the left hand side with the generating cells, I guess, but maybe displayed in a slightly different way in order to distinguish them.

I guess "Theorem" does something similar, but not exactly the same, for example the graphical representation of the theorem looks different than the composite cell. Maybe it's possible to have a second button "Definition" that works a lot like "Theorem", but keeps the graphics of the composed cell, and just inserts the composed cell when clicked upon.

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

turion commented 7 years ago

I see. I'm thinking of 'giving a diagram a special name' more as a definitional equality, I guess. Essentially as a shortcut that redoes all the steps I did when I created the cell. If you disagree and it must really be propositional equality, it would be really handy to have a shortcut that allows you to insert the source or target of a cell (then you could create the theorem cell and then insert its source).

jamievicary commented 7 years ago

Sure, I see what you're suggesting, and it's something I've also had the urge for many times. The issues are just that I'm extremely wary of implementing something that makes the user interface more complicated (and thus confusing to beginners), to achieve something that's already possible (albeit in 4 clicks rather than 1.) It's also extremely easy to underestimate the programming effort required for user-interface features such as this.

That said, of course this issue should not be closed, and people should continue to discuss here.

On Mon, Jul 18, 2016 at 1:10 PM, turion notifications@github.com wrote:

I see. I'm thinking of 'giving a diagram a special name' more as a definitional equality, I guess. Essentially as a shortcut that redoes all the steps

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/jamievicary/globular/issues/58#issuecomment-233376530, or mute the thread https://github.com/notifications/unsubscribe-auth/AKHHHl-0ffVA1KJsUloQoFmwXow1GZ7Qks5qW6V3gaJpZM4JMODh .

cdgls commented 7 years ago

@turion See the issue "Support Definitions and Theorems" https://github.com/jamievicary/globular/issues/39 for an extensive discussion of this and related issues.

Note that I have argued strongly many times since the beginning that globular should allow composite cells to appear in the signature, ie to have non-generators in the signature as you suggest, and eventually after the n-th argument, Jamie and I came to see eye-to-eye, wherein globular would not allow non-generators in the signature (part of what Jamie wanted) but would allow typing of cells, in particular allow definition types (part of what I wanted). See the end of the above thread for details.