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.
I have made the requested higher groups redirect to the existing entry n-groups.
Then I have hyperlinked infinity-groups, which certainly exists.
Also link for connective spectrum.
By the way, to make good use of all these new category:reference
entries, one should point to them from where the articles are being referenced. I have done so now here.
In adding the missing publication data, I have taken the liberty of reformatting a litte.
Does it not look much better this way:
Ulrik Buchholtz, Floris van Doorn, Egbert Rijke:
Higher Groups in Homotopy Type Theory
LICS ’18:
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
on infinity-groups in homotopy type theory.
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.
?
1 to 4 of 4