Christopher Douglas

Maybe it could be done one step at a time --- first snake equation for the invertible cells, then worry about more later as it arises.

I think perhaps minimized cells should still be candidates for matching when clicking on the diagram. Sometimes you want to minimize auxiliary cells, as you say, but sometimes you just...

I agree those are two things you might want to do, but so far, I haven't needed to disable cells, I only want to be able to hide them. This...

Yes, something like that sounds good. Actually: I suggest putting these right where the X is now, and having the X be less accessible --- for instance, what if a...

It occurs to me that if you use the current theorem function to create your definitions, then globular knows the desired link between them. [Is this how you are already...

I agree that it isn't obvious what the best approach is to all this, but to push the discussion, some further questions/thoughts ... 1. If you don't type proofs and...

Okay, so I think the main items under consideration are: 1. Some UI indication of type (Axiom, CellWithADefinition, Definition, Theorem, Proof). (What the heck should that second type be called?)...

Correct me if I'm wrong, but reading the above comments, it seems like we are already roughly in agreement that all of 1,2,3,4 are worth doing. 1. We've all said...

Following a discussion with Jamie, the proposal is the following. (1) In the lower right corner of each cell box, there will be a small box [ ] This will...

I would furthermore add another gray function box on the right called "Definition", such that "Definition" and "Theorem" do exactly the same thing except that "Definition" labels the two cells...