Higher groups in homotopy type theory

DOI10.1145/3209108.3209150zbMATH Open1452.03034arXiv1802.04315OpenAlexW2964185027MaRDI QIDQ5145293FDOQ5145293

Authors: Ulrik Buchholtz, Floris van Doorn, Egbert Rijke 

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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"of 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.

Full work available at URL: https://arxiv.org/abs/1802.04315

Recommendations

• Free higher groups in homotopy type theory
• Eilenberg-MacLane spaces in homotopy type theory
• Higher homotopies in a hierarchy of univalent universes
• \(\pi _{n }(S ^{n })\) in homotopy type theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory

zbMATH Keywords

homotopy type theoryhigher groupsLean proof assistant

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Cited In (27)

• Automorphisms of types in certain type theories and representation of finite groups
• Non-accessible localizations
• Univalent categories of modules
• The long exact sequence of homotopy n-groups
• Topological quantum gates in homotopy type theory
• Nilpotent types and fracture squares in homotopy type theory
• Free higher groups in homotopy type theory
• Homology groups of types in stable theories and the Hurewicz correspondence
• Eilenberg-MacLane spaces in homotopy type theory
• Constructing higher inductive types as groupoid quotients
• Good fibrations through the modal prism
• Modal fracture of higher groups
• Eilenberg-MacLane spaces and stabilisation in homotopy type theory
• The Hurewicz theorem in homotopy type theory
• Title not available (Why is that?)
• Higher Structures in Homotopy Type Theory
• Higher inductive types as homotopy-initial algebras
• Modal descent
• Localization in Homotopy Type Theory
• Sequential colimits in homotopy type theory
• Coherence for monoidal groupoids in HoTT
• The real projective spaces in homotopy type theory
• Formalizing double groupoids and cross modules in the Lean theorem prover
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Internal languages of finitely complete \((\infty , 1)\)-categories
• Title not available (Why is that?)
• Higher homotopies in a hierarchy of univalent universes

Uses Software

• Lean

This page was built for publication: Higher groups in homotopy type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145293)