Higher Groups in Homotopy Type Theory

DOI10.1145/3209108.3209150zbMath1452.03034arXiv1802.04315OpenAlexW2964185027MaRDI QIDQ5145293

Egbert Rijke, Ulrik Buchholtz, Floris van Doorn

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)

Related Items (11)

Localization in Homotopy Type Theory ⋮ Unnamed Item ⋮ Eilenberg-MacLane spaces and stabilisation in homotopy type theory ⋮ Higher Structures in Homotopy Type Theory ⋮ The Hurewicz theorem in homotopy type theory ⋮ Univalent categories of modules ⋮ The long exact sequence of homotopy n-groups ⋮ Unnamed Item ⋮ Nilpotent types and fracture squares in homotopy type theory ⋮ Good Fibrations through the Modal Prism ⋮ Modal descent

Uses Software

• Lean

This page was built for publication: Higher Groups in Homotopy Type Theory