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
1 to 8 of 8