Eilenberg-MacLane spaces in homotopy type theory

DOI10.1145/2603088.2603153MaRDI QIDQ4635651zbMATH OpenOpenAlexFDO

Authors Daniel R. Licata, Eric Finster

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2603088.2603153

zbMATH Keywords

dependent typestype theoryhomotopy type theory

Mathematics Subject Classification ID

Eilenberg-Mac Lane spaces (55P20)

Recommendations

• The real projective spaces in homotopy type theory
• Cellular Cohomology in Homotopy Type Theory
• Higher groups in homotopy type theory
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory

Cited in

(37)

• On Eilenberg-MacLane spaces
• Non-accessible localizations
• Delooping cyclic groups with lens spaces in homotopy type theory
• On symmetries of spheres in univalent foundations
• A Cartesian bicategory of polynomial functors in homotopy type theory
• Synthetic integral cohomology in Cubical Agda
• The long exact sequence of homotopy n-groups
• Nilpotent types and fracture squares in homotopy type theory
• Topological quantum gates in homotopy type theory
• The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
• Higher groups in homotopy type theory
• A foundation for synthetic algebraic geometry
• Parametricity, automorphisms of the universe, and excluded middle
• Synthetic G-jet-structures in modal homotopy type theory
• Types over c(k) spaces
• Adjoint logic with a 2-category of modes
• The equivalence of the torus and the product of two circles in homotopy type theory
• Constructing higher inductive types as groupoid quotients
• Delooping generated groups in homotopy type theory
• The construction of set-truncated higher inductive types
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Homotopical patch 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
• Covering spaces in homotopy type theory
• Higher Structures in Homotopy Type Theory
• Idempotents in intensional type theory
• Using the particle model to find structure in Eilenberg-MacLane spaces
• Localization in Homotopy Type Theory
• Coslice colimits in homotopy type theory
• Modalities in homotopy type theory
• The structuralist mathematical style: Bourbaki as a case study
• The real projective spaces in homotopy type theory
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
• Central H-spaces and banded types
• Computational synthetic cohomology theory in homotopy type theory

Describes a project that uses

Uses Software

• Agda
• Coq

This page was built for publication: Eilenberg-MacLane spaces in homotopy type theory

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