# 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

## Site Tag Cloud

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

1. copied reference from HoTT wiki

Anonymous

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJun 9th 2022

I have made the requested higher groups redirect to the existing entry n-groups.

Then I have hyperlinked infinity-groups, which certainly exists.

By the way, to make good use of all these new category:referenceentries, one should point to them from where the articles are being referenced. I have done so now here.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJun 9th 2022

By the way, we do have an entry delooping. We did not have the requested delooped as a redirect.

I have made it a redirect now, but best to link to standard word form, since we can’t possibly pre-empt all variations as redirects.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJun 9th 2022

In adding the missing publication data, I have taken the liberty of reformatting a litte.

Does it not look much better this way:

Abtract. We present a development of the theory of higher groups, including infinity-groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.

?