Sequential colimits in homotopy type theory

DOI10.1145/3373718.3394801zbMATH Open1498.03035OpenAlexW3029044157MaRDI QIDQ5145685FDOQ5145685

Authors Kristina Sojakova, Floris van Doorn, Egbert Rijke 

Publication date 21 January 2021

Published in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

homotopy type theoryhigher inductive typessequential colimits

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Recommendations

• Homotopy limits in type theory
• Semantics of higher inductive types
• Higher inductive types as homotopy-initial algebras
• Inductive types in homotopy type theory
• Higher groups in homotopy type theory

Cited in

(4)

• Homotopy limits in type theory
• Nilpotent types and fracture squares in homotopy type theory
• The Hurewicz theorem in homotopy type theory
• Localization in Homotopy Type Theory

This page was built for publication: Sequential colimits in homotopy type theory

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