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.

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

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

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

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

]]>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 \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!

]]>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 : A \to B$ yields a 2-cell $B \to A$ by attaching a cup and a cap to appropriate places. Another operator is an intersection operation which takes two 2-cells $R, S$ and yields $mult . 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?

]]>I’m sure the unknot and $4^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.

@David, maybe those knots are actually isotopic?

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

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

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

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

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

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

]]>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?

]]>I added the reference

- Krzysztof Bar, Aleks Kissinger, Jamie Vicary,
*Globular: an online proof assistant for higher-dimensional rewriting*, arXiv:1612.01093

Thanks EMF, fixed!

]]>The Internet Archive fails to work properly. ]]>

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

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.

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

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

]]>