Eilenberg-MacLane spaces in homotopy type theory

DOI10.1145/2603088.2603153zbMATH Open1395.68249OpenAlexW2153583112MaRDI QIDQ4635651FDOQ4635651

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

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

zbMATH Keywords

dependent typestype theoryhomotopy type theory

Mathematics Subject Classification ID

Eilenberg-Mac Lane spaces (55P20)

Cited In (27)

• On Eilenberg-MacLane spaces
• Non-accessible localizations
• A Cartesian bicategory of polynomial functors in homotopy type theory
• Synthetic integral cohomology in Cubical Agda
• The long exact sequence of homotopy n-groups
• Topological quantum gates in homotopy type theory
• Nilpotent types and fracture squares in homotopy type theory
• The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
• Higher groups in homotopy type theory
• Adjoint logic with a 2-category of modes
• Types over c(k) spaces
• The equivalence of the torus and the product of two circles in homotopy type theory
• Constructing higher inductive types as groupoid quotients
• Homotopical patch theory
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• The construction of set-truncated higher inductive types
• 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
• Idempotents in intensional type theory
• Using the particle model to find structure in Eilenberg-MacLane spaces
• Localization in Homotopy Type Theory
• Modalities in homotopy type theory
• The real projective spaces in homotopy type theory
• The structuralist mathematical style: Bourbaki as a case study
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory

Uses Software

• Coq
• Agda

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)