Higher Groups in Homotopy Type Theory
| Autor: | Floris van Doorn, Egbert Rijke, Ulrik Buchholtz |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Pure mathematics media_common.quotation_subject Structure (category theory) 0102 computer and information sciences Type (model theory) 01 natural sciences Identity (mathematics) Infinite loop FOS: Mathematics Algebraic Topology (math.AT) Mathematics - Algebraic Topology 0101 mathematics media_common Mathematics Group (mathematics) 010102 general mathematics Mathematics - Logic Infinity Logic in Computer Science (cs.LO) 03B15 Type theory 010201 computation theory & mathematics Homotopy type theory F.4.1 Logic (math.LO) |
| Zdroj: | LICS |
| DOI: | 10.48550/arxiv.1802.04315 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|