Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 27th 2015
    • (edited Nov 30th 2015)

    Jamie Vicary is kindly adding information to the nnLab 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.

    • CommentRowNumber2.
    • CommentAuthorjamievicary
    • CommentTimeNov 29th 2015

    Cheers!

    • CommentRowNumber3.
    • CommentAuthorRodMcGuire
    • CommentTimeDec 5th 2015

    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)

    • CommentRowNumber4.
    • CommentAuthorjamievicary
    • CommentTimeDec 5th 2015

    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.

    • CommentRowNumber5.
    • CommentAuthorjamievicary
    • CommentTimeDec 5th 2015

    We’re especially interested in virgin experiences - we want it to be intuitive, the first time you ever see it.

    • CommentRowNumber6.
    • CommentAuthorRodMcGuire
    • CommentTimeDec 6th 2015

    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.

    • CommentRowNumber7.
    • CommentAuthorjamievicary
    • CommentTimeDec 6th 2015

    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.

    • CommentRowNumber8.
    • CommentAuthorbarron
    • CommentTimeDec 6th 2015

    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…)

    • CommentRowNumber9.
    • CommentAuthorRodMcGuire
    • CommentTimeDec 6th 2015

    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.

    • CommentRowNumber10.
    • CommentAuthorjamievicary
    • CommentTimeDec 6th 2015

    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.

    • CommentRowNumber11.
    • CommentAuthorjamievicary
    • CommentTimeDec 7th 2015

    @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.)

  1. @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?

    • CommentRowNumber13.
    • CommentAuthorjamievicary
    • CommentTimeDec 7th 2015

    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.

    • CommentRowNumber14.
    • CommentAuthorjamievicary
    • CommentTimeDec 7th 2015
    • (edited Dec 7th 2015)

    Tutorial video now available: https://youtu.be/QXZJvXgs0xk

    • CommentRowNumber15.
    • CommentAuthorRodMcGuire
    • CommentTimeDec 7th 2015
    • (edited Dec 7th 2015)

    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.

    • CommentRowNumber16.
    • CommentAuthorjamievicary
    • CommentTimeDec 7th 2015

    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.

    • CommentRowNumber17.
    • CommentAuthorjamievicary
    • CommentTimeDec 11th 2015
    • (edited Dec 11th 2015)

    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.

    • CommentRowNumber18.
    • CommentAuthorfpvandoorn
    • CommentTimeDec 11th 2015
    This theorem prover, and the tutorial video, look awesome!

    However, I cannot add new 0-cells. If I click the button "New 0-cell", nothing happens. I do get the "finger" as cursor when hovering over it, but clicking doesn't do anything (it doesn't create a message in the console). Everything else seems to work fine. I'm working on Kubuntu 14.04, Chrome 46.0.2490.86 (64-bit).

    Since you asked about first-user experiences. I watched the tutorial video, and after that played around with some very basic theorems (using a single 0-cell, since I couldn't add more). The following things I found counter-intuitive:
    - How to start a proof. (i.e. apply identity and then modify one side)
    - How to finish a proof (i.e. press "Theorem")
    - Say I mark a 2-cell "invertible." Now I am proving a theorem (where the theorem statement is also a 2-cell), and I want to apply the inverse of this 2-cell. If I click the 2-cell, I get a couple of suggestions where to apply this 2-cell, but I don't get suggestions how to apply the inverse of this 2-cell. (In the end I figured out that if I click on a particular side of my diagram, it gave me suggestions of what to apply.)

    Lastly, I had a small bug with the popups, which display the name of a cell. Suppose I have a U-shaped 2-cell (like "red cup" in the tutorial). If I hover over the 1-cells near the edge of the diagram, I get the correct pop-up, but if I hover over the 1-cell near the 2-cell, I get the wrong pop-up (namely, I get the pop-up for the 0-cell around it).
    • CommentRowNumber19.
    • CommentAuthorfpvandoorn
    • CommentTimeDec 11th 2015
    PS: I also cannot add 0-cells on my Windows 10 laptop, using Chrome 47.0.2526.80 m.
    • CommentRowNumber20.
    • CommentAuthorjamievicary
    • CommentTimeDec 11th 2015

    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?

    • CommentRowNumber21.
    • CommentAuthorRodMcGuire
    • CommentTimeDec 11th 2015
    • (edited Dec 11th 2015)

    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.

    • CommentRowNumber22.
    • CommentAuthorfpvandoorn
    • CommentTimeDec 11th 2015
    Great! Adding 0-cells now indeed works.

    > Regarding building theorems and applying invertible cells: do you have any ideas for how this could be made more intuitive?

    One possibility is to have a new button "begin construction," which is just applying identity and moving to the target slice, and changing the name of the button "Theorem" to "end construction."
    • CommentRowNumber23.
    • CommentAuthorjamievicary
    • CommentTimeDec 12th 2015

    @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.

    • CommentRowNumber24.
    • CommentAuthorjamievicary
    • CommentTimeDec 14th 2015

    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

    • CommentRowNumber25.
    • CommentAuthorRodMcGuire
    • CommentTimeJan 3rd 2016

    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;
    };
    
    • CommentRowNumber26.
    • CommentAuthorRodMcGuire
    • CommentTimeJan 4th 2016

    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.

    • CommentRowNumber27.
    • CommentAuthorjamievicary
    • CommentTimeMar 3rd 2016

    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.

    • CommentRowNumber28.
    • CommentAuthorjamievicary
    • CommentTimeMar 8th 2016

    Another update: 4-category functionality is now live. Some juicy proofs to follow soon hopefully.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeMar 8th 2016

    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?

    • CommentRowNumber30.
    • CommentAuthorjamievicary
    • CommentTimeMar 9th 2016
    • (edited Mar 9th 2016)

    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:

    • For 2-categories, there is one 3-cell singularity that arises:
      • The interchanger, arising from the non-generic horizontal composition of 2-cells, i.e. the composite of two 2-cells along a common boundary 0-cell.
    • For 3-categories, there is one additional 4-cell singularity that arises:
      • Naturality for the interchanger in one variable, arising from the non-generic composite of a 3-cell and a 2-cell along a common boundary 0-cell.
    • For 4-categories, there are three additional 5-cell singularities:
      • “Naturality for naturality for the interchanger in one variable”, from composing a 4-cell and a 2-cell along a common boundary 0-cell.
      • “Naturality for the interchanger in two variables”, from composing two 3-cells along a common boundary 0-cell.
      • “Naturality for the invertibility of the interchanger”, which arises for a different reason.

    The general rule is, if you compose an nn-cell and an mm-cell along a common boundary pp-cell, the result is an (n+mp1)(n+m-p-1)-cell. When p=min(n,m)1p=\text{min}(n,m)-1, 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!

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeMar 9th 2016

    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?

    • CommentRowNumber32.
    • CommentAuthorjamievicary
    • CommentTimeMar 9th 2016

    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.

    • CommentRowNumber33.
    • CommentAuthorjamievicary
    • CommentTimeMar 9th 2016
    • (edited Mar 9th 2016)

    Here’s some slides of mine (and Aleks Kissinger) with pictures of the singularities.

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2016

    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.

    • CommentRowNumber35.
    • CommentAuthorjamievicary
    • CommentTimeMar 10th 2016
    • (edited Mar 10th 2016)

    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.)

    • CommentRowNumber36.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 10th 2016

    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 nn-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 nn-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.

    • CommentRowNumber37.
    • CommentAuthorjamievicary
    • CommentTimeMar 10th 2016

    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 nn-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.

    • CommentRowNumber38.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 10th 2016

    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.

    • CommentRowNumber39.
    • CommentAuthorjamievicary
    • CommentTimeMar 10th 2016
    • (edited Mar 10th 2016)

    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.

    • CommentRowNumber40.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 10th 2016
    • (edited Mar 10th 2016)

    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 η:1gf\eta: 1 \to g f as an extrapolation of an equality predicate (and indeed an equality predicate, as a 1-cell in the monoidal 2-category RelRel of the form 1X×X1 \to X \times X, is just such a unit for the self-duality of XX). Similarly, hom X\hom_X can be rendered as a unit 1X op×X1 \to X^{op} \times X in the monoidal 2-category of profunctors for the adjunction XX opX \dashv X^{op}, 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.

    • CommentRowNumber41.
    • CommentAuthorjamievicary
    • CommentTimeMar 10th 2016
    • (edited Mar 10th 2016)

    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 \infty-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.

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2016

    @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.

    • CommentRowNumber43.
    • CommentAuthorjamievicary
    • CommentTimeMar 10th 2016
    • (edited Mar 10th 2016)

    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.

    • CommentRowNumber44.
    • CommentAuthorMike Shulman
    • CommentTimeMar 10th 2016

    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?

    • CommentRowNumber45.
    • CommentAuthorjamievicary
    • CommentTimeMar 10th 2016
    • (edited Mar 10th 2016)

    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.

    • CommentRowNumber46.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2016
    • (edited Mar 11th 2016)

    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 nn-categories for unbounded nn.

    It might might be worthwhile to try to combine OpTT, as the fundametal internal language of an (,)(\infty,\infty)-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 (,)(\infty,\infty)-categories is compatible with established models of (,n)(\infty,n)-categories (hence in particular with models of (n,n)(n,n)-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.

    • CommentRowNumber47.
    • CommentAuthorjamievicary
    • CommentTimeMar 11th 2016

    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 (,)(\infty,\infty)-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.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2016

    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.

    • CommentRowNumber49.
    • CommentAuthorjamievicary
    • CommentTimeMar 11th 2016
    • (edited Mar 11th 2016)

    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.

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2016

    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.

    • CommentRowNumber51.
    • CommentAuthorjamievicary
    • CommentTimeMar 11th 2016
    • (edited Mar 11th 2016)

    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.

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2016
    • (edited Mar 11th 2016)

    I am just highlighting that there is a difference between “it is not conceivable” and “I personally find it difficult”. nn-Category theory for arbitrary nn 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 nn-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.

    • CommentRowNumber53.
    • CommentAuthorjamievicary
    • CommentTimeMar 11th 2016

    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 \infty-categories. If a result is proven in an opetopic \infty-category, I believe (recalling historical discussions with Eric) that it is not clear if it can then be made relevant to a globular \infty-category. It would be good to hear what would be possible in principle here. Maybe it is easier to go from globular to opetopic.

    • CommentRowNumber54.
    • CommentAuthorMike Shulman
    • CommentTimeMar 11th 2016

    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.

    • CommentRowNumber55.
    • CommentAuthorjamievicary
    • CommentTimeMar 11th 2016

    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.

    • CommentRowNumber56.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 18th 2016

    I was going to suggest we put some links in for singularity, resolution of singularities, etc. but they’re not in the greatest shape.

    • CommentRowNumber57.
    • CommentAuthorjamievicary
    • CommentTimeMar 20th 2016

    I have no idea if the concept of ’resolution of singularities’ linked to there is directly relevant for the categorical notion.

    • CommentRowNumber58.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 20th 2016

    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.

    • CommentRowNumber59.
    • CommentAuthorjamievicary
    • CommentTimeMar 20th 2016
    • (edited Mar 20th 2016)

    The fold, cusp, swallowtail, butterfly catastrophes are very relevant; they represent equations that should be satisfied by coherent equivalences in semistrict nn-categories. But many of the singularity resolutions that go into the definition of semistrict nn-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 nn-categories.

    • CommentRowNumber60.
    • CommentAuthorEMF
    • CommentTimeApr 22nd 2016
    I've got another bug. Interchanger reversal (and probably other cells which have input and output that are both one cell) do not cancel with their inverses, and they are often very hard to pull. Also not canceling: interchanger cancel should cancel in snakes. A bit of this could be fixed by having cells where source and target are identity of identity of the same cell interchange (when possible) by a swap (that is exactly self-inverse), but maybe that's a bad idea.
    • CommentRowNumber61.
    • CommentAuthorjamievicary
    • CommentTimeMay 4th 2016

    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.

    • CommentRowNumber62.
    • CommentAuthorjamievicary
    • CommentTimeMay 4th 2016
    • (edited May 4th 2016)

    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.

    • CommentRowNumber63.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2016

    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.

    • CommentRowNumber64.
    • CommentAuthorjamievicary
    • CommentTimeMay 13th 2016

    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.

    • CommentRowNumber65.
    • CommentAuthorEMF
    • CommentTimeJul 20th 2016
    I must report some serious bugs. Much of the time, attempting to apply an INT-[RL](IO)?-S crashes Globular. Also, after opening the 'Nondegenerate Pairing' page, trying to apply the definition of phi* to a diagram containing nothing but phi* completely fails to work.
    • CommentRowNumber66.
    • CommentAuthorjamievicary
    • CommentTimeJul 20th 2016

    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! :)

    • CommentRowNumber67.
    • CommentAuthorEMF
    • CommentTimeJul 20th 2016
    Nondegenerate pairing: 1601.001v1.

    Here's a quick example for Int-LS:
    1607.003v1; open Prop 4; go to source and hit r i (restrict, identity);
    then apply def ysp up at 15; def ysp up inv at 19; pull-through right tangle interchanger above inverse at 20; and pull the pull-throughs to either side of the interchanger between them so they are at 16 and 18. Then try to apply Int-R-S inverse. This will fail and quickly lead to Globular becoming unusable.

    Also, pull-through pull-through can cause trouble:
    1606.002v1; open Lemma_proof and go to target (and restrict);
    pull down the swallowtail_ev_x as far as possible; then pull the interchanger at 7 up and select choice 1. This will lead to a crash if you attempt to work much further.

    Finally, there appears to be a bug with regard to cancelling flipped morphisms. Specifically, foo *1 flip and foo *1 inverse flip fail to cancel. This is a hassle, but not a crash bug, and most likely due to poor handling of inverses?

    Also, I'm a CS student at UConn who finds this fun to play with.
    • CommentRowNumber68.
    • CommentAuthorjamievicary
    • CommentTimeJul 21st 2016

    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.

    • CommentRowNumber69.
    • CommentAuthorEMF
    • CommentTimeJul 21st 2016
    I was playing with Globular and they just happened. Never underestimate the power of bored users to find weird bugs.
    • CommentRowNumber70.
    • CommentAuthorEMF
    • CommentTimeSep 19th 2016
    • (edited Sep 19th 2016)
    Any luck figuring out those bugs yet?

    Also, a suggestion: You could rewrite in OCaml, then use Oscigen and js_of_ocaml to compile to asm.js. This might or might not improve speed, but it will help find bugs.
    • CommentRowNumber71.
    • CommentAuthorEMF
    • CommentTimeNov 16th 2016
    • (edited Nov 16th 2016)
    Is there a reason why Globular is down? The error is ERR_CONNECTION_REFUSED, which seems to me as if the problem is you forgot to pay for another year of hosting.
    The Internet Archive fails to work properly.
    • CommentRowNumber72.
    • CommentAuthorjamievicary
    • CommentTimeNov 16th 2016

    Thanks EMF, fixed!

    • CommentRowNumber73.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 15th 2016

    I added the reference

    • Krzysztof Bar, Aleks Kissinger, Jamie Vicary, Globular: an online proof assistant for higher-dimensional rewriting, arXiv:1612.01093
    • CommentRowNumber74.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 15th 2016

    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?

    • CommentRowNumber75.
    • CommentAuthorjamievicary
    • CommentTimeDec 15th 2016
    • (edited Dec 15th 2016)

    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.

    • CommentRowNumber76.
    • CommentAuthorKeithEPeterson
    • CommentTimeDec 15th 2016

    The computer scientist in me is dying to know, how are n-categories actually represented in code?

    • CommentRowNumber77.
    • CommentAuthorjamievicary
    • CommentTimeDec 15th 2016
    • (edited Dec 15th 2016)

    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.

    • CommentRowNumber78.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 15th 2016
    • (edited Dec 15th 2016)

    @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

    • CommentRowNumber79.
    • CommentAuthorKeithEPeterson
    • CommentTimeDec 15th 2016

    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.

    • CommentRowNumber80.
    • CommentAuthorjamievicary
    • CommentTimeDec 15th 2016

    @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.

    • CommentRowNumber81.
    • CommentAuthorjamievicary
    • CommentTimeDec 15th 2016

    @David, maybe those knots are actually isotopic?

    • CommentRowNumber82.
    • CommentAuthorDavidRoberts
    • CommentTimeDec 15th 2016

    I’m sure the unknot and 4 1 a4^a_1 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.

    • CommentRowNumber83.
    • CommentAuthormatthew_pickering
    • CommentTimeFeb 1st 2017
    • (edited Feb 1st 2017)

    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 f:ABf : A \to B yields a 2-cell BAB \to A by attaching a cup and a cap to appropriate places. Another operator is an intersection operation which takes two 2-cells R,SR, S and yields mult.RS.comultmult . R \otimes S . comult.

    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?

    • CommentRowNumber84.
    • CommentAuthorturion
    • CommentTimeAug 13th 2018

    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 S 2×S 2#CP 2CP¯ 2#CP¯ 2#CP 2S^2 \times S^2 \# CP^2 \cong \overline{CP}^2 \# \overline{CP}^2 \# CP^2, 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!

    • CommentRowNumber85.
    • CommentAuthorjamievicary
    • CommentTimeAug 13th 2018

    Hi Manuel, cool! What reference for the 4d Kirby moves are you using?

    • CommentRowNumber86.
    • CommentAuthorturion
    • CommentTimeAug 13th 2018

    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:

    • Viewing the proof of the lemma I previously mentioned is really slow, even on a fast machine.
    • It would be really nice if cells could be grouped, or at least reordered, so I could organise that workspace properly.
    • CommentRowNumber87.
    • CommentAuthorturion
    • CommentTimeAug 21st 2018

    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/).

    • CommentRowNumber88.
    • CommentAuthorUrs
    • CommentTimeDec 8th 2018

    I have fixed/improved the formatting of the bibtex code for how to cite (here) (this is done by indenting by 6 (six) whitespaces, see the source code)

    diff, v54, current

    • CommentRowNumber89.
    • CommentAuthorKeith Harbaugh
    • CommentTimeApr 24th 2019

    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.

    diff, v55, current

    • CommentRowNumber90.
    • CommentAuthorUrs
    • CommentTimeNov 11th 2022

    completed publication data for this item:

    diff, v58, current

    • CommentRowNumber91.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2023

    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.

    diff, v59, current