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.
Cool!
There is no link on the page to the thing being described, is that right/intended?
@Urs It seems to be a tease
The proof assistant is still under development, and is not yet released for general use. It can be considered a successor to the existing proof assistant Globular, which allows the construction of formal proofs in a strictly associative and unital model of 4-categories.
Presumably the link will be something like homotopy.io, but not yet released.
Okay, thanks. Of course I am sympathetic to the cause, but let’s invest a minimum of energy to make this more of an actual nLab page.
I am on my phone right now, maybe somebody can help me:
First, there must exist some preliminary resource that the page can point to. If nothing else let’s add pointer to Dorn’s talk slides on associative n-categories that Google knows about.
Then, let’s cross link with our page proof assistant.
Finally also the page associative n-category is currently a little unusual for the nLab in its emphasis of announcement over content. Maybe somebody could help Jamie to edit this a little, cross-link with related entries, add references, etc.
okay, I have linked back to here from proof assistant and added pointer to the following references:
Christoph Dorn, Associative $n$-categories, talk at 103rd Peripatetic Seminar on Sheaves and Logic (pdf)
Christoph Dorn, Associative n-categories PhD thesis (pdf)
I suggest the links to contibutors’s names in the entry should all point to their corresponding $n$Lab entries, for link stability, but I won’t implement that, or not now anyways
added some more hyperlinks to keywords in the text, and added the arXiv-identifier for today’s preprint version of
Thanks for adding this.
I’d suggest the main page homotopy.io should have some pointer offering indication on what’s going on, maybe a pointer to the Overview of Functionality that you just added.
added pointer to:
Incidentally, most of the references listed do mention homotopy.io
(though not the first ones, which seem to be included just as background on associative $n$-categories?) but none of the references seems to be really about homotopy.io
as such.
The main link given
does not work for me: it gives me the “Potential Security Risk Ahead”-thing. I am sure somebody will tell me that I can work around this using a VPN or something, but is there a link which would just work?
The one alterntive (?) I could find is
which I have added. But as with most github pages, this doesn’t serve as a landing page for outsiders.
1 to 15 of 15