Paper: Classifying 2-Groups in Homotopy Type Theory (at LICS 2026)

Authors: Perry Hart Owen Milner

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.55

Abstract

Under the homotopy hypothesis, higher dimensional groups are defined as pointed homotopy types whose homotopy groups vanish outside a certain range. In particular, a 2-group is a pointed connected homotopy 2-type. Classically, 2-groups have two equivalent algebraic descriptions: one in terms of weak monoidal categories and the other in terms of group cohomology. We present these two classifications of pointed connected 2-types in homotopy type theory, thereby providing internal, constructive counterparts to the traditional classifications of 2-groups. Our first classification (in terms of monoidal categories) takes the form of a bicategorical equivalence, while our second is a type equivalence that extends to n-groups for all n ≥ 2. We have mechanized our results in Agda.

BibTeX

  @InProceedings{HartMilner-Classifying2Groupsi,
    author = 	 {Perry Hart and Owen Milner},
    title = 	 {Classifying 2-Groups in Homotopy Type Theory},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {55:1--55:25},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.55}
  }