Sequential colimits in homotopy type theory

DOI10.1145/3373718.3394801zbMATH Open1498.03035OpenAlexW3029044157MaRDI QIDQ5145685FDOQ5145685

Floris van Doorn, Kristina Sojakova, 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

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

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)

Cited In (3)

• 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)