Higher Groups in Homotopy Type Theory

## Authors: Ulrik Buchholtz, Floris van Doorn and Egbert Rijke

## Paper Information

Title: | Higher Groups in Homotopy Type Theory |

Authors: | Ulrik Buchholtz, Floris van Doorn and Egbert Rijke |

Proceedings: | LICS PDF files |

Editors: | Anuj Dawar and Erich Grädel |

Keywords: | homotopy type theory, higher groups, Lean proof assistant |

Abstract: | ABSTRACT. 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 has the structure of an infinite loop type. Most of the results have been formalized in the Lean proof assistant. |

Pages: | 10 |

Talk: | Jul 09 12:00 (Session 47E) |

Paper: |