Higher groups in homotopy type theory

DOI10.1145/3209108.3209150MaRDI QIDQ5145293zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

homotopy type theoryhigher groupsLean proof assistant

Mathematics Subject Classification ID

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

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.

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

Cited in

(32)

• Higher homotopies in a hierarchy of univalent universes
• Automorphisms of types in certain type theories and representation of finite groups
• Non-accessible localizations
• On symmetries of spheres in univalent foundations
• Univalent categories of modules
• The long exact sequence of homotopy n-groups
• Nilpotent types and fracture squares in homotopy type theory
• Topological quantum gates 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
• Free commutative monoids in homotopy type theory
• Eilenberg-MacLane spaces and stabilisation in homotopy type theory
• scientific article; zbMATH DE number 7471707 (Why is no real title available?)
• The Hurewicz theorem in homotopy type theory
• Higher inductive types as homotopy-initial algebras
• Higher Structures in Homotopy Type Theory
• Classification of covering spaces and canonical change of basepoint
• 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
• Internal languages of finitely complete ( , 1)-categories
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Central H-spaces and banded types
• scientific article; zbMATH DE number 4181647 (Why is no real title available?)
• Computational synthetic cohomology theory in homotopy type theory

Describes a project that uses

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)