Not signed in (Sign In)

# Start a new discussion

## 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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorjamievicary
• CommentTimeDec 7th 2018

The stub for homotopy.io.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeDec 7th 2018

Cool!

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeDec 7th 2018

There is no link on the page to the thing being described, is that right/intended?

• CommentRowNumber4.
• CommentAuthorAlizter
• CommentTimeDec 7th 2018

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

• CommentRowNumber5.
• CommentAuthorDavidRoberts
• CommentTimeDec 7th 2018

Presumably the link will be something like homotopy.io, but not yet released.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeDec 8th 2018
• (edited Dec 8th 2018)

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.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeDec 8th 2018
• (edited Dec 8th 2018)

okay, I have linked back to here from proof assistant and added pointer to the following references:

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

• CommentRowNumber8.
• CommentAuthorjamievicary
• CommentTimeDec 10th 2018
Thanks for these edits. The intention is not to tease but to get something in place for the release of the proof assistant, hopefully later this week.
• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeDec 31st 2018

added some more hyperlinks to keywords in the text, and added the arXiv-identifier for today’s preprint version of

• CommentRowNumber10.
• CommentAuthorjamievicary
• CommentTimeFeb 5th 2019

Updated information about the user interface.

• CommentRowNumber11.
• CommentAuthorjamievicary
• CommentTimeFeb 5th 2019

Some details about homotopy construction.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeFeb 6th 2019
• (edited Feb 6th 2019)

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.

• CommentRowNumber13.
• CommentAuthorjamievicary
• CommentTimeFeb 7th 2019

Significant updates to the tool description. @Urs: yes, I will add such a link soon.

Add your comments
• Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
• To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

• (Help)