Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Jamie Vicary is kindly adding information to the Lab on the higher-category-theory-proof-assistant that he and collaborators are developing, at:
I have added a few more hyperlinks to related nLab entries.
And I have changed the page name from lower case “globular” to upper case “Globular” to fit our conventions on entry titles.
Currently, lower case “globular” still redirects to the entry. But if anyone has links to the lower case version from elsewhere, please consider changing them, for eventually the lower case “globular” really ought to go to a page that disambiguates all sorts of globular-related entries on the nLab, such as globe and globular set, etc.
Cheers!
I tried playing with Globular a little.
The click/drag actions and popup labels don’t seem to work in my Firefox (v42.0) or FF Developer edition (v 44.0a2 (2015-12-05) on the aurora update channel) but they do work in Chrome. (in FF I noticed some brief popups happening with the mouse over the Project or Slice menus)
Does the Globular documentation need a note to that effect or will this be fixed “real soon now”?
(and why you may ask is FF my default browser? For one, it is the only one with native MathML)
Hi Rod, thanks for your feedback. Yes, Globular is now live, and John has kindly made the obligatory n-Category Cafe blog post for me. Please everybody try it out, and let us know what you think :).
We recommend you use Chrome, because that’s what we’ve used for all the testing so far. Now we’ve launched, an absolute priority for us is to iron out cross-browser issues, of which I fear there will be hundreds. We are inches away from being up as a public project on GitHub, and then all these things can be posted on the issue tracker.
We’re especially interested in virgin experiences - we want it to be intuitive, the first time you ever see it.
I added this to the top of the Globular documentation (moving the Chrome only warning):
(The initial release of Globular works best in the Chrome browser - several mouse actions are broken in Firefox. For now, bugs and usability issues should be reported in the nForum thread Globular).
As for usability, I couldn’t find out any way to delete or undo a change I made. If Globular maintains an undo history then that could be replayed to give a visual representation of the steps in constructing a proof.
Hi Rod. Ok, thanks!
To undo, click the ’back’ button in your browser.
To replay the individual 2d steps of a proof, build the whole thing as a single 3d diagram, and slice through it. I explain via to do this in the n-Category Cafe post.
I found it very confusing that there was no visual indication that I had clicked “source” or “target”. I am supposed to remember “OK, I have indicated the source already, now I have to indicate the target.” There should perhaps be some sort of UI indicator saying “You have selected a source, now select a target…” (This would be more appropriate as a github issue but seeing as there is no repo at the moment…)
To undo, click the ’back’ button in your browser.
I clicked on the 2-cell to add it to Strengthening an equivalence for no good reason and going back doesn’t remove the pink line on the right. Some other uses of the back button may undo things.
barron: Thanks for your feedback. A few people have told me the same thing. So, clearly this is a feature that needs padding.
Rod: thanks for the big report, we’ll get right on it.
@barron, @RodMcGuire: this feature has been added, and this bug has been fixed. (Sorry for the bizarre spelling in the previous post, the perils of typing on the phone.)
@jamie This is so great!!!
I also like the emphasis on making it natural and intuitive. I really like the idea about how you can click and drag and manipulate the diagrams organically.
I also think there is a real need for this. As you know coherence theorems and similar results play a crucial role in several of my/our projects. I recently had a senior mathematician ask me how much of these result had been verified with a proof checker like Coq. He said that mistakes had been made in the past and that he would be doubtful until it was verified by a computer. It would be really excellent if this can be used to give a verification of my coherence results and the Gurski and Osorno results that I use. After using your program I think that is a totally reasonable, but perhaps ambitious multi-stage goal. It would be great to demonstrate that this can be used to verify more than just simple easy lemmas, but can actually be used to prove difficult and important theorems too. I have an interest in seeing that happen, so I would be willing to discuss this further.
Since you were especially keen to hear about virgin experiences I just opened the program and started playing around. At first I couldn’t figure out how to use it, so then I went back to the n-lab page and read more and now I have it figured out. The thing that confused me at first was that I didn’t know how to make new morphisms just from the interface. I saw the link for adding new objects, but I wanted to add a morphisms and couldn’t tell how to do that? No button to click….
Of course the way you do that is by first building the source that you want the morphism to have, saving it, then the target. This is certainly the more efficient method in practice. It would be so wasteful to have to have to click an extra button to make each morphism. So I am not suggesting to change that functionality, but when I first opened the page I was confused. Maybe there should be some built-in tutorial aspect? Like a line of text that says “new 1-cell”, but when you click on it it just opens a small text box telling you what to do?
After I got the feel for it, I tried to implement a simple proof that came up in my book. In this proof I want to show that the “Frobenius relation” for the unbiased semistrict symmetric monoidal bicategory diagram calculus follows from some other simple relations. This is a relatively easy proof which is in Figure 2.48 on page 153 in my book: arXiv:1112.1000. I had no problem clicking on the diagram to apply invertible relations/morphisms so long as the relations happened on the inside of the diagram. But for the proof I wanted to give I need to apply one of the relations to one of the “legs” of the diagram, and I couldn’t figure out how to do that. It would only let me add more morphisms on top.
Next I tried making a really big diagram and manipulating it. Not too bad. I hope I never have to manipulate a diagram that is so big it make the functionality break. When I had a very truly enormous diagram I had trouble clicking and dragging. I think the nodes got too small or something. I am not sure. That could probably be fixed by some kind of zoom and scroll abilities, but is probably low priority.
In the medium sized diagram stage I ran into another problem. When I tried to modify the diagram by the click-drag method, I could get a morphism to move by, say, a single application of the interchanger. But then I have to re-click-drag to move past the next morphism, and re-click-drag again to get past the next one. It would be much better if I could just click and hold and drag the morphism past several other morphisms without having to re-click it each time. It should be like I am just dragging the diagram around naturally, where now I have to keep clicking it annoyingly.
There was one last problem that I had. When I made an invertible morphism/relation and I wanted to apply it in the diagram, sometimes I really wanted to apply the inverse. I couldn’t get that to work so well. It would be better if when I click to apply an invertible morphism that it could show places to attach both that morphism and its inverse at the same time. Of course that becomes tricky if the source and target of the morphism are the same. Maybe the attaching area of the morphism could be in yellow (like it currently is) and the attaching of the inverse in another color, like red?
Hi Chris, thanks for your feedback, I’m glad you like it.
It would be great to demonstrate that this can be used to verify more than just simple easy lemmas, but can actually be used to prove difficult and important theorems too.
That’s just what we want to see happen. I’d be happy to discuss your ideas here.
Since you were especially keen to hear about virgin experiences I just opened the program and started playing around. At first I couldn’t figure out how to use it, so then I went back to the n-lab page and read more and now I have it figured out. The thing that confused me at first was that I didn’t know how to make new morphisms just from the interface. I saw the link for adding new objects, but I wanted to add a morphisms and couldn’t tell how to do that? No button to click…
Thanks for that feedback. I’m not sure how to add information like that in a way that wouldn’t get irritating for experienced users. Hmm…
Next I tried making a really big diagram and manipulating it. Not too bad. I hope I never have to manipulate a diagram that is so big it make the functionality break. When I had a very truly enormous diagram I had trouble clicking and dragging. I think the nodes got too small or something. I am not sure. That could probably be fixed by some kind of zoom and scroll abilities, but is probably low priority.
Zoom and scroll would be great, and indeed essential for really big diagrams, I agree. I have a 40” 4K monitor at home which helps :).
In the medium sized diagram stage I ran into another problem. When I tried to modify the diagram by the click-drag method, I could get a morphism to move by, say, a single application of the interchanger. But then I have to re-click-drag to move past the next morphism, and re-click-drag again to get past the next one. It would be much better if I could just click and hold and drag the morphism past several other morphisms without having to re-click it each time. It should be like I am just dragging the diagram around naturally, where now I have to keep clicking it annoyingly.
This is a really good idea! Maybe not too tricky to implement, either.
There was one last problem that I had. When I made an invertible morphism/relation and I wanted to apply it in the diagram, sometimes I really wanted to apply the inverse. I couldn’t get that to work so well. It would be better if when I click to apply an invertible morphism that it could show places to attach both that morphism and its inverse at the same time. Of course that becomes tricky if the source and target of the morphism are the same. Maybe the attaching area of the morphism could be in yellow (like it currently is) and the attaching of the inverse in another color, like red?
To attach the additional structure arising from an invertible cell, you have to click on the diagram directly at the attachment point (or at the position of the bottom left of its bounding box.) This lets you restrict the choices to those that arise from a particular area of the diagram. The problem with allowing you to click a signature cell to apply its invertible structure is that there can be so many possibilities; the list of options would often become huge. I agree the user-interface needs improving, but I think it needs to involve using the mouse on the main diagram to restrict the possibilities.
Tutorial video now available: https://youtu.be/QXZJvXgs0xk
There is at least still one minor bug with the back (undo) action.
I started with Strengthening an equivalence
Then from the gallery I selected Fig 2.48 (arXiv:1112/1000v2
When I go back the Fig 2.48 ... title still persists though I didn’t notice anything else persisting.
Also is there anyway to make projections remember what slice was last viewed? When I add something and then undo I have to hunt to verify that the addition was undone.
Finally, couldn’t local storage be used to save stuff in addition to the logging in to Globular and saving it there method? I would be embarrassed if things I’ve created so far were available to others. Sure, Globular storage should be used for sharing but I’m not ready. I noticed the working Export button but there is no corresponding Import - and there probably shouldn’t be unless they work on some simplified external JSON representation. I copied and pasted an Export into JSON Editor Online to view it and I wouldn’t try to understand or generate something that big and complicated. Anyway an Import feature would need a well-formedness checker and this usage is probably very low priority now, though local storage saves might be a fairly small change and useful.
Hi Rod, thanks, I’ll investigate that bug.
When you log in and save your workspace, it remains private only to you, and those individuals you directly share it with. Workspaces only become public if you explicitly command it with the ’publish’ button. This is better than local storage, since you can work on your workspaces from any computer.
A new example proof (http://globular.science/1512.012): the Perko knots are isotopic. The Perko knots are a pair of 10-crossing knots stated by Little in 1899 to be distinct, but proven by Perko in 1974 to be isotopic. In this example, the isotopy proof is formalized in 251 steps. Thanks to Andre Henriques for suggesting this proof.
Hi Floris, thanks for your comments. Thanks for for bug report about not being able to create a 0-cell, that’s now fixed. The issue with the popups near vertices is noted in the documentation; the issue is that Globular thinks (for the purpose of calculating what you’re hovering over) that edges are all completely straight. To fix this, Globular should really use SVG mouse hover functionality, which needs a spare half a day to implement.
Regarding building theorems and applying invertible cells: do you have any ideas for how this could be made more intuitive?
Globular should really use SVG mouse hover
I had tried out seeing whether it would be simple to make some of the really tall Globular examples easier to view and mouse by turning them sideways, by pasting this code in the debugger console:
var dcsvg = document.getElementById(“diagram-canvas”).getElementsByTagName(“svg”)[0];
var dg = dcsvg.getElementsByTagName(“g”)[0];
dg.setAttribute(“transform”, “scale (2, -2) rotate(90)”);
I then noticed that hover still thought the elements hadn’t been moved and would pop up on blank areas.
@Rod McGuire - thanks, that was a good experiment!
@fpvandoorn - I’m not sure about that, since it turns one button into two buttons, one of which performs an action that can already be performed with two clicks elsewhere.
Globular is now open-source. The code is here: https://github.com/jamievicary/globular If you want to report a bug, please use the issue tracker here: https://github.com/jamievicary/globular/issues
I tried copying the outerHTML of the main SVG display and pasting it into a separate file in order to see how it looks and whether it could be used as an image/figure to be included elsewhere.
Globular’s SVG has a minor bug - it is missing the "xmlns" attribute and when it is added this works.
Given below is a patch I wrote (mostly from code I already had) - it can just be pasted into the debugger console or made into a Greasemonkey like user script. The patch adds a button open SVG to the menu. Clicking it will convert the SVG to a dataURI and open it in a new tab. Note that I added an extra ;name... parameter to the dataURI to help identify it, though that parameter is fixed for now. (I also had a Greasemonkey hack script that ran on dataURIs that would parse out that parameter and change the document.title to it so that a save would use that name but either Firefox has been updated to prevent me from doing so or I have to get it working again. I don’t know if such a hack is possible in Chrome.)
While this works, it doesn’t make good figures for inclusion because among things the SVG positions the figure in the canvas with extra white space on the sides. One possible approach to making better figures would be to employ SVG inside of SVG - see this Stack Overflow discussion for some examples. In this scheme the inner SVG would be the figure while the outer SVG would just scale and position it on the canvas.
I also noticed that Chrome (but not Firefox) has a “print to PDF” command, and that works on an extracted .svg file. However it produces pdfs only for normal paper sizes. It may be possible to hack that to produce smaller scale pdf or eps files to be included in LaTex documents. Then again I’ve heard of LaTeX packages that can directly include SVGs. I must confess I know very little about all the LaTeX packages and how to include figures.
//globular open SVG patch.js
function setSvgHref(e){
var svg = document.getElementById("diagram-canvas").getElementsByTagName("svg")[0];
if (!svg) return;
svg.setAttribute("xmlns","http://www.w3.org/2000/svg"); // add missing attribute
openSVG.href = SVGtoURI(svg, "Frobenius implies associative_p1_s1.svg");
}
osDiv = document.createElement("div");
osDiv.innerHTML = '<a target="_blank">open SVG</a>';
mainM = document.getElementById("main-menu");
mainM.insertBefore(osDiv, mainM.firstChild);
openSVG = osDiv.firstChild;
openSVG.onmousedown = setSvgHref;
function SVGtoURI(svg, name){
return "data:image/svg+xml;name" + encodeURIComponent(name)
+ ";base64," + window.btoa(escapeHTML(svg.outerHTML));
}
// from: https://github.com/fred-wang/TeXZilla/blob/master/TeXZilla.jison
function escapeHTML(aString){
var rv = "", code1, code2;
for (var i = 0; i '< aString.length; i++) {
code1 = aString.charCodeAt(i); // this line started with "var"
if (code1 < 0x80) {
rv += aString.charAt(i);
continue;
}
if (0xD800 '<= code1 && code1 '<= 0xDBFF) {
i++;
code2 = aString.charCodeAt(i);
rv += "&#x" +
((code1-0xD800)*0x400 + code2-0xDC00 + 0x10000).toString(16) + ";";
continue;
}
rv += "&#x" + code1.toString(16) + ";";
}
return rv;
};
I wrote:
In this scheme the inner SVG would be the figure while the outer SVG would just scale and position it on the canvas.
An easier to implement hack for producing figures might be to use the current SVG as an inner SVG and wrap it with an outer <svg> and a <g> for scaling so that the outer viewbox extracts just the figure. In the current <svg> the first <path> after the <g> seems to contain enough info for me to do this, but this sort of hack in an external patch would be a real pain.
Hi Rod: thanks for these ideas! based on your idea, I implemented PNG downloads, activated by the ’Graphic’ button on the right-hand side, or the letter ’g’. It’s now live.
The strategy is to create a new canvas off-screen with exactly the right size, copy the SVG image data to there, then trigger the PNG export.
Another update: 4-category functionality is now live. Some juicy proofs to follow soon hopefully.
I have not had the chance to even look at this yet, but just for clarification: when you say “4-category functionality”, do you mean that what the program does is construct 4-morphisms, and that therefore if we want to use it to prove equalities, the highest level we can do that at is equalities between 3-morphisms?
Also, what sort of 4-categories are you using?
The latest update tells Globular about how 5-cells work, which lets you prove equalities between 4-morphisms. So that’s why we advertise it as ”4-category functionality”.
We’re using our own definition of semistrict 4-category, which we developed by spending a year or two drawing lots of singularity diagrams. Semistrict n-categories have some generic axioms, like composition being strictly associative. Then for each value of n, there are additional singularity types, some of which correspond to the ’non-generic’ ways that n-cells can now be composed:
The general rule is, if you compose an -cell and an -cell along a common boundary -cell, the result is an -cell. When , this is a generic-position composite, and we can interpret the result in the traditional sense of composite cells in higher category theory. Otherwise, the result is some higher singularity type, whose job it is to resolve the non-genericity.
For example, interchangers resolve the non-genericity of the horizontal composite of two 2-cells in a bicategory. The traditional horizontal composite of two 2-cells is not available in Globular; you have to break the symmetry and use whiskering instead.
For each singularity type, we have to write custom code to tell Globular what the source and target looks like. So, 4-categories are a significant step up in complexity. But we’d learnt a lot implementing 2-categories and 3-categories, so it wasn’t as painful as we’d feared. Looking to the future, 5-categories would be intractable using these methods (although it would be easy enough to just write down the singularity types), so new ideas will be needed.
Of course, we need to document these singularities properly on the nLab, and, er, write a paper!
Very interesting! Reminds me a lot of this talk by Makkai.
Do you have any justification for your notion of semistrict 4-category, e.g. in the form of a coherence theorem?
Wow, that’s super relevant. I will study it and email him.
We don’t have any sort of coherence theorem. We haven’t even written down the definition properly yet, and writing it down elegantly seems quite hard, even though we believe the definition itself is natural enough.
Here’s some slides of mine (and Aleks Kissinger) with pictures of the singularities.
Thanks! So just to be clear, when we prove something about 4-categories in Globular, we don’t technically know yet that it yields a theorem about any naturally occurring 4-categories, right? Unless any naturally occurring 4-categories happen to be semistrict, which seems unlikely (at least, it rarely happens for 3-categories). I don’t mean to be critical — Globular sounds really amazing and I’m still looking forward to finding the time to try it out — I just want to be sure I understand the state of knowledge.
In a strict sense, that’s right.
However, in a more relaxed sense, which is more typical of how mathematicians really work, it’s hard to see this as much of a problem. (I don’t claim you’re saying it is a big problem, just explaining our perspective.) Firstly, to what are you comparing a Globular proof - a handwritten proof? Clearly, neither are strictly formal, and the Globular proof has the advantage of being fully explicit. No proof (because proving it by hand is too complicated)? Then Globular wins by default. A HoTT proof in Coq? OK, then maybe HoTT wins, but as we’ve discussed before, there are not that many proofs well-suited to formalization in both Globular and Coq. (Consider the Perko knot isotopy proof, compared to a proof in Coq that uses any sort of non-algebraic structure like a universal property.)
Also, note that handcrafted proofs are often carried out in an informal semistrict style anyway! For example, see a lot of the work of Scott Carter and collaborators on knotted surfaces calculations, which are taking place in a braided monoidal bicategory; they don’t stop to worry too much about the definition of semistrict 4-category, they just let geometry guide them. The same is true for a lot of the Morse-theoretic calculations of people like Chris Douglas, Andre Henriques and Chris Schommer-Pries; for example, Andre Henriques has an explicit sphere eversion proof which takes place formally in a semistrict 6-category.
Also, I would expect that if an expert in some “trusted” definition of 4-category looks at the singularity structure that Globular is using, they would say, “yeah, those rules are in my definition of 4-category, implicitly or explicitly”. And I think often this would be such an easy process, a Globular proof would give them a very good sense of how to construct a proof using their definition. (Of course, it would be nice to talk to some experts (like you Mike!) and see if they agree.) Perhaps more likely would be that they have some proof already in their definition of 4-category, and not see how to write it as a Globular proof. So they might say “hey, your definition of semistrict 4-category is not general enough.” And maybe they would be right (although I don’t think so), time will tell.
Note that even if we had proved that every weak 4-category is equivalent to a semistrict 4-category by our definition, that would only take you half way to fully trusting the Globular formalization: you would also need to prove that the source code of Globular implements the definition correctly. This is far from straightforward; as you know, writing a proof assistant is far more complicated than just “typing in the definition of the logical system”. And Globular is written in Javascript, which does not lend itself to formal verification, to say the least.
(By the way, using Javascript made Globular quite easy (in a relative sense) to write and debug; I don’t think Globular would exist today if we’d tried to write it in a more traditional programming language for computational logic. And if we’d succeeded, you’d have to download some crummy installer to use it, rather than just click on a link in your browser; and it would only exist on some platforms; and nobody would use it. So for many good reasons, being very formal is quite low down our list of priorities at the moment.)
Also, note that handcrafted proofs are often carried out in an informal semistrict style anyway! For example, see a lot of the work of Scott Carter and collaborators on knotted surfaces calculations, which are taking place in a braided monoidal bicategory; they don’t stop to worry too much about the definition of semistrict 4-category, they just let geometry guide them. The same is true for a lot of the Morse-theoretic calculations of people like Chris Douglas, Andre Henriques and Chris Schommer-Pries; for example, Andre Henriques has an explicit sphere eversion proof which takes place formally in a semistrict 6-category.
This is the type of thing I was dreaming around 20 years ago when I began thinking about general notions of -category. The feeling I had then and today is that it should be possible to express virtually all the key lemmas in Morse theory (e.g., lemmas on rearrangement and cancellation of critical points) as formal calculations in a suitable semi-strict -category with duals. So reading about the work of Douglas, Henriques, and Schommer-Pries here is exciting to me.
Spiritually, this work seems very much on the right path to me.
The feeling I had then and today is that it should be possible to express virtually all the key lemmas in Morse theory (e.g., lemmas on rearrangement and cancellation of critical points) as formal calculations in a suitable semi-strict n n-category with duals.
And that gives a way to understand what semistrict -categories are, and what Globular is aiming to be — singularity theory, but not necessarily with duals! So it’s the same techniques that the manifold theorists use, but applying them to more general mathematical objects.
I confess I haven’t looked seriously at Globular yet (mainly because of my general incompetence in dealing with computer programs).
When you say “not necessarily with duals”, does this mean you don’t handle duals via critical points directly, and instead eliminate critical points of Morse functions by progressifying the string diagram (“progressifying” referring to progressive string diagrams)? My first immediate thought runs to the yanking move which expresses a triangular equation for an adjunction, the most elementary example of a cancellation of critical points. Progressifying means refining the stratification by adding those critical points as extra points to the 0-dimensional part of the stratification.
I think you’ve got it right, although I don’t quite understand everything you’re asking. Globular doesn’t know about the yanking move automatically, since it isn’t implied by the definitions of a semistrict n-category. So you have to add it to your signature, then you can use it wherever you want.
I don’t understand this sentence, because the two propositions either side of the comma seem consistent to me:
does this mean you don’t handle duals via critical points directly, and instead eliminate critical points of Morse functions by progressifying the string diagram (“progressifying” referring to progressive string diagrams)?
We do handle duals via critical points directly; and indeed, the way those critical points are manipulated are by the user specifying certain rules (like “the snake equation holds”), and then applying them at will to eliminate or introduce critical points.
So you have to add it to your signature
I think that sort of answers my question.
the way those critical points are manipulated are by the user specifying certain rules (like “the snake equation holds”)
Okay, thanks.
I don’t know how to go about it for something like Globular, but here’s roughly the thing I’d like to see one day. You can think of a unit of an adjunction as an extrapolation of an equality predicate (and indeed an equality predicate, as a 1-cell in the monoidal 2-category of the form , is just such a unit for the self-duality of ). Similarly, can be rendered as a unit in the monoidal 2-category of profunctors for the adjunction , and this too I think of as a generalized equality predicate.
Now I’d like to see a program in which such “equality” is something that doesn’t need to be user-specified, but something already embedded in the program. So that some predicates come for free and are not embodied in a signature or generating computad or whatnot; the corresponding critical points would not be marked as 0-cells in the stratification. If you see vaguely what I mean.
I think you’re asking: could the equations for a duality be “baked in” to Globular?
The answer is yes. The problem is not everyone would want this (since not all 1-morphisms in a bicategory have an adjoint), so you’d have to be able to turn it on and off. And why stop there — why not be able to specify that any generating cell in your signature is fully dualizable, in the sense of the cobordism hypothesis? Or orientedly fully dualizable? Or ambidextrously fully dualizable? Or an -equivalence? And so on.
So, that’s lots of potential features that someone could program in, if they can work out an appropriate corecursive description of all the necessary structure (which may not be known, such as for oriented full dualizability), and if they have enough time on their hands.
The only cell property we’ve implemented so far is invertibility. In a sense, this is the most powerful sort of dualizability you can ever ask for, and it’s clear how to corecursively generate all the necessary associated higher structure. You can choose this by selecting the little “Invertible” checkbox next to a generator.
However, the corresponding critical points that this gives rise to are still marked in the singularity graphic, as you have to be able to interact with them (apply interchangers to them, etc) just as for any other critical point.
@jamie #35: I agree entirely (that’s why I used the word “technically”). However, I do worry a bit that the work by people who “let geometry guide them” is too sloppy, precisely because it implicitly semistrictifies.
Interesting perspective. So do you doubt that ’geometric’ semistrictification (ie with all the weakness in interchangers and associated structures) is possible in general?
I would take a strongly opposite perspective: the only conceivable way to formalize these proofs (eg of sphere eversion in a 6-category) is by semistrictifying.
Well, I cling to the old-fashioned view that we only know something is possible once we’ve proven it. So since we don’t know it’s possible, I suppose by definition there is room for some doubt. I wouldn’t bet against it, if that’s what you mean; but I wouldn’t claim to know anything that depends on it until it’s been proven.
As for your second paragraph, I suppose that depends on what you mean by “formalize” and “conceivable”. In principle it certainly ought to be possible to make such an argument in a weak 6-category, but I guess maybe you’re saying that a weak 6-category is too complicated to ever imagine a human being actually doing anything with directly?
I also wouldn’t bet against it. People who do these high-dimensional semistrict calculations might be working in a relatively ill-defined axiomatic framework — although many of them would challenge that strongly I expect! — but I think ’sloppy’ is an unfair word, because it implies there’s an alternative approach. (Is there?) Personally I find it quite refreshing, letting the formal framework develop alongside the proof, rather than before it (but maybe that’s my physics degree talking.)
By ’conceivable’, I mean ’I could imagine a human guiding every stage of the proof’. Of course, maybe it would be possible with a proof assistant that fills in all the technical details, with the human only providing the key steps; but that’s very close to semistrictness again.
At the risk of repeating myself, I’ll say that Eric Finster’s opetopic type theory does seem to make conceivable the idea of fully formal proofs in fully weak -categories for unbounded .
It might might be worthwhile to try to combine OpTT, as the fundametal internal language of an -category, with interfaces that offer more high level constructs such as the singularity data used in Globular.
I know Eric is working on interfacing OpTT with HoTT. A while back here in Bonn he presented his beautiful picture of how all the type forming rules in HoTT are naturally implemented as cells in OpTT, and how “running” HoTT on OpTT this way would or should realize the old dream of making all rewriting “proof relevant” (or whatever it’s called, I might not use the right terminology).
Given that, above and elsewhere, you vaguely wonder about connecting Globular to HoTT, it would seem to me that OpTT might be the natural fundament for something like this to work.
By the way, personally I am fascinated by how Eric explained to me that the single “term introduction rule” of OpTT is really to do with the universal property of higher adjunctions. I might have to go back to my notes to say this more properly, and I don’t have the time for this now, but I had gotten the glimpse that OpTT might even naturally put adjoint type theory into the picture.
Of course, also for OpTT there is presently no proof (or any discussion, for that matter) that its model of -categories is compatible with established models of -categories (hence in particular with models of -categories that Globular is dealing with), but since by design in OpTT absolutely nothing is ever “strict” (not even judgemental equality) it is rather plausible that it is.
Yes, that’s a very important approach, and clearly there is a lot that could be formalized there in principle that wouldn’t be possible by other means, since it is the only formalization of -categories that we have available. But in practice, the lack of a geometric string diagram calculus for opetopic categories makes it hard to see how heavily geometrical proofs (like the Perko knot isotopy proof linked to above, or the other example proofs on the Globular webpage) would actually be formalized by a human (and then understood by other humans.) And the weakness of course make the formalized proofs longer.
Jamie, my point isn’t that the axiomatic framework of semistrict higher categories is ill-defined (although your comments about not having written down your definition of semistrict 4-category yet suggest that it is, and at the very least I’ve never heard of any “accepted” general definition, although some people like Makkai have attempted one), but rather that it’s sloppy to work in a semistrict context but claim that the results also apply to the weak context. Perhaps they aren’t doing that either, but since in my experience very few categories arising in practice are naturally semistrict, it seems that a theorem only about semistrict ones would not be very useful.
Of course, proofs computed today by Globular in a 4-category should not be advertised without qualification as applying to weak 4-categories, until such a time as somebody proves the appropriate coherence theorem.
Such a proof may still be useful, even if the ultimate application is intended to be in a weak n-category, if no other tractable formal approach is available, and I contend this is the case today for 4-category proofs with a strongly geometrical flavour.
the lack of a geometric string diagram calculus for opetopic categories
The beauty of Eric Finster’s “opetopic diagrams” is that they are precisely that: string diagram calculus generalized to arbitrary dimension.
The beauty of Eric Finster’s “opetopic diagrams” is that they are precisely that: string diagram calculus generalized to arbitrary dimension.
My phrasing was poor: opetopic n-categories of course have a geometric diagrammatic calculus, which is the basis for his opetopic tool. However, I personally find this difficult to use for constructing proofs, because it differs from the diagrammatic calculus for globular n-categories that I am familiar with, in which composites are denoted literally as connected structures hanging in n-dimensional Euclidean space, and which can then be visualized by taking projections or subspaces.
If someone with a better intuitive understanding than me could translate some proofs (like the proof that an equivalence in a bicategory can be promoted to an adjoint equivalence) into the opetopic tool, that might help me develop my intuition. I suggested this to Eric last time we spoke, maybe he has done it, I’m not sure.
I am just highlighting that there is a difference between “it is not conceivable” and “I personally find it difficult”. -Category theory for arbitrary is bound to be difficult. All the more is it worthwhile to look for formalisms that help systematize it. In #30 you wrote regarding the diagrammatic calculus for globular -categories that you are familiar with:
Looking to the future, 5-categories would be intractable using these methods, so new ideas will be needed.
I am thinking OpTT looks like such a new idea, that makes some things conceivable which in some comments above were suggested to be inconceivable.
Of course passing from conceivable to conceiving will take work. Above I suggested that it might be useful to use the globular diagrams as high-level interfaces for opetopic cells. I.e. have a program read in globular structures and turn them into opetopic cells. That must be possible. Maybe it would allow to combine the intuitive appeal of Globular with the more foundational strength of OpTT.
Urs, I think that’s a great idea. All these approaches have quite different strengths, so seeking to combine them makes a lot of sense.
However, I realize I am confused about the formal relationships between opetopic and globular -categories. If a result is proven in an opetopic -category, I believe (recalling historical discussions with Eric) that it is not clear if it can then be made relevant to a globular -category. It would be good to hear what would be possible in principle here. Maybe it is easier to go from globular to opetopic.
I don’t think I’ve heard anyone verbally disbelieve that opetopic ω-categories and globular ones (at least, the sort of globular ones that don’t come with “extra invertibility data”) ought to end up being equivalent. However, I don’t think I’ve seen a proof written down even for 3-categories.
I agree that even without a coherence theorem, semistrict proofs may be useful in the sense of making a result believable, suggesting how one might prove it in the weak case, motivating us to actually prove the coherence theorem, and so on.
Mike, then we agree perfectly.
I had strongly got the impression from Eric that the notions (opetopic vs globular) would be incommensurable. Maybe I misunderstood. I will email him.
I was going to suggest we put some links in for singularity, resolution of singularities, etc. but they’re not in the greatest shape.
I have no idea if the concept of ’resolution of singularities’ linked to there is directly relevant for the categorical notion.
That would be good to find out. Who first used the term resolution of singularities in your sense?
What do we know about the general picture? Presumably that the singularities/catastrophes of Arnold and Thom show up in higher algebra (as the discussion goes here).
And this is very much connected to higher categories and stratified spaces, where we hear of “resolution of singularities” in the usual sense, as in Factorization homology from higher categories.
The fold, cusp, swallowtail, butterfly catastrophes are very relevant; they represent equations that should be satisfied by coherent equivalences in semistrict -categories. But many of the singularity resolutions that go into the definition of semistrict -category are more basic. For example, the interchanger is a singularity resolution in this sense, as is naturality for the interchanger, but you won’t find these on a standard list of catastrophe types.
The phrase ’resolution of singularities’ is just something we made up for the context of semistrict -categories.
Hi EMF, thanks for your bug report, and sorry for the slow reply; I only check this every couple of weeks or so, and unfortunately I don’t know who you are, so I can’t send you a direct email.
Regarding your first point: interchangers certainly should cancel with their inverses. Can you provide a workspace exhibiting the problem you are having? You can click ’Export’ on the right-hand menu to download a file encoding the current workspace.
Regarding your second point: you’re right that coherence for interchangers is missing. This would be a useful feature that we should add. The issue here is that invertible cells in Globular aren’t automatically coherently invertible. It’s not known how to generate all the coherent equivalence equations in all dimensions, but we could certainly at least implement snakes in the first dimension, I agree.
Also, regarding your point that “they are often very hard to pull”: it is often the case that even though something looks like you can pull it through, in fact you cannot, for reasons that will be clear if you unproject and look carefully at the slices through your diagram. Another idea: when you try to pull an interchanger, make sure you are clicking on the intersection point. You can tell if you’re hovering correctly over the centre of the interchanger by looking at the pop-up caption by the mouse cursor.
Note that you can subscribe to an RSS/ATOM feed for just a single nForum discussion: it’s under “Discussion Feed” on the top left of this page.
Thanks Mike, I think I’ve added the notification, although I’ve not done this before so I’m not sure I’ve set it up right.
I’ve just uploaded a nontrivial 4-category proof, worked out with my student Krzysztof Bar: an adjunction of 1-morphisms in a 4-category gives rise to a coherent adjunction satisfying the butterfly equations.
Hi EMF, thanks for your messages, and for your bug report.
Regarding the Int-LS family of morphisms: could you provide a workspace that allows me to replicate the crash you are experiencing?
Regarding the second issue: I’m afraid I don’t know what you mean by the “nondegenerate pairing page”. Can you please explain your issue here a bit more.
Also, could you tell me who you are? It’s nice to know the real-world identity of people who are using it! :)
Hi EMF, thanks for these excellent and detailed bug reports. Some of these features are undocumented and a bit ’experimental’ – how did you find out about them?
I think I understand the problems here. I hope I can fix them tomorrow. I will post here when there is an update.
Thanks EMF, fixed!
I added the reference
Very relevant to something I’m reviewing, in terms of what can be proved in ordinary knot theory, is it that only identities, such as The Perko knots are isotopic, are possible? Proving non-equivalence of two knots presumably can’t be done. And proving results about a class of knots?
Knot theorists prove the non-isotopy of two knots using invariants. They put a lot of effort into finding new invariants. You get extra points as a knot theorist if your new invariant distinguishes many non-isotopic knots, or if it’s efficient to compute. It’s decidable whether two knots are isotopic, but the complexity class is high, and in practice people can’t go further than knots with 11 crossings.
At the meeting Knots in Washington I was at last weekend, Dror Bar-Natan presented a beautiful new knot invariant which can distinguish all knots with up to 10 crossings. See here for some beautiful pictures.
A natural extension of Globular would be for it to compute invariants of the diagrams that you draw. Since these diagrams are higher-dimensional category diagrams, not merely knot diagrams, these invariants would be more general than knot invariants, but I’m sure they would be closely related.
The computer scientist in me is dying to know, how are n-categories actually represented in code?
Hi Keith, good question! I explained this in the talk at the Simons Institute I gave recently, linked to from a recent post on the Azimuth blog.
The most important breakthrough we had—it seems an over-dramatic word now, but it really felt like a breakthrough at the time—was to never put any vertices at the same height. This means that the set of vertices of a given diagram forms an ordered set; say, from bottom to top. So to define an n-diagram, we first define its source (n-1)-diagram. We then give the list of vertices in the diagram, from bottom to top, giving for each vertex n-1 natural numbers that specify the ’coordinates’ at which to attach it to the part of the n-diagram below it. It seems here that I haven’t told you how to define its source (n-1)-diagram. But in fact I have; you just use the same definition, in a recursive way. You stop by saying that a 0-diagram is just a choice of 0-cell generator.
“Never putting any vertices at the same height” is a familiar property from Morse theory, where they use diagrams with this property to study higher-dimensional manifolds. So really our diagrams are “generalized higher Morse diagrams”; “generalized” in the sense that we’re not just using them to describe manifolds, but any higher-algebraic structure.
@Jamie
Wow, that’s incredible! I don’t quite understand his table though: a number of entries are 0 that I thought were his [1] invariant.
[1] or possibly Rozansky’s
By the way, you should put in some common presets, so if a user wants to build up something quickly they don’t have to reinvent the wheel as it were.
@David, I’m not sure either…
@Keith, all projects are fully editable, so if you want a ’preset’ you can just load an existing project and start modifying it. A good start is to delete (with the red ’X’) any generators you don’t want. Don’t worry, you won’t overwrite the public version that you loaded. To save it to your machine, click the ’Export’ button.
@David, maybe those knots are actually isotopic?
I’m sure the unknot and should be distinguished by a knot invariant, no?
…
Ah, I just realised, it’s the pair (Alexander,Rozansky) that is able to distinguish all knots up to ten crossings, no just the Rozanksy invariant. That makes more sense.
Jamie, firstly thanks for the great tool. It is very impressive and intuitive once you get used to the minimal interface.
I was wondering whether there is an idiomatic way to create abstractions when doing proofs.
For example, I want to define a converse operator which for each 2-cell yields a 2-cell by attaching a cup and a cap to appropriate places. Another operator is an intersection operation which takes two 2-cells and yields .
Then I want to prove general equations which hold between the two operators but I have not found a satisfactory way to do this. For example, how the converse distributes over the intersection for all R and S.
The way I have been doing this so far is by introducing an “inert” 2-cell which acts as a meta-variable. I worry that this approach won’t scale as more complicated equations will need multiple meta-variables and I don’t want to prove basic facts about each operator multiple times for each meta-variable I require and having to explicitly introduce 3-cells for any time I have to instantiate the meta-variable.
Is there a recommended way to structure programs in this manner?
I formalised bare-bones Kirby calculus in Globular, so if you want you can define 4-manifolds and formalise diffeomorphisms between them now!
It’s here: http://globular.science/1808.001
In order to prove your own diffeomorphisms, open the workspace, start clicking together your Kirby diagram from the existing 3-cells, then press “Identity” and apply Kirby moves and isotopies until you end up with the manifold you wanted.
It’s still quite tedious. In order to prove a simple lemma like , I still need over 100 moves (as compared to, say, 6 sketches on paper). If you have any recommendations as to how to simplify things (maybe by proving a lot of little technical lemmas), I’d like to hear it.
If you find a problem with it, want help how to use this, or want to see some diffeomorphism formalised, I’m also happy to discuss!
Hi Manuel, cool! What reference for the 4d Kirby moves are you using?
Hi Jamie, I’m just using Gompf & Stipsicz, and my own musings. The idea to “fuse” handles at two points and then to isotope the fusion points around is mine, but it is not a very deep idea to people (such as me) who have spent too much time proving handle slides in fusion categories. I hope that it’s correctly encoded, since I have no way to express that two handles in the diagram are distinct (except for redoing all the generators and relations for each new handle). But given that I could formalise a nontrivial diffeomorphism, I would assume that my encoding is complete (you can formalise any explicitly given diffeomorphism). But maybe the fusion trick makes it unsound in some way I couldn’t fathom yet.
A few comments on usability:
One deadly sin that globular commits is the use of plain http without an https option, in particular when logging in. This means that your password is transmitted in cleartext. Globular not being “big” yet is no excuse, nor is any advice like “Then don’t pick a valuable password.”. Https is free and easy to set up these days (https://letsencrypt.org/).
Added to References links to two Jamie Vicary videos at YouTube. A link to the tutorial was already in the body of the text but I thought it deserved to be mentioned as a reference. Also a link to Jamie’s 2016-12-05 talk at the Simons Institute. This seems to be a new reference. But has more recent work made it obsolete? Hope format is right, used reference above as style guide.
completed publication data for this item:
Deep down in this entry was a line saying that Globular “will soon be followed by a succesor tool homotopy.io”. I don’t really know about any of this, but it looks like homotopy.io long exists and may be preferred by users, so I moved that line to the very top of the entry.
In the process I noticed that there was not a single mention of “associative n-categories” on this page, while homotopy.io claims it’s all about that notion. So I added the pointer to “associative n-categories” also to the first sentence of “Overview” here.
1 to 91 of 91