Path spaces of higher inductive types in homotopy type theory

DOI10.5555/3470152.3470159MaRDI QIDQ6654472zbMATH OpenFDO

Authors Nicolai Kraus, Jakob von Raumer

Publication date 19 December 2024

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) 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

• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• Homotopy type theory in Lean
• The equivalence of the torus and the product of two circles in homotopy type theory
• Inductive types in homotopy type theory

This page was built for publication: Path spaces of higher inductive types in homotopy type theory

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